= Solution
\b[The translation gives a sound and complete route through an optimized <SAT solver>; it trades access to general-purpose <SAT> machinery against encoding cost and the possible loss of constraint-specific structure.] Modern <SAT solvers> use efficient <unit propagation>, adaptive branching and <clause learning>. Learned <Boolean clauses> can summarize conflicts involving many original <variables>, allowing later branches to avoid repeating the same failed combination. The reduction also offers a standard, reusable interface: improvements to a <SAT solver> can benefit many finite-domain <constraint satisfaction problems>.
The <Boolean formula> may be much larger than the original <constraint satisfaction problem>, especially for a succinct high-arity relation. One original <variable> becomes many indicators, and general branching may lose the interpretation that the <minimum remaining values> and <degree heuristic> exploit directly. Native <constraint propagation> can exploit a relation without enumerating all its forbidden tuples. Even in the binary case, stronger propagation does not follow just from switching to <SAT>.
For example, take $D_X=\{1,2\}$, $D_Y=\{a,b,c\}$, and let the only allowed pairs be $(1,c),(2,a),(2,b)$. The forbidden-pair encoding contains $\neg p_{X,1}\lor\neg p_{Y,a}$ and $\neg p_{X,1}\lor\neg p_{Y,b}$. If $p_{Y,c}$ becomes false, <arc consistency> deletes $X=1$ because it has no support. Yet the direct encoding has no unit <Boolean clause> forcing $\neg p_{X,1}$: both $a,b$ remain possible individually, so plain <unit propagation> does not make that deletion. A <SAT solver> can eventually derive it through additional reasoning or search. Conversely, <clause learning> can combine information beyond the local consistency enforced by <AC-3>. \b[Neither approach uniformly dominates:] performance depends on representation, propagation strength and the instance's structure; both still face exponential worst-case search on general inputs.
Back to article page
