CALL FOR PAPERS

                QBF 2016
       4th International Workshop on 
  Quantified Boolean Formulas (and Beyond)

      Bordeaux, France, July 4, 2016

     Affiliated to and co-located with: 
           SAT 2016 conference
     Bordeaux, France, July 5-8, 2016

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 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. Considerable progress has been made in the theory and practice of QBF solving throughout the past years.

As the efforts of extending languages with quantifiers have not only been made for propositional logic in terms of QBFs, but in many other formalism like Constraint Satisfaction Problem (CSP) and Satisfiability Modulo Theories (SMT), QBF 2016 also targets researchers working in these related fields in order to exchange experiences and ideas.

The goal of the International Workshop on Quantified Boolean Formulas (and Beyond) is to bring together researchers working on theoretical and practical aspects of QBF solving and related formalisms involving quantifiers. The workshop addresses theoreticians and practitioners in order to reflect on the state of the art in research and to consolidate on immediate and long-term challenges.


Please follow http://fmv.jku.at/qbf16/ for any updates.

  • May 8 2016: paper submission
  • May 29 2016: notification of acceptance
  • June 20 2016: camera-ready version of papers
  • July 4 2016: workshop


The workshop is concerned with all aspects of current research on formalisms enriched by quantifiers, in particular QBF. The topics of interest include (but are not limited to):

  • Applications, encodings and benchmarks with quantifiers

  • Experimental evaluations of solvers or related tools

  • Case studies illustrating the power of quantifiers

  • Certificates and proofs for QBF, QSMT, QCSP, etc.

  • Formats of proofs and certificates

  • Implementations of proof checkers and verifiers

  • Decision procedures

  • Calculi and their relationships

  • Proof theory and complexity results

  • Data structures, implementation details, and heuristics

  • Pre- and inprocessing techniques

  • Structural reasoning


Submissions of papers will be managed via Easychair: https://easychair.org/conferences/?conf=qbf2016

We solicit paper submissions in the following categories:

  • talk-only papers: 2-4 pages
  • full papers: up to 12 pages
  • short tutorial presentation: 2-4 pages

Page limits do not include references and optional appendices.

Talk-only papers present work that has been published already, novel unpublished work, or work in progress. We explicitly solicit the submission of talk-only papers describing work that has been published at other venues and which falls into the scope of the workshop.

Full papers describe novel, unpublished work, including work in progress.

Authors are encouraged to provide additional material such as source code of tools, experimental data, benchmarks and related publications.

We plan to publish the accepted papers (except talk-only papers) in CEUR workshop proceedings, which are indexed with an ISSN.

NEW: we solicit 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.

Submissions which describe novel applications of QBF 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.

Previously published work or extensions thereof may be submitted to the workshop but that case has to be explicitly stated in the submitted paper. This regulation also applies to work which is currently under review elsewhere.

Authors of accepted papers are expected to give a talk at the workshop.

A short abstract of each talk given at the workshop will be published on the workshop webpage.


  • Florian Lonsing Vienna University of Technology, Austria

  • Martina Seidl
    Johannes Kepler University Linz, Austria


  • Fahiem Bacchus, University of Toronto, Canada
  • Olaf Beyersdorff, University of Leeds, UK
  • Jasmin Christian Blanchette, Inria Nancy and LORIA, France
  • Hubie Chen, Universidad del Pais Vasco and Ikerbasque, Spain
  • Marijn Heule, The University of Texas at Austin, USA
  • Jie-Hong Roland Jiang, National Taiwan University, Taiwan
  • Friedrich Slivovsky, TU Wien, Austria