Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

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

share|improve this question
1  
    
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
add comment

1 Answer 1

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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