The goal of the International Workshop on Quanti ed 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 re ect 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 Satis ability 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 quanti cation in other formalisms like quanti ed constraint satisfaction problems (QCSP), satis ability modulo theories (SMT) or theorem proving. After a careful reviewing process, three contributed papers were chosen for presentation. The papers are the rst 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 Buning on \Open Problems for Quanti ed 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 subreviewers for their work helping us to set up an interesting program for the workshop and to ensure the quality of this proceedings.
Fahiem Bacchus Olaf Beyersdor Jasmin Christian Blanchette Hubie Chen Marijn Heule Jie-Hong Roland Jiang Florian Lonsing Martina Seidl Friedrich Slivovsky University of Toronto, Canada University of Leeds, UK Inria Nancy and LORIA, France Universidad del Pais Vasco and Ikerbasque, Spain The University of Texas at Austin, USA National Taiwan University, Taiwan TU Wien, Austria JKU Linz, Austria TU Wien, Austria