In conjunction with SAT 2023.

Program

9:00

Welcome

9:10

Leroy Chew: Proof Simulation via Round-based Strategy Extraction for QBF

9:30

Simone Heisinger, Maximilian Heisinger: Quantifier Shifting for Quantified Boolean Formulas Revisited

9:50

Michael Hartisch, Ulf Lorenz: On the Opportunities of Linking Quantification and Optimization

10:10

Maximilian Heisinger, Irfansha Shaik, Jaco van de Pol: Search-Space Pruning with Int-Splits [Slides]

10:30

Break

11:00

Andoni Rodriguez, César Sánchez: QBF solvers for counter-example generation in reactive specifications modulo theories

11:20

Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider: Circuit Minimization with QBF-Based Exact Synthesis

11:40

Irfansha Shaik and Jaco van de Pol: Concise QBF Encodings for Games on a Grid

12:00

QBFGallery, 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

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

  • Luca Pulina, University of Sassari

  • Martina Seidl, JKU Linz

  • Friedrich Slivovsky, TU Wien

Important Dates

  • May 20: Submission

  • May 31: Notification

  • June 15: Final Version

  • July 4: Workshop

Contact