<p>Since your integer variables are from a finite domain, you could &quot;bit-blast&quot; to SAT, then use a <a href="https://cstheory.stackexchange.com/questions/11022/checking-formulas-with-two-quantifiers-forall-exists-2qbf?noredirect=1&amp;lq=1">2QBF solver</a>.</p>
<p>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.</p>
<hr />
<p>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 <span class="math-container">$\exists x \forall y \varphi$</span>:</p>
<ol>
<li><p>Let <span class="math-container">$b_1,\dots,b_n$</span> be some values.</p>
</li>
<li><p>Testing the satisfiability of <span class="math-container">$\varphi[b_1/y] \land \dots \land \varphi[b_n/y]$</span>.  If this is not satisfiable, then you can terminate, as it implies that <span class="math-container">$\exists x \forall y \varphi$</span> is not satisfiable.  If it is satisfiable, suppose it is satisfied by <span class="math-container">$x=a$</span>.</p>
</li>
<li><p>Then try to satisfy <span class="math-container">$\neg \varphi[a/x]$</span>.  If it cannot be satisfied, then you can terminate, as it implies that <span class="math-container">$\exists x \forall y \varphi$</span> is satisfiable with <span class="math-container">$x=a$</span>.  If it can be satisfied, say by <span class="math-container">$y=b$</span>, let <span class="math-container">$b_{n+1}=b$</span>, increment <span class="math-container">$n$</span>, and go back to step 2.</p>
</li>
</ol>
<p>You could implement each of these steps in Z3, and this would take advantage of Z3's SMT theories, without requiring you to &quot;bit-blast&quot; 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.</p>

CC BY-SA 4.0
2021-03-31T18:14:27.917Z
2021-04-01T06:51:42.577Z
2021-04-01T06:51:42.577Z
D.W.
<p>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
<span class="math-container">$$\exists x \forall y ((y \ge 1 \land y \le 2) \implies ((\neg x)\land(y * y \ge 1)).$$</span></p>
<p>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?</p>
<p><a href="https://cstheory.stackexchange.com/questions/11022/checking-formulas-with-two-quantifiers-forall-exists-2qbf">This question</a> describes tools for 2QBF, but 2QBF only supports SAT formulas (i.e., only supports Boolean variables). The formulas in my question include integer variables.</p>

CC BY-SA 4.0
2021-03-31T07:55:47.950Z
Does this answer your question? [Checking formulas with two quantifiers ($\forall \exists$) - 2QBF](https://cstheory.stackexchange.com/questions/11022/checking-formulas-with-two-quantifiers-forall-exists-2qbf)
D.W.
CC BY-SA 4.0
2021-03-31T11:24:24.570Z
@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.
Giang Trinh
CC BY-SA 4.0
2021-03-31T18:07:32.260Z
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 https://cs.meta.stackexchange.com/q/657/755.
D.W.
CC BY-SA 4.0
2021-03-31T18:08:13.223Z
Note that you can use LaTeX here to typeset mathematics in a more readable way. See [here](https://cs.meta.stackexchange.com/questions/271/add-short-reference-for-latex-commands) for a short introduction.
D.W.
CC BY-SA 4.0
2021-04-01T06:38:00.690Z
@D.W. I see. Thank you for the useful guidance.
Giang Trinh
CC BY-SA 4.0
2021-04-01T06:51:53.343Z
See my edited answer for another possible approach.
D.W.
<ds.algorithms><sat><heuristics>
Efficient tools for checking SMT formulas with two quantifiers ($\exists\forall$)
Giang Trinh
# Efficient tools for checking SMT formulas with two quantifiers ($\exists\forall$)

(Asked by: username_0 on 2021-03-29)

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](https://cstheory.stackexchange.com/questions/11022/checking-formulas-with-two-quantifiers-forall-exists-2qbf) describes tools for 2QBF, but 2QBF only supports SAT formulas (i.e., only supports Boolean variables). The formulas in my question include integer variables.

**Tags:** ds.algorithms, sat, heuristics
> **Comments:**
> **username_1**: Does this answer your question? [Checking formulas with two quantifiers ($\forall \exists$) - 2QBF](https://cstheory.stackexchange.com/questions/11022/checking-formulas-with-two-quantifiers-forall-exists-2qbf)  
> **username_0**: @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.  
> **username_1**: 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 https://cs.meta.stackexchange.com/q/657/755.  
> **username_1**: Note that you can use LaTeX here to typeset mathematics in a more readable way. See [here](https://cs.meta.stackexchange.com/questions/271/add-short-reference-for-latex-commands) for a short introduction.  
> **username_0**: @D.W. I see. Thank you for the useful guidance.  
> **username_1**: See my edited answer for another possible approach.  

---

## 1 answers

### Answer by username_1 on 2021-03-31. Score: 0 | Accepted answer

Since your integer variables are from a finite domain, you could "bit-blast" to SAT, then use a [2QBF solver](https://cstheory.stackexchange.com/questions/11022/checking-formulas-with-two-quantifiers-forall-exists-2qbf?noredirect=1&lq=1).

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.


---

