In conjunction with SAT 2024.
Program
9:15 |
Opening |
|
9:30 |
Long-Hin Fung, Che Cheng, Yu-Wei Fan, Tony Tan, and Jie-Hong Roland Jiang |
2-DQBF Solving and Certification via Property-Directed Reachability Analysis |
10:00 |
Franz-Xaver Reichl |
Revisiting candidate representation in the DQBF solver Pedant |
10:30 |
Break |
|
11:00 |
Alex Weng and Friedrich Slivovsky |
Certified Circuit Reconstruction for QBF |
11:30 |
Olaf Beyersdorff, Benjamin Böhm and Meena Mahajan |
Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs |
12:00 |
Break |
|
14:00 |
Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche and Luc Nicolas Spachmann |
Polynomial Calculus for Quantified Boolean Logic: Lower Bounds through Circuits and Degree |
14:30 |
Abhimanyu Choudhury and Meena Mahajan |
Proof systems for QCDCL with dependency schemes |
15:00 |
Discussion |
Overview
Quantified Boolean formulas (QBF) are an extension of propositional logic which allows for explicit quantification over propositional variables. The decision problem of QBF is PSPACE-complete, compared to the NP-completeness of the decision problem of propositional logic (SAT). Many problems from application domains such as model checking, formal verification or synthesis are PSPACE-complete, and hence could be encoded in QBF in a natural way. Considerable progress has been made in QBF solving throughout the past years. However, in contrast to SAT, QBF is not yet widely applied to practical problems in academic or industrial settings. For example, the extraction and validation of models of (un)satisfiability of QBFs has turned out to be challenging, given that state-of-the-art solvers implement different solving paradigms. The goal of the International Workshop on Quantified Boolean Formulas (QBF Workshop) is to bring together researchers working on theoretical and practical aspects of QBF solving. In addition to that, it addresses (potential) users of QBF in order to reflect on the state-of-the-art and to consolidate on immediate and long-term research challenges. The workshop also welcomes work on reasoning with quantifiers in related problems, such as dependency QBF (DQBF), quantified constraint satisfaction problems (QCSP), and satisfiability modulo theories (SMT) with quantifiers.
About
Continued improvements in the performance of propositional satisfiability (SAT) solvers are enabling a growing number of applications in the area of electronic design automation, such as model checking, synthesis, and symbolic execution. SAT solvers are also a driving force behind recent progress in constrained sampling and counting, and competitive planning tools. In most of these cases, SAT solvers deal with problems from complexity classes beyond NP and propositional encodings that grow super-polynomially in the size of the original instances. Clever techniques such as incremental solving can partly alleviate this issue, but ultimately the underlying asymptotics lead to formulas that are too large to be solved by even the most efficient SAT solvers.
This has prompted the development of decision procedures for more succinct generalizations of propositional logic such as Quantified Boolean Formulas (QBFs), which allow for explicit quantification over truth values. The decision problem of QBF is PSPACE-complete, and thus many problems from application domains such as model checking, formal verification or synthesis—which happen to be PSPACE-complete— could be succinctly encoded in QBF.
Considerable progress has been made in QBF solving throughout the past years. However, in contrast to SAT, QBF solvers generally do not scale well enough on practically relevant problems arising in an industrial setting.
-
The main aim of the workshop is to bring together researchers working on QBF theory and solver developers so as to further our theoretical understanding of this hardness and find ways of overcoming it in practice. It provides a forum in which the community can identify immediate and long-term research challenges. That includes (potential) users, which are invited to reflect on the current state-of-the-art and identify obstacles to the adoption of QBF solvers as well as specific problems (instances) for developers to target.
-
Researchers in other areas of automated reasoning face similar problems in lifting techniques and algorithms for quantifier-free formulas to a quantified version. For instance, this is the case in Quantified Constrained Satisfaction Problems (QCSP), or Sat Modulo Theory (SMT) with quantifiers. This workshop also seeks to promote an exchange of ideas and collaboration between researchers working on QBF and those in other subfields of automated reasoning that deal with quantification.
-
Recent years have seen research on Dependency QBF (DQBF), which further generalize QBFs by allowing non-linear quantifier prefixes. Given that DQBF evaluation is NEXP-complete, and in view of the difficulties presented by QBF solving, the development of DQBF solvers may seem futile. However, the trade-off between succinctness and complexity offered by DQBF may be favorable in practice. The workshop also aims to be a platform for research on formalisms that go beyond QBF in this way.
Submission
Submissions of extended abstracts are invited and will be managed via Easychair https://easychair.org/conferences/?conf=qbf2024
In particular, we invite the submission of extended abstracts on work that has been published already, novel unpublished work, or work in progress.
The following forms of submissions are solicited:
-
Proposals for short tutorial presentations on topics related to the workshop. Tutorial proposals will be reviewed by the PC. The number of accepted tutorials depends on the overall number of accepted papers and talks, with the aim to set up a balanced workshop program.
-
Talk abstracts reporting on already published work. Such an abstract should include an outline of the planned talk, and pointers to relevant bibliography.
-
Talk proposals presenting work that is unpublished or in progress.
-
Submissions which describe novel applications of QBF or related formalisms in various domains are particularly welcome. Additionally, this call comprises known applications which have been shown to be hard for QBF solvers in the past as well as new applications for which present QBF solvers might lack certain features still to be identified.
Each submission should have an overall length of 1-4 pages in LNCS format. Authors may decide to include an appendix with additional material. Appendices will be considered at the reviewers’ discretion.
The accepted extended abstracts will be published on the workshop webpage. The workshop does not have formal proceedings.
Authors of accepted contributions are expected to give a talk at the workshop.
Program Committee
-
Hubie Chen, Birkbeck, King’s College London
-
Martina Seidl, JKU Linz
-
Friedrich Slivovsky, Univ. Liverpool
Important Dates
-
July 20: Submission
-
July 31: Notification
-
August 10: Final Version
-
August 20: Workshop