<p>If I may, quite blatantly, advertise myself, we wrote an article about this last year
<a href="http://scholar.google.com/citations?view_op=view_citation&amp;hl=en&amp;user=SFg4raQAAAAJ&amp;citation_for_view=SFg4raQAAAAJ%3aeQOLeE2rZwMC">Abstraction-Based Algorithm for 2QBF</a>. I've got an implementation for qdimacs, which I can provide if you wish but from my experience, one can benefit greatly from specializing the algorithm for a particular problem. There is also an older paper <a href="http://www.satisfiability.org/SAT04/programme/113.pdf">A Comparative Study of 2QBF Algorithms</a>, which also presents fairly easily implemetable algorithms.</p>

CC BY-SA 3.0
2012-04-09T01:54:39.713Z
Awesome!  Thanks, Mikolas, this is just the sort of thing I was hoping for.
D.W.
CC BY-SA 3.0
2012-04-09T19:09:38.913Z
Hi @D.W. glad I could help. Hopefully you'll find some of this useful. QBF is quite a different beast that SAT so one has to be a little careful because things can blow up very easily :-). Feel free to write me an e-mail if you have any more detailed questions about our work.
Mikolas
CC BY-SA 3.0
2012-04-08T20:36:57.250Z
2012-04-08T20:36:57.250Z
Mikolas
<p>I have read two papers related to this, one specifically related to 2QBF.  The papers are the following: </p>

<p><a href="https://link.springer.com/chapter/10.1007/978-3-319-40970-2_23" rel="nofollow noreferrer">Incremental Determinization</a>, Markus N. Rabe and Sanjit Seshia, Theory and Applications of Satisfiability Testing (SAT 2016).</p>

<p>They have implemented their algorithm in a tool named <a href="https://github.com/MarkusRabe/cadet" rel="nofollow noreferrer">CADET</a>. The basic idea is to incrementally add new constraints to the formula till constraints describes a unique Skolem function or until there absence is confirmed.  </p>

<p>Second one is <a href="http://arxiv.org/pdf/1402.2410.pdf" rel="nofollow noreferrer">Incremental QBF Solving</a>, Florian Lonsing and Uwe Egly.</p>

<p>Implemented in a tool named <a href="https://github.com/lonsing/depqbf" rel="nofollow noreferrer">DepQBF</a>. It do not put any constraint over the number of quantifier alternation. It begins with the assumption that we have a closely related qbf formulas. It's based on incremental solving and do not throw the clauses learned during last solving. It add clauses and cubes to the current formula and stops either if clauses or cubes are empty, representing unsat or sat.</p>

<p><strong>Edit</strong>: Just for a perspective how well these approaches work for 2QBF-benchmarks. Please look at the <a href="http://www.qbflib.org/main.pdf" rel="nofollow noreferrer">Results of QBFEVal-2018</a> for the results of yearly QBF competition <a href="http://www.qbflib.org/index_eval.php" rel="nofollow noreferrer">QBFEVAL</a>. In 2019 there was no 2QBF track. </p>

<blockquote>
  <p>In <strong>2QBF Track</strong> QBFEVAL-2018 <strong>DepQBF</strong> <strong>was the winner</strong>, <strong>CADET</strong> was the <strong>second</strong> in the race. </p>
</blockquote>

<p>So these two approaches actually works very well in practice (at least on the QBFEVAL benchmarks).  </p>

CC BY-SA 4.0
2017-11-14T13:42:08.660Z
2020-01-01T18:42:05.073Z
2020-01-01T18:42:05.073Z
Pushpa
<p>To show satisfiability of $\exists x \forall y \phi$, we can play a game with two players A and B who each have access to a SAT solver. If we're working in a domain $D$, then at each iteration (including the first) A chooses an element which satisfies the constraint set it has (it starts empty), $a \in D$, as our candidate to satisfy the formula. Then, B tries to satisfy $\neg \phi[a/x]$ with some $b \in B$. If B cannot do this, this means that $a$ works and we're done, otherwise we go back to A and we add to its constraint set $\phi [b/y]$, which guarantees this sort of mistake will not be made again. I have a feeling that one could think about the form of $\phi$ and do this sort of a procedure in a more strategic way, relying upon some sufficient subsets to eliminate any given candidate or some known symmetries to eliminate parts of this search early. Perhaps one might even add their own constraints to the initial constraint set of A.</p>

