Models and Counter-Models of Quantified Boolean Formulas (Invited Talk)
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.
Quantified Boolean Formula
Solution Extraction
Solution Counting
Theory of computation~Automated reasoning
1:1-1:7
Invited Talk
Parts of this work were supported by the LIT AI Lab founded by the State of Upper Austria.
Martina
Seidl
Martina Seidl
Johannes Kepler University Linz, Austria
https://orcid.org/0000-0002-3267-4494
10.4230/LIPIcs.SAT.2024.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.
https://doi.org/10.1007/S10703-012-0152-6
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.
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.
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.
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.
Olaf Beyersdorff. Proof Complexity of Quantified Boolean Logic - A Survey, chapter Chapter 15, pages 397-440. World Scientific, 2023.
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.
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.
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.
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.
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.
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.
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.
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.
Marijn J. H. Heule, Martina Seidl, and Armin Biere. Solution validation and extraction for QBF preprocessing. J. Autom. Reason., 58(1):97-125, 2017.
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.
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.
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.
Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified boolean formulas. Inf. Comput., 117(1):12-18, 1995.
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.
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.
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.
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.
Florian Lonsing, Martina Seidl, and Allen Van Gelder. The QBF gallery: Behind the scenes. Artif. Intell., 237:92-114, 2016.
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.
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.
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.
Luca Pulina and Martina Seidl. The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17). Artif. Intell., 274:224-248, 2019.
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.
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.
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.
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.
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.
Leander Tentrup. CAQE and quabs: Abstraction based QBF solvers. J. Satisf. Boolean Model. Comput., 11(1):155-210, 2019.
Martina Seidl
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode