4
$\begingroup$

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

$\endgroup$
5
$\begingroup$

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.

We can also handle CSPs which are not binary, i.e., in which the variables are not binary but rather have some finite domain. The idea is similar to how I described coloring as a CSP above, and left to the reader.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.