Download!
(from OW2 Gitlab)
See the release notes or download SAT4J 1.7 now!
A new version of the Sudoku as Satisfiability demo written by Ivor Spence has been released. That demo has been customized for the French Science Fest 2006. See the information for the science fest (in French) or download the sudoku demo now!
See the release notes or download SAT4J 1.6 now!
Ivor Spence and Kerry Soileau joined the SAT4J project in January 2006.
All the details regarding the preparation for the SAT Race will be available on the project wiki.
The default CSP to SAT translator was not correct: some constraints were missing when a value had an empty support. That release fixes this problem. There is no other changes. If you are not using the CSP translator, there is no need to update now.
A new CSP to SAT translator is available on CVS, that generalizes support encoding to nary constraints, based on the work of Bessiere et al 2003. The output of the CSP reader has also been improved.
SAT4J is now being hosted on ObjectWeb.
The release 1.5 of SAT4J is now available. Note that this version requires Java 5.
That release follows the participation of the library to the Fourth SAT competition, First Pseudo Boolean evaluation and First CSP competition. You can check by yourself that SAT4J performed reasonably against current state-of-the-art SAT/PB/CSP solvers.
Download now!
Our SAT based CSP solver is performing quite well in the CSP competition (look for dleberre/1 solver in yellow). As a result, we improved further the CSP to SAT translator.
Interested in testing that new CSP solver by yourself?
java -jar sat4j-1.5.jar path/to/bench.txt
It is also possible to prefix any file with CSP or CSP2 to explicitely mention that the file contains a CSP instance:
java -jar sat4j-1.5.jar CSP:path/to/bench.txt
java -jar sat4j-1.5.jar CSP2:path/to/bench.txt
