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

QBF Proofs and Certificates (Research Project)

Funding organization: Austrian Science Fund (FWF)

Project number: (ESP 197 ESPRIT-Programm)

Project Team

Leroy Chew (PI)

Stefan Szeider

Friedrich Slivovsky

Topic

Quantified Boolean Formulas (QBF) extends propositional logic. Solving a QBF is theoretically more difficult than solving a propositional SAT (satisfiability) problem. QBFs are canonically PSPACE complete, meaning solving them could be used to solve any PSPACE problem by proxy. In the last decade progress in QBF solving is being undertaken. Proof complexity is the main theoretical framework used to understand SAT and QBF solving. Proof systems use the same logical rules as sound solvers, the proof size can often be a lower bound of running time between proof systems and related solvers. Proof systems can also be used to certify the correctness of solvers. However certification of QBF solvers is not yet a common occurrence.

We wish to further study the landscape of QBF proof complexity, studying the existing QBF proof systems that have emerged to capturing the solvers over the last decade. We also wish to use knowledge of soundness and complexity to make minor and major modifications to QBF proof systems, that could be beneficial to theory and practice. Our hope is that such knowledge will be of use to the QBF solving community.

Publications

Sorry, no results for this query

News

  • PhD completed by Andre Schidler

    PhD completed by Andre Schidler

    2023-05-31
    Congratulations to André Schidler, who successfully defended his PhD thesis "Scalability for SAT-based combinatorial problem solving" today.   Thanks to …Read More »
  • PhD completed by Vaidyanathan P.R.

    PhD completed by Vaidyanathan P.R.

    2023-05-12
    Congratulations to Vaidyanathan P.R., who successfully defended his PhD thesis Scalable Bayesian Network Structure Learning using SAT-based Methods today. Thanks …Read More »
  • New FWF ESPRIT Postdocs

    New FWF ESPRIT Postdocs

    2022-11-09
    Leroy Chew and Alexis de Colnet just joined the Algorithms and Complexity group as PIs of their own FWF ESPRIT …Read More »
  • Best student paper award at DIAGRAMS 2022

    Best student paper award at DIAGRAMS 2022

    2022-10-01
    Alexander Dobler received the Best Student Paper Award at the 13th International Conference on the Theory and Application of Diagrams …Read More »
  • Robert Ganian promoted to Associate Professor

    Robert Ganian promoted to Associate Professor

    2022-07-01
    Effective as of today, Robert Ganian is promoted to a tenured Associate Professor at the Algorithms and Complexity group. Congratulations, …Read More »

News archive

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