2
$\begingroup$

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.

$\endgroup$
6
  • 2
    $\begingroup$ Does this answer your question? Checking formulas with two quantifiers ($\forall \exists$) - 2QBF $\endgroup$
    – D.W.
    Mar 31 at 7:55
  • $\begingroup$ @D.W. Thank you. I have read this topic. However, the tools mentioned in this topic only support SAT formulas (i.e., only support Boolean variables). Formulas in my question include integer variables. $\endgroup$ Mar 31 at 11:24
  • $\begingroup$ Thanks. Please don't use "Edit."" Instead, revise the question so it reads well for someone who encounters it for the first time. No need to mark what has changed, we have built-in revision history. See cs.meta.stackexchange.com/q/657/755. $\endgroup$
    – D.W.
    Mar 31 at 18:07
  • $\begingroup$ Note that you can use LaTeX here to typeset mathematics in a more readable way. See here for a short introduction. $\endgroup$
    – D.W.
    Mar 31 at 18:08
  • 1
    $\begingroup$ See my edited answer for another possible approach. $\endgroup$
    – D.W.
    Apr 1 at 6:51
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.