9

SMT-Solver can be used for constraint solving. As we known, CSP solvers are also for constraint solving for many years. So what's the advantage of SMT-solver over CSP solvers?

user1393905
  • 121
  • 5

1 Answers1

4

That entirely depends on what you want to do. You can translate both to SAT and solve constraint problems as a SAT problem. Constraint solvers usually offer the highest level of abstraction when it comes to modelling the problem. SAT solvers are very fast, but depending on your problem an SMT or constraint solver might be faster.

There is no general answer to your question. It depends on your particular use case.

Lars Kotthoff
  • 107,425
  • 16
  • 204
  • 204
  • Yes, you are right, thank your~And I want to know when SMT solvers run faster than CSP solvers? or what kind of problems are better suited for SMT solvers and conversely? Does SMT solvers can deal with optimization problems, which can be handled by CSP solvers well? – user1393905 May 15 '12 at 13:45
  • Both constraints and SMT can deal with optimisation problems, although I believe that support for this in actual solvers is more common in constraints. There are no set rules when SMT/constraints/SAT is better/faster/... It really does depend on the actual problem you're trying to solve. – Lars Kotthoff May 15 '12 at 16:25
  • SMT solvers are more general and henceforth cover a larger domain as compared to constraint solvers. – user2994783 Dec 29 '21 at 15:54