SAT-Solving a system of one-hot constraints [closed]

Question

Closed. This question needs to be more focused. It is not currently accepting answers.

---

Want to improve this question? Update the question so it focuses on one problem only by editing this post.

Closed 8 years ago.

Improve this question

I'm trying to solve a SAT problem that consists of one-hot constraints only. Right now I'm using the one-hot encoding proposed by Claessen in Sec. 4.2 of [1] and MiniSAT.

I wonder if there is a better way of solving such a problem, e.g. a class of solvers that is a better match for this kind of problems compared to CNF-based SAT solvers. I've searched a bit but can't find much information on SAT and one-hot constraints at all.

[1] Successful SAT Encoding Techniques. Magnus Bjiirk. 25th July 2009

Answer 1

Satisfiability modulo theorem solvers are often a good choice for expressing mathematical problems that would otherwise end up using one-hot CNF encodings. A key insight is that with CNF and DPLL-based solvers alone you're limited to what unit propagation can discover efficiently. At a higher level of abstraction there are theories of numbers and sets that can be used to prune the search space before selectively applying a SAT solver to more appropriate subproblems. That's what SMT gives you, along with more expressive power and a much more pleasant language in which express relationships.

But if you're stuck with one-hot constraints with no associated higher level math problem, there are more efficient ways to encode onehot constraints that require only a linear number of new clauses to express the relation instead of the usual quadratic increase. See

Efficient CNF Encoding for Selecting 1 from N Objects by Klieber and Kwon.