Inside CP-SAT: SAT Translation and CDCL

How CP-SAT translates finite-domain constraint problems into Boolean satisfiability (SAT) clauses, and how the underlying solver searches using Boolean Constraint Propagation (BCP) and Conflict-Driven Clause Learning (CDCL) with non-chronological backjumping.

Step 1 of 157%

Tutorial

Direct Encoding of CP Variables into SAT

CP-SAT solves a constraint problem by rewriting it as a set of Boolean clauses and passing the result to a SAT engine. The first step is replacing every finite-domain variable with a collection of Booleans.

The direct encoding of a CP variable $x$ with domain $D_x = \{v_1, v_2, \ldots, v_k\}$ introduces $k$ Boolean variables

b_{x=v_1},\; b_{x=v_2},\; \ldots,\; b_{x=v_k},

where $b_{x=v_i}$ is true iff the CP variable $x$ takes the value $v_i$ .

Two families of clauses guarantee that $x$ takes exactly one value:

At-least-one (ALO): a single clause

b_{x=v_1} \lor b_{x=v_2} \lor \cdots \lor b_{x=v_k}.

At-most-one (AMO, pairwise): for every pair $i<j$ ,

\lnot b_{x=v_i} \lor \lnot b_{x=v_j}.

The AMO family contributes $\binom{k}{2}$ clauses, one per pair of domain values.

Mini-example. For $x \in \{1, 2\}$ we get $k=2$ Booleans and $1 + \binom{2}{2} = 1 + 1 = 2$ clauses:

b_{x=1} \lor b_{x=2}, \qquad \lnot b_{x=1} \lor \lnot b_{x=2}.