When to use SAT vs Constraint Satisfaction?

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?)

• Note that a problem can't be too hard if you want to reduce to SAT. – Raphael May 28 '13 at 7:15
• Or why only focus on SAT/CSP, how about SMT? – Juho May 28 '13 at 15:07
• Using a constraint solver tool has the advantage that you can easily try some optimizations (e.g. simmetry breaking techniques) on instances that are not too hard (and check the effectiveness of such optimizations). Furthermore many of them can output a standard CNF file as intermediate output. – Vor May 28 '13 at 15:35
• Great point, @Juho! SMT is worth considering, too -- feel free to compare all three (SAT, CSP, SMT), if you have any thoughts on that. – D.W. May 28 '13 at 16:01
• I had the same question, thanks for asking. – xxx--- Jun 10 '19 at 0:59

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.