When to use SAT vs Constraint Satisfaction?

Question

If I have a hard problem, one standard approach is to express it as a SAT instance and try running a SAT solver on it. Another standard approach is to express it as a constraint satisfaction problem, and try using a CSP solver. The two feel somehow vaguely similar in what sorts of problems can be naturally expressed in their input format.

Are there any guidelines or rules of thumb for how to recognize, for a given problem, which approach is more likely to yield good results? Is there any guidance anyone can offer about which sorts of problems can be handled better by SAT solvers than by CSP solvers, or vice versa?

(Obviously, there are some easy problems that can be solved by both approaches. There are also some hard problems that can't be usefully solved by either approach. Let's set those aside. The case where guidance is most helpful are problems where either SAT solvers perform better than CSP solvers, or where CSP solvers perform better than SAT solvers. How do I recognize when a SAT solver is likely to be a better fit than a CSP solver, or when a CSP solver is likely to be a better fit than a SAT solver -- i.e., which approach to try first?)

Answer 1

I think this is a very good question. You could also ask: when to use a SMT solver? I have a feeling it might be hard to determine before modeling the problem and actually running the CSP/SAT/SMT solvers and finding out. It is well known that even different solvers perform very differently on the same instances! My intuition also comes from the fact that there are potentially many ways of modeling a problem. Furthermore, there are many ways of doing search and inference, depending on what type of constraints is used (if the formalism in question allows different types).

Take for example the standard Sudoku puzzle. For the standard $8 \times 8$ puzzle, a modern SAT/CSP solver will solve any such puzzle in an instant. However, I would rather use a CSP solver because it is easier to express my intention. The mentioned puzzle needs $9+9+9=27$ alldiff constraints, and I'm done. There's actually quite a bit of research in the context of CSP solvers trying to solve Sudoku instances of different size. As far as I remember, they don't do any comparisons between SAT, but rather try to determine what kind of inference works the best, or what kind of Sudoku puzzles are hard. I don't know if for say $32 \times 32$ Sudoku puzzles, SAT solvers would be faster than CSP solvers.

Different formalisms are able to capture domain specific information and exploiting it better and in different ways. For a bit more on this, see the answer and the comments here.