4 ms·

In terms of applicability, SMT (satisfiability module theory) solvers basically allow you to do things which are slightly more complex than plain SAT solving.

In terms of applicability, SMT (satisfiability module theory) solvers basically allow you to do things which are slightly more complex than plain SAT solving. If you're looking to learn more, Leonardo has a nice introduction to SMT and its applications over here: http://dl.acm.org/citation.cfm?id=1995394 http://dl.acm.org/citation.cfm?id=1995394. To make a long story short, various problems in program verification and static analysis have seen success with SMT. /some academic navel-gazing follows. Yices (http://yices.csl.sri.com/index.shtml http://yices.csl.sri.com/index.shtml) and Z3 are the two main SMT solvers used by academics today. Yices is the "original" solver and was developed by Leonardo de Moura and Bruno Dutertre at SRI in the mid-2000s. At some point towards the end of the last decade, Leonardo moved to Microsoft Research and for reasons which are unclear started working on Z3 independently. I am told that Z3 is a slightly faster solver today.

apw 13y ago
Is STP considered a qualitatively different kind of tool than Yices and Z3?
beambot 13y ago
Pardon the relative ignorance... but I thought these types of problems (SAT and SMT) were NP-Complete in the general case? Does Z3 do something special (eg apply heuristics)? It looks very impressive!
- dons 13y ago
  http://www.csl.sri.com/users/rushby/slides/jaist07.pdf http://www.csl.sri.com/users/rushby/slides/jaist07.pdf See "SMT Solvers: Disruptive Innovation in Theorem Proving", Rushby, 2007. > SAT solving is the quintessential NP-complete problem. But now amazingly fast in practice (most of the time) > SMT ... generalizes SAT solving by adding the ability to handle arithmetic and other decidable theories
- jcd748 13y ago
  SAT is NP-complete, but there are certain properties that allow theorem provers to show that a particular instance is overconstrained (and therefore unsatisfiable), or underconstrained (and many solutions exist). It's at a particular point, so-called phase transitions, where one finds the very hard instances. As an example, when characterizing 3-SAT instances by grouping by their ratio of clauses to variables, the very hard instances are grouped around a value of ~4.3.
- microarchitect 13y ago
  Although SAT is indeed NP-complete, modern solvers are ridiculously fast for the kinds of SAT queries that appear in scenarios like hardware model checking and verification. It's not uncommon for queries with millions of variables and clauses to be solved in a matter of seconds. There are some algorithmic tricks combined with clever data structures and search space exploration heuristics that make this possible. btw, if you're curious about the workings of a modern SAT solver, the first few sections of this paper: http://www.georg.weissenbacher.name/papers/mod12.pdf http://www.georg.weissenbacher.name/papers/mod12.pdf should make interesting and hopefully accessible reading. Unfortunately, I don't know enough about the internals of Z3 to know what specifically makes it the fastest SMT solver. But I also don't think it's too far wrong to say that SMT solvers like Z3 are fast because the underlying SAT solver they use is very fast.

apw 13y ago

Is STP considered a qualitatively different kind of tool than Yices and Z3?

beambot 13y ago

Pardon the relative ignorance... but I thought these types of problems (SAT and SMT) were NP-Complete in the general case? Does Z3 do something special (eg apply heuristics)? It looks very impressive!

dons 13y ago
http://www.csl.sri.com/users/rushby/slides/jaist07.pdf http://www.csl.sri.com/users/rushby/slides/jaist07.pdf See "SMT Solvers: Disruptive Innovation in Theorem Proving", Rushby, 2007. > SAT solving is the quintessential NP-complete problem. But now amazingly fast in practice (most of the time) > SMT ... generalizes SAT solving by adding the ability to handle arithmetic and other decidable theories
jcd748 13y ago
SAT is NP-complete, but there are certain properties that allow theorem provers to show that a particular instance is overconstrained (and therefore unsatisfiable), or underconstrained (and many solutions exist). It's at a particular point, so-called phase transitions, where one finds the very hard instances. As an example, when characterizing 3-SAT instances by grouping by their ratio of clauses to variables, the very hard instances are grouped around a value of ~4.3.
microarchitect 13y ago
Although SAT is indeed NP-complete, modern solvers are ridiculously fast for the kinds of SAT queries that appear in scenarios like hardware model checking and verification. It's not uncommon for queries with millions of variables and clauses to be solved in a matter of seconds. There are some algorithmic tricks combined with clever data structures and search space exploration heuristics that make this possible. btw, if you're curious about the workings of a modern SAT solver, the first few sections of this paper: http://www.georg.weissenbacher.name/papers/mod12.pdf http://www.georg.weissenbacher.name/papers/mod12.pdf should make interesting and hopefully accessible reading. Unfortunately, I don't know enough about the internals of Z3 to know what specifically makes it the fastest SMT solver. But I also don't think it's too far wrong to say that SMT solvers like Z3 are fast because the underlying SAT solver they use is very fast.