Efficient tools for checking SMT formulas with two quantifiers ($\exists\forall$)

Question

I would like to check a sort of SMT formulas with two quantifiers where universal variables range over finite/bounded integer domains. An example formula is $$\exists x \forall y ((y \ge 1 \land y \le 2) \implies ((\neg x)\land(y * y \ge 1)).$$

I found that Z3 can handle the sort of formulas. However, the heuristics for handling quantifiers in Z3 seem not tuned for problems where universal variables range over finite/bounded domains. Are there any other efficient tools for checking the sort of formulas?

This question describes tools for 2QBF, but 2QBF only supports SAT formulas (i.e., only supports Boolean variables). The formulas in my question include integer variables.

Answer 1

Since your integer variables are from a finite domain, you could "bit-blast" to SAT, then use a 2QBF solver.

In other words, you translate formulas over these int variables into formulas over boolean variables, by building a boolean circuit to represent each of the operations (multiplication and comparison, in your example), and then using the Tseitin transform.

---

Another approach is to apply one of the methods for 2QBF to your problem directly. You'd have to implement this yourself. For example, here is a naive approach. Suppose your formula is $\exists x \forall y \varphi$:

1. Let $b_1,\dots,b_n$ be some values.

2. Testing the satisfiability of $\varphi[b_1/y] \land \dots \land \varphi[b_n/y]$. If this is not satisfiable, then you can terminate, as it implies that $\exists x \forall y \varphi$ is not satisfiable. If it is satisfiable, suppose it is satisfied by $x=a$.

3. Then try to satisfy $\neg \varphi[a/x]$. If it cannot be satisfied, then you can terminate, as it implies that $\exists x \forall y \varphi$ is satisfiable with $x=a$. If it can be satisfied, say by $y=b$, let $b_{n+1}=b$, increment $n$, and go back to step 2.

You could implement each of these steps in Z3, and this would take advantage of Z3's SMT theories, without requiring you to "bit-blast" to SAT. Note that in this procedure, you only invoke Z3 to test satisfiability of singly-quantified formulas; there are no nested quantifiers. You might even be able to use Z3's incremental solving abilities for better performance.