International Workshop on
Quantified Boolean Formulas and Beyond
https://qbf.pages.sai.jku.at/qbf25/
In conjunction with SAT 2025
====================
===========
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 and
extensions like DQBF.
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 QBF
===========
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=qbf25
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
* Talk abstracts reporting on already published work
* 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.
There are two submission deadlines. If submitted before the first deadline
has passed, the notification will be before the early registration
deadline of SAT.
===========
Program Committee
===========
* Hubie Chen, King's College London
* Leroy Chew, TU Wien
* Martina Seidl, JKU Linz
* Friedrich Slivovsky, Univ. Liverpool
===========
Important Dates
===========
* June 10: 1st submission deadline (round 1 deadline)
* June 22: notification of round 1
* July 10: 2nd submission round (round 2 deadline)
* July 22: notification of round 2
* August 11: workshop
== Contact
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************
Posts
