9
$\begingroup$

Do CSP solvers have any fundamental advantages over SMT/SAT solvers, in terms of performance?

The answer is going to be problem dependent, so I should also ask: what does a problem need to contain in order for CSP to be faster than SMT/SAT ?

$\endgroup$
3
  • 3
    $\begingroup$ Most likely the main advantage of CSP solvers is expressiveness. What you gain in expressiveness, you lose in performance. $\endgroup$ Jul 8 '11 at 14:17
  • 2
    $\begingroup$ I've heard that CSP solvers' advantage over SAT solvers comes when they've encoded special solving logic for special constraints. One of the most commonly-cited such constraint is "all-different". Unfortunately, I don't have any first-hand data to provide to support this, so this is all hearsay. $\endgroup$
    – mhum
    Jul 8 '11 at 16:52
  • 1
    $\begingroup$ An encoding of certain problems like Market-Split which enables them to be solved quickly can be huge in SAT. CSP is good in such circumstances. Also the logic for special constraints that mhum mentions above is very very useful in problems like quasigroup with holes, etc. and has even been incorporated in integer programming - have a look at the SCIP mixed integer programming solver. $\endgroup$
    – Opt
    Jul 9 '11 at 0:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.