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

<p>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 ?</p>

CC BY-SA 3.0
2011-07-08T14:17:37.113Z
Most likely the main advantage of CSP solvers is  expressiveness. What you gain in expressiveness, you lose in performance.
Dave Clarke
CC BY-SA 3.0
2011-07-08T16:52:06.617Z
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.
mhum
CC BY-SA 3.0
2011-07-09T00:07:23.850Z
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.
Opt
<sat><csp>
When is CSP faster than SMT/SAT?
jah
# When is CSP faster than SMT/SAT?

(Asked by: username_0 on 2011-07-08)

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 ?

**Tags:** sat, csp
> **Comments:**
> **username_1**: Most likely the main advantage of CSP solvers is  expressiveness. What you gain in expressiveness, you lose in performance.  
> **username_2**: 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.  
> **username_3**: 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.  

---

## 0 answers

