CAQE: a certifying QBF solver. We present a new CEGAR-based algorithm for QBF. The algorithm builds on a decomposition of QBFs into a sequence of propositional formulas, which we call the clausal abstraction. Each of the propositional formulas contains the variables of just one quantifier level and additional variables describing the interaction with adjacent quantifier levels. This decomposition leads to a simpler notion of refinement compared to earlier approaches. We also show how to effectively construct Skolem and Herbrand functions from true, respectively false, QBFs; allowing us to certify the solver result. We implemented the algorithm in a solver called CAQE. The experimental evaluation shows that CAQE has competitive performance compared to current QBF solvers and outperforms previous certifying solvers.

References in zbMATH (referenced in 16 articles )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Akshay, S.; Chakraborty, Supratik; Goel, Shubham; Kulal, Sumith; Shah, Shetal: Boolean functional synthesis: hardness and practical algorithms (2021)
  2. Beyersdorff, Olaf; Blinkhorn, Joshua; Mahajan, Meena: Building strategies into QBF proofs (2021)
  3. Bloem, Roderick; Braud-Santoni, Nicolas; Hadzic, Vedad; Egly, Uwe; Lonsing, Florian; Seidl, Martina: Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations (2021)
  4. Fandinno, Jorge; Laferriere, Francois; Romero, Javier; Schaub, Torsten; Son, Tran Cao: Planning with incomplete information in quantified answer set programming (2021)
  5. Mengel, Stefan; Slivovsky, Friedrich: Proof complexity of symbolic QBF reasoning (2021)
  6. Schlaipfer, Matthias; Slivovsky, Friedrich; Weissenbacher, Georg; Zuleger, Florian: Multi-linear strategy extraction for QBF expansion proofs via local soundness (2020)
  7. Barichard, Vincent; Stéphan, Igor: Quantified constraint handling rules (2019)
  8. Pulina, Luca; Seidl, Martina: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17) (2019)
  9. Lonsing, Florian; Egly, Uwe: (\textsfQRAT^+): generalizing QRAT by a more powerful QBF redundancy property (2018)
  10. Mahajan, Meena: Lower bound techniques for QBF proof systems (2018)
  11. Faymonville, Peter; Finkbeiner, Bernd; Rabe, Markus N.; Tentrup, Leander: Encodings of bounded synthesis (2017)
  12. Peitl, Tomáš; Slivovsky, Friedrich; Szeider, Stefan: Dependency learning for QBF (2017)
  13. Lonsing, Florian; Egly, Uwe; Seidl, Martina: Q-resolution with generalized axioms (2016)
  14. Rabe, Markus N.; Seshia, Sanjit A.: Incremental determinization (2016)
  15. Tentrup, Leander: Non-prenex QBF solving using abstraction (2016)
  16. Wimmer, Karina; Wimmer, Ralf; Scholl, Christoph; Becker, Bernd: Skolem functions for DQBF (2016)