3
$\begingroup$

I have a system of constraints described by a set of clauses of the form $x_1 \neq x_2 \lor \dots \lor x_{i-1} \neq x_i$, for instance:

x1 != x2
x3 != x4 or x5 != x6

and I need to find the smallest set $A$ such that $x_1, \dots x_n \in A$, and of course an instanciation of those variables.

Note that I'm not working with numbers, so I don't have any other sorts of inequalities (like $x_i \leq x_j$, etc.), only $x_i \neq x_j$.

Has this problem a name ? Is there a specific algorithm for this problem ?

I was planning to use a SMT solver for this, replacing $A$ by $\mathbb{N}$ and adding the constraint $\forall i, x_i \leq k$ while minimizing $k$. This works fine but I feel like it's a bit too much.

Thanks for your help!

Improve this question
$\endgroup$
3
  • 3
    $\begingroup$ Graph coloring is a special case of your problem: Every variable $x_i$ corresponds to a vertex of the graph, and an edge between two vertices means that the two variables must take different values. $\endgroup$
    – Gamow
    Commented May 22, 2018 at 13:31
  • $\begingroup$ @Gamow I thought abouth that, but how do you model $x_3 \neq x_4 \lor x_5 \neq x_6$ ? If a put an edge between $x_3,x_4$ and an other one between $x_5,x_6$, I'll have $x_3 \neq x_4 \land x_5 \neq x_6$, right? $\endgroup$
    – Jingbee
    Commented May 22, 2018 at 13:55
  • $\begingroup$ @Jingbee - I believe the claim was that an instance of Graph Coloring can be formulated as an instance of your problem - so you are not trying to build a graph from a formula, rather a formula from a graph. This formula doesn't even use the full expressive power of your constraint system - even just the not-equals constraints are enough to describe graph coloring; therefore, your problem encapsulates graph coloring as a special case. $\endgroup$
    – Neeldhara
    Commented Jun 24, 2018 at 13:52

1 Answer 1

Reset to default
2
$\begingroup$

Your problem is at least as hard as SAT: given a CNF formula $\varphi$ on variables $x_1,\dots,x_n$, add variables $x_{\bot},x_{\top}$ and the clause $x_{\bot} \ne x_{\top}$, and translate each occurrence of the literal $x_i$ in $\varphi$ to $x_i \ne x_\bot$ and each occurrence of the literal $\overline{x_i}$ to $x_i \ne x_\top$. In this way each clause of $\varphi$ can be translated into a constraint of your form. Then $\varphi$ is satisfiable iff the resulting set of constraints can be satisfied by a set $A$ of size 2 (i.e., $|A|=2$). Therefore, if we could solve your problem, we could solve SAT. So your problem is at least as hard as SAT.

Consequently, solving your problem by bit-blasting to SAT is a reasonable way to solve your problem. I don't think you should expect a much better algorithm.

This does leave some room for cleverness in how you encode your problem as a SAT instance. You could encode each $x_i$ either with a one-hot encoding (using $nk$ bits), or in binary (with $n\lceil \lg k \rceil$ bits), or by encoding which pairs of $x$'s are equal (with ${n \choose 2}$ bits, i.e., a boolean variable for each $i,j$ encoding whether $x_i = x_j$, with transitivity constraints enforced). Which you choose is likely to affect the running time in practice. I suggest experimenting a bit with different possible ways of encoding your problem as SAT to see what seems to work best for the types of problems you are dealing with. (I don't particularly expect a SMT solver to do any better than a SAT solver here, but you could try it.)

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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