Direct SAT encoding of finite-domain constraints (${\phi }_P$)

Represent each original value choice $X_i=v$ by a Boolean variable $p_{i,v}$ and impose an exactly-one constraint for each original variable. For every forbidden tuple $(v_i{)}_{i\in S}$ of a constraint with scope $S$, add the Boolean clause ${\bigvee }_{i\in S}\neg p_{i,v_i}$. A complete original assignment satisfies every constraint exactly when its one-hot indicators satisfy all these Boolean clauses: each forbidden-tuple Boolean clause excludes precisely that joint choice. A satisfying assignment decodes by reading the unique true indicator for each original variable.

For constraint domain sizes $q_i$, pairwise uniqueness requires ${\sum }_i\left(\genfrac{}{}{0ex}{}{q_i}{2}\right)$ Boolean clauses. If a constraint has $f_C$ forbidden tuples and arity $r_C$, its contribution is $f_C$ Boolean clauses and $r_C{f}_C$ literal occurrences. Thus bounded arity gives a polynomial-size encoding in explicitly listed domains, whereas enumerating a succinct high-arity relation can be exponential in its description length. Unit propagation on this encoding can be weaker than arc consistency on the original binary constraints.