# Non-Boolean SAT

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.

• You also need all clauses of the form $x_i \neq a \lor x_i \neq b$. Commented Sep 17, 2019 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.