 Solution

Use an exactly-one constraint for each finite-domain variable and a Boolean clause forbidding each disallowed constraint tuple. Let the variables be $X_1,\dots ,X_n$, with explicitly listed finite constraint domains $D_i$, and let constraint $C$ have distinct-variable scope $S_C$ and allowed relation $R_C\subseteq {\prod }_{i\in S_C}{D}_i$. Introduce a Boolean variable $p_{i,v}$ for every $v\in D_i$, interpreted as $X_i=v$. The direct SAT encoding of finite-domain constraints isIn the middle logical conjunction, each unordered distinct pair is included once. The first Boolean clause requires at least one value, the pairwise Boolean clauses permit at most one, and a final Boolean clause is false exactly when all coordinates of one forbidden tuple are selected. The formula is in conjunctive normal form. An empty constraint domain produces an empty Boolean clause, correctly making the instance unsatisfiable.

For soundness of the reduction, a solution $x$ of the constraint satisfaction problem gives the Boolean valuation $p_{i,v}=1$ exactly when $v=x_i$. Every exactly-one constraint holds; a forbidden tuple differs from $x$ on at least one scoped coordinate, making its negative Boolean clause true. Thus $x$ supplies a satisfying assignment for ${\phi }_P$.

Conversely, a satisfying assignment selects a unique value $x_i$ for every $X_i$. If a constraint failed, the selected scoped tuple would belong to $F_C$, and its entire negative Boolean clause would be false. That contradicts satisfiability. Hence $x$ is a solution. Decoding takes $O({\sum }_i|D_i|)$ by scanning the value indicators. This proves $P$ has a solution if and only if ${\phi }_P$ is satisfiable.

For explicit size accounting, put $q_i=|D_i|$, $r_C=|S_C|$ and $f_C=|F_C|$. There are ${\sum }_i{q}_i$ Boolean variables,Boolean clauses, andliteral occurrences. These formulas count nonempty scopes; a false zero-arity constraint contributes an empty Boolean clause, while a true one contributes none. Formula storage is $O(K+L)$ literal-sized records; a bit-level encoding also stores indicator indices. With maximum constraint domain size $q$, $m$ constraints and maximum arity $r$, this is bounded by $O(n{q}^2+mr{q}^r)$ for nontrivial domains and scopes. In the common binary case it is $O((n+m)q^2)$.

The input representation matters: listing all forbidden tuples costs up to ${\prod }_{i\in S_C}{q}_i$ tests per constraint. This is polynomial for bounded arity and explicitly represented domains, but can be exponential in the description length of a succinct high-arity constraint. The translation is valid in that case without constituting a polynomial-size reduction. If a compact constraint is supplied as a polynomial-size Boolean circuit, one may instead encode that circuit using auxiliary Boolean variables and local conjunctive normal form equivalences, with size proportional to the circuit. No compact representation is silently assumed.

For the instance in (c), after unary filtering there are $17$ indicators. The five at-least-one Boolean clauses, $22$ pairwise at-most-one Boolean clauses and $24$ forbidden-equality Boolean clauses give $51$ Boolean clauses. Setting only $p_{a,1},p_{b,2},p_{c,3},p_{d,2},p_{e,1}$ true encodes the displayed solution.