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?

Mosaic

see also Computer Science or even Theoretical Computer Science – Koran

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).

Pod

Could you please elaborate more about why the given QF BV example will be difficult for SMT solvers? If possible, can you also show an intuition of such problems in general. Any references on this matter are also highly appreciated. Thanks. – Asphyxiate

@Asphyxiate We can discuss this in chat. – Pod

In run(), I think you might mean assert(a*b != <some large number>); or if (a*b == <some large number>) assert(false);. a*b is not a l-value; it cannot be assigned to. If this is what you meant, a SMT solver can't easily prove that assert(false); will occur: it'll first have to demonstrate that the large number is composite. Anyway, you might want to edit the answer to fix the definition of run(). – Yellowbird

Hi @D.W., been a long time. Yeah it is pseudocode, but assuming a c-like language, you are correct. In SMT languages, you simply make logical statements, so it made more sense the way I wrote it, at the time. – Pod

I'm not convinced by this statement: "SMT solvers are not any more powerful than SAT solvers." - I assume you mean that any problem solvable by an SMT solver could be encoded as a SAT problem. This is obviously true for fixed BV problems but parametric BV, no-linear arithmetic, strings, quantifiers? – Veneer

@Veneer Edit it with a more accurate answer. – Pod