Chapter 7
SAT solver

JaCoP has a SAT solver that can be used together with JaCoP solver. It has been developed by Simon Cruanes and Radosław Szymanek. The SAT solver can be integrated in JaCoP as a SAT constraint and used with JaCoP search methods. This functionality is offered by a org.jacop.satwrapper.SatWrapper class. Typical translation of Boolean constraints, used in flatzinc compilations are defined in
org.jacop.satwrapper.SatTranslation.

 7.1 Boolean expressions translations
 7.2 FDV encoding and constraint translations