Typical Boolean formulas can be added to SAT solver using class SatTranslation. This class offers translation of typical operations as and, or, not, xor, implication, all equalities and inequalities as well as reified versions of these. The following code illustrates use of the translation.
The code generates Boolean clause of the form (a → b) ∧ (a∧b = c) that is translated to CNF Boolean clause supported by the SAT solver.
(a ∨ b) ∧
(a ∨b ∨ c) ∧
(a ∨c) ∧
(b ∨c)
The SAT translation performs several tasks. First, it defines SAT literals and binds Boolean variables to these literals. In our example, Boolean variables a, b and c are translated to literals, denoted by the same letter in the above formulas but they are different representations. Second, it adds CNF clauses representing Boolean clauses to the SAT solver. The SAT wrapper will then propagate changes between CP and SAT solver based on the evaluations of both solvers.
The search for solutions is identical with CP framework. In case of the example, we can make search on variables a, b and c. All solutions to the constraint are {0, 0, 0}, {0, 1, 0}, {1, 1, 1}