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

Variable Dependencies of QBFs (Research Project)

Funding Organisation: The Austrian Science Fund, FWF
Project Number: FWF P 27721

Project Team

Friedrich Slivovsky (Postdoc)
Tomas Peitl (Doctoral Student)
Stefan Szeider (Professor, Principal Investigator)

Topic

The satisfiability problem of Quantified Boolean Formulas (QBF) offers succinct encodings for hard problems arising in areas such as formal verification and planning. This research project explores new ways to leverage independence of variables for QBF. The nesting of existential and universal quantifiers in Quantified Boolean Formulas can generate variable dependencies that are a serious obstacle to lifting successful techniques from propositional satisfiability to QBF. In some cases one can identify a variable dependency as spurious and conclude that the corresponding variables are in fact independent. This information can be used to significantly improve the performance of decision procedures, but deciding whether variables are independent is a highly intractable problem in itself.

The aim of this project is three-fold: (A) to advance the state of the art in detecting variable independence by developing new theory and improved algorithms for currently used methods; (B) to find new approaches to detecting and harnessing variable independence; (C) to extend the scope of successful techniques from QBF to more general problems.

Software

Research under Theme (B) has lead to the development of Qute (GitHub), a dependency learning QBF solver. Qute placed 3rd in the PCNF track and 4th in the Prenex non-CNF track of QBFEVAL'17.

Publications

9 results
2022
[9]Sum-of-Products with Default Values: Algorithms and Complexity Results
Robert Ganian, Eun Jung Kim, Friedrich Slivovsky, Stefan Szeider
Journal of Artificial Intelligence Research, volume 33, pages 535–552, 2022.
[bibtex] [pdf]
2019
[8]Long-Distance Q-Resolution with Dependency Schemes
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Journal of Automated Reasoning, volume 63, number 1, pages 127–155, 2019.
[bibtex] [pdf] [doi]
[7]Proof Complexity of Fragments of Long-Distance Q-resolution
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Proceedings of SAT 2019, the 22nd International Conference on Theory and Applications of Satisfiability Testing, July 7–12, 2019, Lisbon, Portugal (Mikoláš Janota, Inês Lynce, eds.), volume 11628 of Lecture Notes in Computer Science, pages 319–335, 2019, Springer Verlag.
[bibtex] [pdf] [doi]
[6]Combining Resolution-Path Dependencies with Dependency Learning
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Proceedings of SAT 2019, the 22nd International Conference on Theory and Applications of Satisfiability Testing, July 7–12, 2019, Lisbon, Portugal (Mikoláš Janota, Inês Lynce, eds.), volume 11628 of Lecture Notes in Computer Science, pages 306–318, 2019, Springer Verlag.
[bibtex] [pdf] [doi]
2018
[5]Polynomial-Time Validation of QCDCL Certificates
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Proceedings of SAT 2018, the 21st International Conference on Theory and Applications of Satisfiability Testing, Part of FLoC 2018, July 9–12, 2018, Oxford, UK (Olaf Beyersdorff, Christoph M. Wintersteiger, eds.), volume 10929 of Lecture Notes in Computer Science, pages 253–269, 2018, Springer Verlag.
[bibtex] [pdf] [doi]
[4]Portfolio-Based Algorithm Selection for Circuit QBFs
Holger H. Hoos, Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Proceedings of CP 2018, the 24rd International Conference on Principles and Practice of Constraint Programming (John N. Hooker, ed.), volume 11008 of Lecture Notes in Computer Science, pages 195–209, 2018, Springer Verlag.
[bibtex] [pdf] [doi]
[3]Sum-of-Products with Default Values: Algorithms and Complexity Results
Robert Ganian, Eun Jung Kim, Friedrich Slivovsky, Stefan Szeider
Proceedings of ICTAI 2018, the 30th IEEE International Conference on Tools with Artificial Intelligence (Lefteri H. Tsoukalas, Éric Grégoire, Miltiadis Alamaniotis, eds.), pages 733–737, 2018, IEEE.
[bibtex] [pdf] [doi]
2017
[2]Dependency learning for QBF
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings (Serge Gaspers, Toby Walsh, eds.), volume 10491 of Lecture Notes in Computer Science, pages 298–313, 2017, Springer Verlag.
[bibtex] [pdf] [doi]
2016
[1]Long Distance Q-Resolution with Dependency Schemes
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings (Nadia Creignou, Daniel Le Berre, eds.), volume 9710 of Lecture Notes in Computer Science, pages 500–518, 2016, Springer Verlag.
[bibtex] [pdf] [doi]

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.