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