I was wondering about the complexity of SAT tests with variables $x_i = 0 \lor 1 \lor 2 \dots \lor n$, with clauses being of the form $x_i = a \implies x_j \neq b$. When $n=2$, we have 2SAT, which has linear time algorithms. Meanwhile, if $n > 2$, then if we can almost convert it to 2SAT by having Boolean variables $x_{i,a}$ corresponding to the statement $x_i = a$, however this allows for $x_{i,1}=x_{i,2}= \dots = x_{i,n}=0$, which would leave $x_i$ unassigned.

  • $\begingroup$ You also need all clauses of the form $x_i \neq a \lor x_i \neq b$. $\endgroup$ – Yuval Filmus Sep 17 '19 at 21:48

Your problem is NP-complete, even when the range of the $x_i$ has size 3.

Consider a 3SAT instance with $m$ clauses. We will construct an instance of your problem with $m$ variables $x_1,\ldots,x_m$. The value of $x_i$ will denote the literal satisfied in the $i$th clause. Correspondingly, if the $a$th literal in the $i$th clause is the negation of the $b$th literal in the $j$th clause then we will have the constraint $x_i \neq a \lor x_j \neq b$. This gives $O(m^2)$ constraints.

Given a satisfying assignment of the new instance, we can decode a satisfying assignment for the original one by reading the values of the satisfied literals in all clauses. By construction, each original variable is assigned at most one value in this way. Conversely, if the original instance is satisfiable, then a satisfying assignment naturally leads to a satisfying assignment to the new instance.


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.