# transformation of constraint satisfaction to SAT

How can any Constraint satisfaction problem be converted to an instance of Satisfiability? I have a CSP and i know its NP hard to solve it, but i would like to convert to an instance of k-SAT, but im not sure of any algorithm for transformation

-
–  Kyle Jones Mar 28 at 3:18
There are lots of good algorithms and heuristics for solving CSPs. Are you sure that transforming to SAT is the best way? –  David Richerby Mar 28 at 9:14

I'm not sure what you mean by CSP, but suppose that you mean the following: there are $n$ binary variables and $m$ constraints. Each constraint is associated with a $k$-tuple of (distinct) variables, for some $k$ depending on the constraint, along with a subset of $\{0,1\}^k$ which is the allowed assignments for the $k$-tuple of variables.
For example, graph coloring, or rather, whether a given graph $G$ can be $\chi$-colored, can be viewed as a CSP. If there are $n$ vertices (we identify the vertex set with $\{1,\ldots,n\}$) then we have $n$ groups $x_1,\ldots,x_n$ of $\lceil \log_2 \chi \rceil$ variables. For each $i \in \{1,\ldots,n\}$ there is a constraint on each group $x_i$ stating that the assignment for $x_i$ is the binary encoding of a number in the range $\{0,\ldots,\chi-1\}$. For any two connected vertices $(i,j)$ there is a constraint on both groups $x_i,x_j$ stating that $x_i \neq x_j$. This CSP is satisfiable iff $G$ is $\chi$-colorable.
In order to convert such a binary CSP to a SAT instance, we replace each constraint with the corresponding CNF. Continuing the example above, if $\chi = 2$ then for any $i,j$ there is a constraint $x_i \neq x_j$ which we realize as $$(x_i \lor \lnot x_j) \land (\lnot x_i \lor x_j).$$ The resulting CNF is satisfiable iff the CSP is. You can use the standard reduction to convert this CNF to a 3CNF if you wish.