CC BY-SA 3.0
2017-11-15T07:05:44.640Z
This is the algorithm described in the paper that [Mikolas cites](https://cstheory.stackexchange.com/a/11028/5038); see Algorithm 1 of that paper.  If $\phi$ is provided as the negation of a CNF formula, they then show some ways to further improve the algorithm by taking into account the form of $\phi$ (as your answer suggests might be possible); see Section 5 of that paper. Nice explanation of an elegant and powerful approach!
D.W.
CC BY-SA 3.0
2017-11-15T08:01:26.897Z
It's quite nice, there is an analogy with adversarial machine learning if you squint at and indeed it works for any complemented lattice where you have a solver of sorts
Samuel Schlesinger
CC BY-SA 3.0
2017-11-14T18:11:18.547Z
2017-11-15T06:53:40.927Z
2017-11-15T06:53:40.927Z
Samuel Schlesinger
<p>SAT solvers give a powerful way to check the validity of a boolean formula with one quantifier.</p>

<p>For instance, to check the validity of $\exists x . \varphi(x)$, we can use a SAT solver to determine whether $\varphi(x)$ is satisfiable.  To check the validity of $\forall x . \varphi(x)$, we can use a SAT solver to determine whether $\neg \varphi(x)$ is satisfiable.  (Here $x=(x_1,\dots,x_n)$ is a $n$-vector of boolean variables, and $\varphi$ is a boolean formula.)</p>

<p>QBF solvers are designed to check the validity of a boolean formula with an arbitrary number of quantifiers.</p>

<p>What if we have a formula with two quantifiers?  Are they any efficient algorithms for checking validity: ones  that are better than just using generic algorithms for QBF?  To be more specific I have a formula of the form $\forall x . \exists y . \psi(x,y)$ (or $\exists x . \forall y . \psi(x,y)$), and want to check its validity.  Are there any good algorithms for this?  <strong>Edit 4/8:</strong> I learned that this class of formulas is sometimes known as 2QBF, so I am looking for good algorithms for 2QBF.</p>

<p>Specializing further: In my particular case, I have a formula of the form $\forall x . \exists y . f(x)=g(y)$ whose validity I want to check, where $f,g$ are functions that produce a $k$-bit output.  Are there any algorithms for checking the validity of this particular sort of formula, more efficiently than generic algorithms for QBF?</p>

<p>P.S. I am not asking about the worst-case hardness, in complexity theory.  I am  asking about practically useful algorithms (much as modern SAT solvers are practically useful on many problems even though SAT is NP-complete).</p>

CC BY-SA 3.0
2012-04-08T02:43:30.660Z
$\forall x \exists y \  \psi(x,y)$ is not essentially equivalent to $\exists x \forall y \  \psi(x,y)$.
Huck Bennett
CC BY-SA 3.0
2012-04-08T02:53:51.130Z
I think the OP means this informally, in that they're both difficult for SAT solvers and that an solution to either would be interesting
Suresh Venkat
CC BY-SA 3.0
2012-04-08T03:22:42.847Z
@HuckBennett, I think the two have equivalent hardness. (Proof: $\exists x . \forall y . \psi(x,y)$ is valid iff $\neg \forall x . \exists y . \neg \psi(x,y)$ is.  Therefore, if we have a way to test validity of formulas of the form $\forall x . \exists y . \psi(x,y)$, we can also test validity of formulas $\exists x . \forall y . \psi(x,y)$  by letting $\psi'(x,y) = \neg \psi(x,y)$ and testing the validity of $\forall x . \exists y . \psi'(x,y)$.)  But anyway, I would be interested in algorithms for either case.
D.W.
CC BY-SA 3.0
2012-04-08T05:46:50.320Z
@D.W., not necessarily, e.g. SAT and TAUT are not believed to have the same complexity.
Kaveh
CC BY-SA 3.0
2012-04-08T14:13:55.837Z
I found this relevant question: http://stackoverflow.com/questions/3739248/reducing-planning-to-quantified-boolean-formulae . Since we would expect an algorithm to receive input with an unbounded number of quantifiers and since there is no easy exploit for certain number of quantifiers (at least I am not aware of it), a TQBF solver would be closer to what you would need. From the discussion, it seems that a few, if any, exist.
chazisop
CC BY-SA 3.0
2012-04-08T19:06:17.420Z
@chazisop: I think the OP is asking for $\Pi_2/\Sigma_2$-SAT algorithms/solvers, not general QBF solvers. However plenty of QBF solvers do exist. See the "solvers" tab at http://www.qbflib.org/
Huck Bennett
<ds.algorithms><lo.logic><sat><boolean-functions>
Checking formulas with two quantifiers ($\forall \exists$) - 2QBF
D.W.
# Checking formulas with two quantifiers ($\forall \exists$) - 2QBF

(Asked by: username_0 on 2012-04-08)

SAT solvers give a powerful way to check the validity of a boolean formula with one quantifier.

For instance, to check the validity of $\exists x . \varphi(x)$, we can use a SAT solver to determine whether $\varphi(x)$ is satisfiable. To check the validity of $\forall x . \varphi(x)$, we can use a SAT solver to determine whether $\neg \varphi(x)$ is satisfiable. (Here $x=(x\_1,\dots,x\_n)$ is a $n$-vector of boolean variables, and $\varphi$ is a boolean formula.)

QBF solvers are designed to check the validity of a boolean formula with an arbitrary number of quantifiers.

What if we have a formula with two quantifiers? Are they any efficient algorithms for checking validity: ones that are better than just using generic algorithms for QBF? To be more specific I have a formula of the form $\forall x . \exists y . \psi(x,y)$ (or $\exists x . \forall y . \psi(x,y)$), and want to check its validity. Are there any good algorithms for this? **Edit 4/8:** I learned that this class of formulas is sometimes known as 2QBF, so I am looking for good algorithms for 2QBF.

Specializing further: In my particular case, I have a formula of the form $\forall x . \exists y . f(x)=g(y)$ whose validity I want to check, where $f,g$ are functions that produce a $k$-bit output. Are there any algorithms for checking the validity of this particular sort of formula, more efficiently than generic algorithms for QBF?

P.S. I am not asking about the worst-case hardness, in complexity theory. I am asking about practically useful algorithms (much as modern SAT solvers are practically useful on many problems even though SAT is NP-complete).

**Tags:** ds.algorithms, lo.logic, sat, boolean-functions
> **Comments:**
> **username_1**: $\forall x \exists y \  \psi(x,y)$ is not essentially equivalent to $\exists x \forall y \  \psi(x,y)$.  
> **username_2**: I think the OP means this informally, in that they're both difficult for SAT solvers and that an solution to either would be interesting  
> **username_0**: @HuckBennett, I think the two have equivalent hardness. (Proof: $\exists x . \forall y . \psi(x,y)$ is valid iff $\neg \forall x . \exists y . \neg \psi(x,y)$ is.  Therefore, if we have a way to test validity of formulas of the form $\forall x . \exists y . \psi(x,y)$, we can also test validity of formulas $\exists x . \forall y . \psi(x,y)$  by letting $\psi'(x,y) = \neg \psi(x,y)$ and testing the validity of $\forall x . \exists y . \psi'(x,y)$.)  But anyway, I would be interested in algorithms for either case.  
> **username_3**: @D.W., not necessarily, e.g. SAT and TAUT are not believed to have the same complexity.  
> **username_4**: I found this relevant question: http://stackoverflow.com/questions/3739248/reducing-planning-to-quantified-boolean-formulae . Since we would expect an algorithm to receive input with an unbounded number of quantifiers and since there is no easy exploit for certain number of quantifiers (at least I am not aware of it), a TQBF solver would be closer to what you would need. From the discussion, it seems that a few, if any, exist.  
> **username_1**: @chazisop: I think the OP is asking for $\Pi_2/\Sigma_2$-SAT algorithms/solvers, not general QBF solvers. However plenty of QBF solvers do exist. See the "solvers" tab at http://www.qbflib.org/  

---

## 3 answers

### Answer by username_5 on 2012-04-08. Score: 22

If I may, quite blatantly, advertise myself, we wrote an article about this last year
[Abstraction-Based Algorithm for 2QBF](http://scholar.google.com/citations?view_op=view_citation&hl=en&user=SFg4raQAAAAJ&citation_for_view=SFg4raQAAAAJ%3aeQOLeE2rZwMC). I've got an implementation for qdimacs, which I can provide if you wish but from my experience, one can benefit greatly from specializing the algorithm for a particular problem. There is also an older paper [A Comparative Study of 2QBF Algorithms](http://www.satisfiability.org/SAT04/programme/113.pdf), which also presents fairly easily implemetable algorithms.

> **Comments:**
> **username_0**: Awesome!  Thanks, Mikolas, this is just the sort of thing I was hoping for.  
> **username_5**: Hi @D.W. glad I could help. Hopefully you'll find some of this useful. QBF is quite a different beast that SAT so one has to be a little careful because things can blow up very easily :-). Feel free to write me an e-mail if you have any more detailed questions about our work.  

---

### Answer by username_6 on 2017-11-14. Score: 7

I have read two papers related to this, one specifically related to 2QBF. The papers are the following:

[Incremental Determinization](https://link.springer.com/chapter/10.1007/978-3-319-40970-2_23), Markus N. Rabe and Sanjit Seshia, Theory and Applications of Satisfiability Testing (SAT 2016).

They have implemented their algorithm in a tool named [CADET](https://github.com/MarkusRabe/cadet). The basic idea is to incrementally add new constraints to the formula till constraints describes a unique Skolem function or until there absence is confirmed.

Second one is [Incremental QBF Solving](http://arxiv.org/pdf/1402.2410.pdf), Florian Lonsing and Uwe Egly.

Implemented in a tool named [DepQBF](https://github.com/lonsing/depqbf). It do not put any constraint over the number of quantifier alternation. It begins with the assumption that we have a closely related qbf formulas. It's based on incremental solving and do not throw the clauses learned during last solving. It add clauses and cubes to the current formula and stops either if clauses or cubes are empty, representing unsat or sat.

**Edit**: Just for a perspective how well these approaches work for 2QBF-benchmarks. Please look at the [Results of QBFEVal-2018](http://www.qbflib.org/main.pdf) for the results of yearly QBF competition [QBFEVAL](http://www.qbflib.org/index_eval.php). In 2019 there was no 2QBF track.

> In **2QBF Track** QBFEVAL-2018 **DepQBF** **was the winner**, **CADET** was the **second** in the race.

So these two approaches actually works very well in practice (at least on the QBFEVAL benchmarks).


---

### Answer by username_7 on 2017-11-14. Score: 4

To show satisfiability of $\exists x \forall y \phi$, we can play a game with two players A and B who each have access to a SAT solver. If we're working in a domain $D$, then at each iteration (including the first) A chooses an element which satisfies the constraint set it has (it starts empty), $a \in D$, as our candidate to satisfy the formula. Then, B tries to satisfy $\neg \phi[a/x]$ with some $b \in B$. If B cannot do this, this means that $a$ works and we're done, otherwise we go back to A and we add to its constraint set $\phi [b/y]$, which guarantees this sort of mistake will not be made again. I have a feeling that one could think about the form of $\phi$ and do this sort of a procedure in a more strategic way, relying upon some sufficient subsets to eliminate any given candidate or some known symmetries to eliminate parts of this search early. Perhaps one might even add their own constraints to the initial constraint set of A.

> **Comments:**
> **username_0**: This is the algorithm described in the paper that [Mikolas cites](https://cstheory.stackexchange.com/a/11028/5038); see Algorithm 1 of that paper.  If $\phi$ is provided as the negation of a CNF formula, they then show some ways to further improve the algorithm by taking into account the form of $\phi$ (as your answer suggests might be possible); see Section 5 of that paper. Nice explanation of an elegant and powerful approach!  
> **username_7**: It's quite nice, there is an analogy with adversarial machine learning if you squint at and indeed it works for any complemented lattice where you have a solver of sorts  

---

