Algorithms and Complexity Group
  • People
  • Research
  • Courses
  • Talks
  • Jobs
  • Contact

Learning to Solve Quantified Boolean Formulas (Research Project)

Funding Organisation: Vienna Science and Technology Fund, WWTF
Project Number: ICT19-060
Duration: 05/2020 - 04/2023

Project Team

Franz Xaver Reichl (PhD Student)
Leroy Chew (PostDoc)
Friedrich Slivovsky (PI)
Stefan Szeider (Co-PI)

Topic

Quantified Boolean Formulas (QBFs) can succinctly encode hard problems arising in planning, verification,
and synthesis, and the development of efficient procedures for evaluating QBFs (so-called QBF solvers)
will drive advances in all of these areas.

These applications require that QBF solvers not only decide whether a formula is true or false but also
output a witnessing strategy. For instance, when using QBF to solve a program synthesis problem, we
expect solvers to return the synthesized program. Our work on solver design and proof theory has
convinced us that strategies are at the heart of QBF research. However, the prevailing theoretical models of
QBF solvers as decision procedures or proof systems do not capture the fact that they need to compute
strategies. This project aims to develop a new, richer model of QBF solvers as strategy learning algorithms.

Software

  • Unique: A preprocessor for (D)QBF that computes unique Skolem and Herbrand functions (GitHub).
  • Pedant: A certifying DQBF solver based on definition extraction (GitHub).

Publications

11 results
2023
[11]Circuit Minimization with QBF-Based Exact Synthesis
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023 (Brian Williams, Yiling Chen, Jennifer Neville, eds.), pages 4087–4094, 2023, AAAI Press.
[bibtex] [pdf] [doi]
2022
[10]Towards Uniform Certification in QBF
Leroy Chew, Friedrich Slivovsky
39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022, March 15-18, 2022, Marseille, France (Virtual Conference) (Petra Berenbrink, Benjamin Monmege, eds.), volume 219 of LIPIcs, pages 22:1–22:23, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[bibtex] [pdf] [doi]
2021
[9]Certified DQBF Solving by Definition Extraction
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings (Chu-Min Li, Felip Manyà, eds.), volume 12831 of Lecture Notes in Computer Science, pages 499–517, 2021, Springer Verlag.
[bibtex] [pdf] [doi]
[8]Proof Complexity of Symbolic QBF Reasoning
Stefan Mengel, Friedrich Slivovsky
Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings (Chu-Min Li, Felip Manyà, eds.), volume 12831 of Lecture Notes in Computer Science, pages 399–416, 2021, Springer Verlag.
[bibtex] [pdf] [doi]
[7]Engineering an Efficient Boolean Functional Synthesis Engine
Priyanka Golia, Friedrich Slivovsky, Subhajit Roy, Kuldeep S. Meel
IEEE/ACM International Conference On Computer Aided Design, ICCAD 2021, Munich, Germany, November 1-4, 2021, pages 1–9, 2021, IEEE.
[bibtex] [pdf] [doi]
[6]Davis and Putnam Meet Henkin: Solving DQBF with Resolution
Joshua Blinkhorn, Tomáš Peitl, Friedrich Slivovsky
Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings (Chu-Min Li, Felip Manyà, eds.), volume 12831 of Lecture Notes in Computer Science, pages 30–46, 2021, Springer Verlag.
[bibtex] [pdf] [doi]
2020
[5]A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
Friedrich Slivovsky, Stefan Szeider
Proceedings of SAT 2020, The 23rd International Conference on Theory and Applications of Satisfiability Testing (Luca Pulina, Martina Seidl, eds.), volume 12178 of Lecture Notes in Computer Science, pages 267–276, 2020, Springer Verlag.
[bibtex] [pdf]
[4]Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing
Friedrich Slivovsky
Computer Aided Verification - 32nd International Conference, CAV 2020 (Shuvendu K. Lahiri, Chao Wang, eds.), volume 12224 of Lecture Notes in Computer Science, pages 508–528, 2020, Springer Verlag.
[bibtex] [pdf]
[3]Short Q-Resolution Proofs with Homomorphisms
Ankit Shukla, Friedrich Slivovsky, Stefan Szeider
Proceedings of SAT 2020, The 23rd International Conference on Theory and Applications of Satisfiability Testing (Luca Pulina, Martina Seidl, eds.), volume 12178 of Lecture Notes in Computer Science, pages 412–428, 2020, Springer Verlag.
[bibtex] [pdf]
[2]Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness
Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, Florian Zuleger
Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference (Luca Pulina, Martina Seidl, eds.), volume 12178 of Lecture Notes in Computer Science, pages 429–446, 2020, Springer Verlag.
[bibtex]
[1]Fixed-Parameter Tractability of Dependency QBF with Structural Parameters
Robert Ganian, Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020 (Diego Calvanese, Esra Erdem, Michael Thielscher, eds.), pages 392–402, 2020.
[bibtex] [pdf]

News

  • Best Paper Award at SOFSEM 2025

    Best Paper Award at SOFSEM 2025

    2025-01-23
    Thomas Depian, Simon D. Fink, Alexander Firbas, Robert Ganian, and Martin Nöllenburg received the Best Paper Award for their paper …Read More »
  • Markus Wallinger receives Award of Excellence for his PhD Thesis

    Markus Wallinger receives Award of Excellence for his PhD Thesis

    2024-12-05
    Our former group member Markus Wallinger won the Award of Excellence by the Federal Ministry for Education, Science and Research. …Read More »
  • Thomas Depian receives State Prize for his Master’s Thesis

    Thomas Depian receives State Prize for his Master’s Thesis

    2024-11-21
    Our group member Thomas Depian won the Appreciation Award given by the Federal Ministry for Education, Science and Research. This …Read More »
  • Best Paper Award at GECCO 2024 for M. Bresich, G. Raidl, and S. Limmer

    Best Paper Award at GECCO 2024 for M. Bresich, G. Raidl, and S. Limmer

    2024-07-24
    Maria Bresich, Günther Raidl, and Steffen Limmer received the best paper award at the 2024 Genetic and Evolutionary Computation Conference …Read More »
  • Welcome to our Feodor Lynen Fellow Dr. Frank Sommer

    Welcome to our Feodor Lynen Fellow Dr. Frank Sommer

    2024-06-14
    On June 1, 2024, Dr. Frank Sommer has joined the Algorithms and Complexity group with a prestigious Feodor Lynen postdoc …Read More »

News archive

All news for 2015, 2016, 2017, 2018, 2019, 2020, 2021, 2022, 2023 and 2024.
TU Wien Informatics
Offenlegung (§25 MedienG) Inhaber der Website ist das Institut für Logic and Computation an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. – Disclaimer – Datenschutzerklärung
Log in requires cookies.