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 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.