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 Theore

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