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

Qute: A Dependency Learning QBF Solver

Quantified Boolean Formulas, or QBFs, augment propositional formulas with existential and universal quantification over truth values. QBFs can succinctly encode problems arising in areas such as formal verification and synthesis.

For instance, if \(\phi(X, Y)\) specifies a system's desired input/output behavior (with inputs \(X\) and outputs \(Y\)), the QBF \(\Phi = \forall X \exists Y \phi (X, Y)\) is true if there is a system implementing this specification. In general, the value of a variable \(y \in Y\) can depend on the values of all variables \(x \in X\), but in practice \(y\) often depends only on a small subset of \(X\). Such information on variable dependencies can significantly reduce the search space that QBF solvers must consider, but unfortunately deciding whether \(y\)  depends on \(x\) is as hard as evaluating a QBF. Some solvers rely on so-called dependency schemes to over-approximate the set of variable dependencies, but the resulting approximation tends to be coarse and frequently coincides with the set of syntactic dependencies.

As part of our project on variable dependencies of QBFs we developed Qute, a QBF solver that obtains information on variable dependencies on the fly. Qute assumes that variable \(y\) is independent of variable \(x\) until it runs into a problem that suggests otherwise, in which case the pair \((x, y)\) is added to a database of dependencies that must be observed. Experiments show that Qute typically only learns a small fraction of a formula's syntactic dependencies, which results in improved propagation and a more freedom for decision heuristics.

Awards

Qute placed 3rd in the PCNF track of QBFEVAL'17.

Download

Qute is open source and available from GitHub. Qute is written in C++14.

Team

Friedrich Slivovsky, Tomas Peitl, and Stefan Szeider

Developers

Friedrich Slivovsky and Tomas Peitl

Publications

1 result
2017
[1]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]

 

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.