The Trouble with Quantifier Instantiation in an SMT Solver? Triggers.

Tuesday, June 22nd, 2010

So, i’ve been recently working through the quantifier instantiation mechanism in wyone. This is a tricky, yet important topic. There’s been a lot of interesting research in this area as well (see further reading below for some examples), although I found the papers often hard work at times.

Anyway, the basic idea is pretty straightforward. Let’s imagine we’re testing the following formula for satisfiability:

in(x,xs) && x < 0 && forall Y [ in(Y,xs) ==> Y >= 0 ]

In this formula, the forall expression enforces a constraint that every element in the “collection” xs must be positive. On the other hand, we have a variable x which is known to be in xs, and is negative. Therefore, we can easily see that there is a contradiction here. But, how does the SMT solver show this? The answer is through quantifier instantiation. To do this, it constructs a binding from quantified variables to ground literals (or possibly ground formulas). Once a suitable binding is found, it instantiates the quantifier. For our example, a good binding would be [Y->x] and using this to instantiate our quantifier gives:

in(x,xs) && x < 0 && forall Y [ in(Y,xs) ==> Y >= 0 ]
=> && in(x,xs) ==> x >= 0
=> && x >= 0

At this point, the arithmetic theory of the SMT solver will kick in and immediately derive a contradiction from x<0 && x>=0.

The difficulty in this process stems from the problem of finding a good binding. A lot of work in this area has been done, particularly with systems like Prolog which use unification. Modern SMT solvers usually rely on so-called triggers to generate the binding. A trigger is essentially just a pattern match which generates bindings. In our example, you could trigger on in(X,Y) literals: when you saw one in a quantified formula, you’d try and generate a binding by looking at all existing ground instances of it. In our example, that would lead to unifying in(x,xs) against in(Y,xs) and that would generate the required binding.

This approach to quantification has numerous drawbacks. First and foremost, it can be very expensive to determine a binding as this requires a potentially exponential search through all possible trigger matches. Secondly, the problem arises when the SMT solver doesn’t use the exact trigger you need to get the contradiction. This is particularly likely to happen when the formula involves triggering on arithmetic expressions. For example:

f(x-1,x) && !g(x-1,x) && forall X,Y [ f(X,X+Y) ==> g(X,X+Y) ]

(Ok, this is a slightly artificial example, but it makes the point)

The challenge here is to obtain the binding [X->x-1, Y->1] which will lead us to the contradiction. Certainly, this is possible … but the problem of unification is suddenly much harder as we must be prepared to make complex expression rewrites during unification. At some point, the SMT solver may give up searching for matches, and you’ll be forced to write formulas in a way that helps it find them.

Anyway, that’s all for now. But, I’d be quite interested to know how far existing solvers like Z3 or Simplify go in this department …

The Trouble with Quantifier Instantiation in an SMT Solver? Triggers.

Further Reading