SAT4J is an open source and free reasoning engine library in Java based on the SATisfiability problem (SAT).
SAT4J library's goal is to provide an efficient library of SAT solvers in Java. Compared to the OpenSAT project, the SAT4J library targets first users of SAT "black boxes", willing to embed SAT technologies into their application without worrying about the details.
Detailed usage instructions for the SAT4J reasoning engine are available
here.
Requirements:
· Java
What's New in This Release: [ read full changelog ]
Bug:
· [SAT-65] - Fix the value of the objective function in maxsat when some constraints are satisfied
· [SAT-75] - create a toString method for negated objects within Dependency Helper
· [SAT-76] - Intermediate results not displayed during optimization
· [SAT-77] - Allow dependencyHelper to return the truth value of a negated object
· [SAT-84] - Maxsat fails with java.lang.ArrayIndexOutOfBoundsException
· [SAT-87] - exploding runtime in case of repeated calls for satisfiability
Improvement:
· [SAT-33] - Improve project documentation (including web site)
· [SAT-85] - Allow easy access to a pseudo boolean optimizer
· [SAT-86] - Add Glucose 21 dynamic restart strategy and enable it by default
· [SAT-88] - Avoid calling visualization code when no visualization is needed
New Feature:
· [SAT-13] - Compute minimal size unsat core
· [SAT-23] - Optimization timeout
· [SAT-68] - Allow computing all MUSes using two calls to the SAT solver
· [SAT-70] - Allow the possibility to compute counter models (negate a formula)
· ...
Find us on Google+
