14
$\begingroup$

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).

Improve this question
$\endgroup$
6
  • 4
    $\begingroup$ $\forall x \exists y \ \psi(x,y)$ is not essentially equivalent to $\exists x \forall y \ \psi(x,y)$. $\endgroup$
    – Huck Bennett
    Apr 8, 2012 at 2:43
  • 2
    $\begingroup$ 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 $\endgroup$
    – Suresh Venkat
    Apr 8, 2012 at 2:53
  • 1
    $\begingroup$ @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. $\endgroup$
    – D.W.
    Apr 8, 2012 at 3:22
  • 6
    $\begingroup$ @D.W., not necessarily, e.g. SAT and TAUT are not believed to have the same complexity. $\endgroup$
    – Kaveh
    Apr 8, 2012 at 5:46
  • 4
    $\begingroup$ @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 qbflib.org $\endgroup$
    – Huck Bennett
    Apr 8, 2012 at 19:06

3 Answers 3

Reset to default
22
$\begingroup$

If I may, quite blatantly, advertise myself, we wrote an article about this last year Abstraction-Based Algorithm for 2QBF. 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, which also presents fairly easily implemetable algorithms.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Awesome! Thanks, Mikolas, this is just the sort of thing I was hoping for. $\endgroup$
    – D.W.
    Apr 9, 2012 at 1:54
  • 2
    $\begingroup$ 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. $\endgroup$
    – Mikolas
    Apr 9, 2012 at 19:09
7
$\begingroup$

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

Incremental Determinization, Markus N. Rabe and Sanjit Seshia, Theory and Applications of Satisfiability Testing (SAT 2016).

They have implemented their algorithm in a tool named 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, Florian Lonsing and Uwe Egly.

Implemented in a tool named 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 for the results of yearly QBF competition QBFEVAL. 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).

Improve this answer
$\endgroup$
0
4
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ This is the algorithm described in the paper that Mikolas cites; 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! $\endgroup$
    – D.W.
    Nov 15, 2017 at 7:05
  • $\begingroup$ 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 $\endgroup$
    – Samuel Schlesinger
    Nov 15, 2017 at 8:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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