Sat4j: the boolean satisfaction and optimization library for Java
| Product | Maven declaration | Description | Target Audience | Maturity | Input Format | Dependencies |
|---|---|---|---|---|---|---|
SAT4J Core  |
<dependency> <groupId>org.sat4j</groupId> <artifactId>org.sat4j.core</artifactId> <version>2.3.1</version> </dependency> |
Lightweight constraint programming with a SAT solver. Ships with Eclipse/Equinox 3.4+ as OSGi bundle org.sat4j.core. | Java developers, Researchers | Production | Dimacs CNF or AIG | None |
SAT4J SAT  |
<dependency> <groupId>org.sat4j</groupId> <artifactId>org.sat4j.sat</artifactId> <version>2.3.1</version> </dependency> | SAT Toolkit in Java. Offers a command line interface to SAT4J core allowing to easily test various SAT solver configurations | SAT researchers | Production | Dimacs CNF or AIG | SAT4J Core, Apache Jakarta Commons (BeanUtils, CLI) |
SAT4J Pseudo  |
<dependency> <groupId>org.sat4j</groupId> <artifactId>org.sat4j.pb</artifactId> <version>2.3.1</version> </dependency> | Pseudo Boolean Solvers. Ships with Eclipse/Equinox 3.4+ as OSGi bundle org.sat4j.pb. | Java developers, Researchers | Production | SAT4J Core | |
SAT4J Maxsat  |
<dependency> <groupId>org.sat4j</groupId> <artifactId>org.sat4j.maxsat</artifactId> <version>2.3.1</version> </dependency> | MAX SAT Solvers based on reduction to Pseudo Boolean optimization problems. | Java developers, Researchers | Production | SAT4J Core, SAT4J PB, Apache Jakarta Commons | |
SAT4J CSP  |
<dependency> <groupId>org.sat4j</groupId> <artifactId>org.sat4j.csp</artifactId> <version>2.3.1</version> </dependency> | CSP solvers based on a translation into SAT. | Researchers | Ongoing development | SAT4J Core, Rhino | |
Sudoku Demo  | SAT-based Sudoku generator and solver. Contributed by Ivor Spence Also available online as an applet | Sudoku lovers | Production | Most common Sudoku online formats | SAT4J Core. Ships as a all-in-one package (SAT4J core included). |
