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 EvoCOP 2022

    Best paper award at EvoCOP 2022

    2022-05-24
    Jonas Mayerhofer, Markus Kirchweger, Marc Huber, and Günther Raidl received the best paper award for their work A Beam Search …Read More »
  • New PhD: Guangping Li

    New PhD: Guangping Li

    2022-05-13
    Guangping Li successfully defended her PhD thesis “An Algorithmic Study of Practical Map Labeling” on May 13, 2022. Congratulations, Dr. …Read More »
  • Outstanding results for TU Wien students at the 2021 Graph Drawing Contest

    Outstanding results for TU Wien students at the 2021 Graph Drawing Contest

    2021-09-24
    The 28th Annual Graph Drawing Contest, a long running tradition of the graph drawing research community, was held in conjunction …Read More »
  • Jan Dreier receives a LICS’21 Distinguished Paper Award

    Jan Dreier receives a LICS’21 Distinguished Paper Award

    2021-07-02
    Congratulations to Jan Dreier for his LICS 2021 Distinguished Paper Award for his paper Lacon- and Shrub-Decompositions: A New Characterization …Read More »
  • Lecture at Austrian Parliament

    Lecture at Austrian Parliament

    2021-06-16
    Stefan Szeider and Martin Kronegger gave a lecture on Algorithms and Programming to members of the Austrian Parliament. The lecture …Read More »

News archive

All news for 2015, 2016, 2017, 2018, 2019, 2020 and 2021.
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.