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

  • Martin Nöllenburg: promotion to Full Professor

    Martin Nöllenburg: promotion to Full Professor

    2020-12-17
    By December 1st, 2020, our colleague Martin Nöllenburg has been promoted to Full Professor for Graph and Geometric Algorithms.  Martin has …Read More »
  • Martin Kronegger wins the Best Teaching Award 2020

    Martin Kronegger wins the Best Teaching Award 2020

    2020-10-23
    Congratulations to Martin Kronegger who received a Best Teaching Award 2020 from TU Wien. The Algorithms and Complexity group is …Read More »
  • Welcome to our Feodor Lynen Fellow Dr. Manuel Sorge

    Welcome to our Feodor Lynen Fellow Dr. Manuel Sorge

    2020-10-12
    On October 1, 2020, Dr. Manuel Sorge has joined the Algorithms and Complexity group with a prestigious Feodor Lynen postdoc …Read More »
  • TU Wien students excel at the 2020 Graph Drawing Contest

    TU Wien students excel at the 2020 Graph Drawing Contest

    2020-10-01
    The 27th annual Graph Drawing Contest, held (virtually) in conjunction with the 28th International Symposium on Graph Drawing and Network …Read More »
  • Best Paper Award at CP’2020

    Best Paper Award at CP’2020

    2020-09-11
    Tomáš Peitl and Stefan Szeider won the Best Paper Award at the main track of CP'2020, the 26th International Conference on Principles …Read More »

News archive

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