About Sat4j

The aim of the SAT4J library is to provide an efficient library of boolean engines for solving satisfaction, optimization and other related problems based on SAT technology in Java. Sat4j targets first users of SAT ”black boxes”, willing to embed SAT technologies into their application without worrying about the details. Since we use the library for our own research, it is also possible for SAT researchers to use it as a basis for their work.

SAT4J includes our implementation in Java of Niklas Een and Niklas Sorenson’s MiniSAT specification:An extensible SAT solver.

Whereas the overall algorithmic of the solver is respected, the design has been adapted to Java practices. Furthermore, the initial design has been extended to allow testing several heuristics and learning schemes.

The library includes a wide variety of tools based on SAT solvers. The most robust part of the code are the "core" and "pb" libraries, which are used within the Eclipse open platform since June 2008.