Preface

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. The aim of this workshop is to provide an interactive
platform for discussing recent advancements and alternative approaches to QBF
solving. The QBF Workshop 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 4th edition of the QBF Workshop took place on the 4th of July in
Bordeaux and was co-located with the 19th International Conference on Theory
and Applications of Satisfiability Testing. In its 4th edition, the QBF Workshop
broadened its scope. Apart from topics related to QBF, topics of interest included
the theory and practice of quantification in other formalisms like quantified
constraint satisfaction problems (QCSP), satisfiability modulo theories (SMT)
or theorem proving.
    After a careful reviewing process, three contributed papers were chosen for
presentation. The papers are the first three papers included in these proceedings.
Besides three invited talks by M. Janota, C. Scholl and R. Wimmer, and M. Suda,
the QBF Workshop had the pleasure to feature a keynote by H. Kleine Büning on
“Open Problems for Quantified Boolean Formulas”. In six short presentations,
several solvers participating the QBFEval 2016, were presented. We invited all
participants to include a solver description in this proceedings. Three teams
provided such descriptions which were accepted for this proceedings after an
additional round of reviews. L. Pulina concluded the QBF Workshop with a
presentation of the results of the QBFEval 2016. A summary is included in this
proceedings as invited contribution.
    Last but not least, we would like to thank all the PC members and subreview-
ers for their work helping us to set up an interesting program for the workshop
and to ensure the quality of this proceedings.


Linz/Vienna, Oct. 2016                        Florian Lonsing, Martina Seidl
Program Committee
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
Florian Lonsing               TU Wien, Austria
Martina Seidl                 JKU Linz, Austria
Friedrich Slivovsky           TU Wien, Austria

Subreviewers: Benjamin Kiesl, Katalin Fazekas, both TU Wien, Austria