Document Open Access Logo

Models and Counter-Models of Quantified Boolean Formulas (Invited Talk)

Author Martina Seidl

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.1.pdf
  • Filesize: 490 kB
  • 7 pages

Document Identifiers

Author Details

Martina Seidl
  • Johannes Kepler University Linz, Austria

Funding

Parts of this work were supported by the LIT AI Lab founded by the State of Upper Austria.

Cite AsGet BibTex

Martina Seidl. Models and Counter-Models of Quantified Boolean Formulas (Invited Talk). In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 1:1-1:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.1

Abstract

Because of the duality of universal and existential quantification, quantified Boolean formulas (QBF), the extension of propositional logic with quantifiers over the Boolean variables, have not only solutions in terms of models for true formulas like in SAT. Also false QBFs have solutions in terms of counter-models. Both models and counter-models can be represented as certain binary trees or as sets of Boolean functions reflecting the dependencies among the variables of a formula. Such solutions encode the answers to application problems for which QBF solvers are employed like the plan for a planning problem or the error trace of a verification problem. Therefore, models and counter-models are at the core of theory and practice of QBF solving. In this invited talk, we survey approaches that deal with models and counter-models of QBFs and identify some open challenges.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Quantified Boolean Formula
  • Solution Extraction
  • Solution Counting

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods Syst. Des., 41(1):45-65, 2012. URL: https://doi.org/10.1007/S10703-012-0152-6.
  2. Valeriy Balabanov, Jie-Hong Roland Jiang, Mikolas Janota, and Magdalena Widl. Efficient extraction of QBF (counter)models from long-distance resolution proofs. In Blai Bonet and Sven Koenig, editors, Proc. of the 29th AAAI Conference on Artificial Intelligence, pages 3694-3701. AAAI Press, 2015. Google Scholar
  3. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In Carsten Sinz and Uwe Egly, editors, Proc. of the 17th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2014), volume 8561 of Lecture Notes in Computer Science, pages 154-169. Springer, 2014. Google Scholar
  4. Bernd Becker, Rüdiger Ehlers, Matthew Lewis, and Paolo Marin. ALLQBF Solving by Computational Learning. In Proc. of the 10th Int. Conf. on Automated Technology for Verification and Analysis (ATVA), volume 7561 of LNCS, pages 370-384. Springer, 2012. Google Scholar
  5. Marco Benedetti. skizzo: A suite to evaluate and certify qbfs. In Robert Nieuwenhuis, editor, Proc. of the 20th Int. Conf. on Automated Deduction (CADE-20), volume 3632 of Lecture Notes in Computer Science, pages 369-376. Springer, 2005. Google Scholar
  6. Olaf Beyersdorff. Proof Complexity of Quantified Boolean Logic - A Survey, chapter Chapter 15, pages 397-440. World Scientific, 2023. Google Scholar
  7. Olaf Beyersdorff, Leroy Chew, and Mikolas Janota. On unification of QBF resolution-based calculi. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Proc. of the 39th Int. Symposium on Mathematical Foundations of Computer Science (MFCS 2014), volume 8635 of Lecture Notes in Computer Science, pages 81-93. Springer, 2014. Google Scholar
  8. Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, and Martina Seidl. Quantified boolean formulas. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1177-1221. IOS Press, 2021. Google Scholar
  9. Roderick Bloem, Robert Könighofer, and Martina Seidl. Sat-based synthesis methods for safety specs. In Kenneth L. McMillan and Xavier Rival, editors, Proc. of the 15th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014), volume 8318 of Lecture Notes in Computer Science, pages 1-20. Springer, 2014. Google Scholar
  10. Florent Capelli, Jean-Marie Lagniez, Andreas Plank, and Martina Seidl. A top-down tree model counter for quantified boolean formulas. In Accepted for IJCAI 2024, 2024. Google Scholar
  11. Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, and Armin Biere. Skolem function continuation for quantified boolean formulas. In Sebastian Gabmeyer and Einar Broch Johnsen, editors, Proc. of the 11th Int. Conf. on Tests and Proofs (TAP 2017), volume 10375 of Lecture Notes in Computer Science, pages 129-138. Springer, 2017. Google Scholar
  12. Alexandra Goultiaeva, Allen Van Gelder, and Fahiem Bacchus. A uniform approach for generating proofs and strategies for both true and false QBF formulas. In Toby Walsh, editor, Proc. of the 22nd Int. Joint Conf. on Artificial Intelligence (IJCAI 2011), pages 546-553. IJCAI/AAAI, 2011. Google Scholar
  13. Vedad Hadzic, Roderick Bloem, Ankit Shukla, and Martina Seidl. Ferpmodels: A certification framework for expansion-based QBF solving. In Bruno Buchberger, Mircea Marin, Viorel Negru, and Daniela Zaharie, editors, Proc. of the 24th Int. Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2022), pages 80-83. IEEE, 2022. Google Scholar
  14. Maximilian Heisinger, Martina Seidl, and Armin Biere. Paraqooba: A fast and flexible framework for parallel and distributed QBF solving. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Proc. of the 29th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), volume 13993 of Lecture Notes in Computer Science, pages 426-447. Springer, 2023. Google Scholar
  15. Marijn J. H. Heule, Martina Seidl, and Armin Biere. Solution validation and extraction for QBF preprocessing. J. Autom. Reason., 58(1):97-125, 2017. Google Scholar
  16. Mikolás Janota. Towards generalization in QBF solving via machine learning. In Sheila A. McIlraith and Kilian Q. Weinberger, editors, Proc. of the 32nd AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), pages 6607-6614. AAAI Press, 2018. Google Scholar
  17. Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, and Christoph M. Wintersteiger. A first step towards a unified proof checker for QBF. In João Marques-Silva and Karem A. Sakallah, editors, Proc. of the 10th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2007), volume 4501 of Lecture Notes in Computer Science, pages 201-214. Springer, 2007. Google Scholar
  18. Manuel Kauers and Martina Seidl. Symmetries of quantified boolean formulas. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Proc. of the 21st Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2018), volume 10929 of Lecture Notes in Computer Science, pages 199-216. Springer, 2018. Google Scholar
  19. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified boolean formulas. Inf. Comput., 117(1):12-18, 1995. Google Scholar
  20. Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, and Martina Seidl. Enhancing search-based QBF solving by dynamic blocked clause elimination. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Proc. of the 20th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), volume 9450 of Lecture Notes in Computer Science, pages 418-433. Springer, 2015. Google Scholar
  21. Florian Lonsing and Uwe Egly. Depqbf 6.0: A search-based QBF solver beyond traditional QCDCL. In Leonardo de Moura, editor, Proc. of the 26th Int. Conf. on Automated Deduction (CADE 26), volume 10395 of Lecture Notes in Computer Science, pages 371-384. Springer, 2017. Google Scholar
  22. Florian Lonsing, Uwe Egly, and Martina Seidl. Q-resolution with generalized axioms. In Nadia Creignou and Daniel Le Berre, editors, Proc. of the 19th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2016), volume 9710 of Lecture Notes in Computer Science, pages 435-452. Springer, 2016. Google Scholar
  23. Florian Lonsing and Martina Seidl. Parallel solving of quantified boolean formulas. In Youssef Hamadi and Lakhdar Sais, editors, Handbook of Parallel Constraint Reasoning, pages 101-139. Springer, 2018. Google Scholar
  24. Florian Lonsing, Martina Seidl, and Allen Van Gelder. The QBF gallery: Behind the scenes. Artif. Intell., 237:92-114, 2016. Google Scholar
  25. João Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 133-182. IOS Press, 2021. Google Scholar
  26. Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, and Armin Biere. Resolution-based certificate extraction for QBF - (tool presentation). In Alessandro Cimatti and Roberto Sebastiani, editors, Proc. of the 15th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2012), volume 7317 of Lecture Notes in Computer Science, pages 430-435. Springer, 2012. Google Scholar
  27. Andreas Plank, Sibylle Möhle, and Martina Seidl. Enumerative level-2 solution counting for quantified boolean formulas (short paper). In Proc. of the 29th Int. Conf. on Principles and Practice of Constraint (CP), volume 280 of LIPIcs, pages 49:1-49:10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  28. Luca Pulina and Martina Seidl. The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17). Artif. Intell., 274:224-248, 2019. Google Scholar
  29. Markus N. Rabe and Sanjit A. Seshia. Incremental determinization. In Nadia Creignou and Daniel Le Berre, editors, Proc. of the 19th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2016), volume 9710 of Lecture Notes in Computer Science, pages 375-392. Springer, 2016. Google Scholar
  30. Irfansha Shaik, Maximilian Heisinger, Martina Seidl, and Jaco van de Pol. Validation of QBF encodings with winning strategies. In Meena Mahajan and Friedrich Slivovsky, editors, Proc. of the 26th Int. Conf. on Theory and Applications of Satisfiability (SAT 2023), volume 271 of LIPIcs, pages 24:1-24:10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  31. Irfansha Shaik and Jaco van de Pol. Classical planning as QBF without grounding. In Akshat Kumar, Sylvie Thiébaux, Pradeep Varakantham, and William Yeoh, editors, Proc. of the 32nd Int. Conf. on Automated Planning and Scheduling (ICAPS 2022), pages 329-337. AAAI Press, 2022. Google Scholar
  32. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified boolean formulas. In Proc. of the 31st IEEE Int. Conf. on Tools with Artificial Intelligence (ICTAI 2019), pages 78-84. IEEE, 2019. Google Scholar
  33. Ankit Shukla, Sibylle Möhle, Manuel Kauers, and Martina Seidl. Outercount: A first-level solution-counter for quantified boolean formulas. In Proc. of the 15th Int. Conf on Intelligent Computer Mathematics (CICM 2022), volume 13467 of Lecture Notes in Computer Science, pages 272-284. Springer, 2022. Google Scholar
  34. Leander Tentrup. CAQE and quabs: Abstraction based QBF solvers. J. Satisf. Boolean Model. Comput., 11(1):155-210, 2019. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact