= Direct SAT encoding of finite-domain constraints
{title2=$\varphi_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\binom{q_i}{2}$ <Boolean clauses>. If a constraint has $f_C$ forbidden tuples and arity $r_C$, its contribution is $f_C$ <Boolean clauses> and $r_Cf_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>.
Back to article page
