Limits of SMT solvers

Question

Traditionally most work with computational logic was either propositional, in which case you used a SAT (boolean satisfiability) solver, or first-order, in which case you used a first-order theorem prover.

In recent years, a lot of progress has been made on SMT (satisfiability modulo theory) solvers, which basically augment propositional logic with theories of arithmetic etc.; John Rushby of SRI International goes so far as to call them a disruptive technology.

What are the most important practical examples of problems that can be handled in first-order logic but still can't be handled by SMT? Most particularly, what sort of problems arise that can't be handled by SMT in the domain of software verification?

Answer 1

SMT solvers are not any more powerful than SAT solvers. They will still run in exponential time or be incomplete for the same problems in SAT. The advantage of SMT is that many things that are obvious in SMT can take a long time for an equivalent sat solver to rediscover.

So with software verification as an example, if you use a QF BV (quantifier-free theory of bit-vectors) SMT solver, the SMT solver will be aware that (a+b = b+a) on a word level instead, while it can take an SAT solver a really long time to prove that using the individual boolean values.

So wrt to software verification, you can easily make problems in software verification that would be hard for any SMT or SAT solver.

First, loops have to be unrolled in QF BV, which means that practically you must limit what the solver checks for. If quantifiers were allowed, it becomes a PSPACE-complete problem, not just NP-complete.

Second, problems that are considered hard in general are easy to encode in QF BV. For example, you can write a program as follows:

void run(int64_t a,int64_t b)
{
  a * b == <some large semiprime>;

  assert (false);
}

Now of course the SMT solver will easily prove that assert(false) will occur, but it will have to provide a counter example, which will give you the inputs a,b. If you set <some large number> to an RSA semiprime, then you just reversed multiplication ... otherwise known as integer factorization! Thus this will likely be hard for any SMT solver, and demonstrates that software verification is a hard problem in general (unless P=NP, or at least integer factorization becomes easy). Such SMT solvers are just a leg up on SAT solvers by dressing things up in an easier-to-write and easier-to-reason-with language.

SMT solvers that solve more advanced theories are necessarily incomplete or are even slower than SAT solvers, because they are attempting to solve harder problems.

See also:

• Interestingly, the Beaver SMT solver translates QF BV to CNF and can use an SAT solver as a back-end.
• Klee which can take a program compiled to LLVM IR (intermediate representation), and checks for bugs, and finds counter examples to assertions etc. If it finds a bug, it can give a counter-example to the correctness (it will give you input that will reproduce the bug).