CODEWITHSUNDEEP
z3smtconstraint-programminggecode
user13387285
user13387285

Reputation: 47

Constraint solver vs SMT solver

can someone give me examples that can be solved using SMT solver ( like microsoft z3 ) but cant be solved by constraint solvers ( like Gecode ) ?? What is the basic difference between constraint solver and SMT solver?

Upvotes: 1

Views: 901

Answers (1)

alias
alias

Reputation: 30418

In general SMT solvers can handle many theories of interest: Integers, reals, strings, sequences, sets, uninterpreted functions, data-types, recursive definitions, linear and non-linear arithmetic...

You can take a look at http://smtlib.cs.uiowa.edu/logics.shtml to see the common logics that are supported. Where SMT solvers shine is how you can freely mix-and-match constraints from these domains in one common framework.

I'm not terribly familiar with Gecode, but I presume it is much more focused, looking at only a class of constraints. This, of course, would make it very powerful for the domain it is intended for, but would also mean they don't have the generality offered by SMT solvers.

If you are trying to "pick" one, I'd recommend deciding on a case-by-case: For each problem you might find the winner might be an SMT-solver or some other constraint solver that's not based on SMT-technology. I doubt you can "uniquely" pick one over the other for any problem you might have. If you post specific-questions you are interested in, you can get better suggestions.

Upvotes: 2

Related Questions