Quantifie d Boolean formulas (QBF) are an extension of propo sitional logic which allows for explicit quantific ation over propositional variables. Many problems from application domains such as model checking, f ormal verification or synthesis are PSPACE-complet e, and hence could be encoded in QBF in a natural way. However, in contrast to SAT, QBF is not yet w idely applied to practical problems in academic or industrial settings. The goal of the Internationa l Workshop on Quantified Boolean Formulas (QBF Wor kshop) is to bring together researchers working on theoretical and practical aspects of QBF solving. In addition to that, it addresses (potential) use rs of QBF in order to reflect on the state-of-the- art and to consolidate on immediate and long-term research challenges.
\n\nQBF 2021 is affil iated to and co-located with: Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2 021) July 5-9, 2021. The workshop also welcomes wo rk on reasoning with quantifiers in related proble ms, such as dependency QBF (DQBF), quantified cons traint satisfaction problems (QCSP), and satisfiab ility modulo theories (SMT) with quantifiers.
\ nThe workshop is concerned with all aspects of current research on all formalisms enriched by quantifiers, and in particular QBF. Su bmissions of extended abstracts are invited and wi ll be managed via Easychair. In particular, we inv ite the submission of extended abstracts on work t hat has been published already, novel unpublished work, or work in progress, as well as proposals fo r short tutorial presentations. Submissions which describe novel applications of QBF or related form alisms in various domains are particularly welcome .
\n\nEach submission should have an overa ll length of 1-4 pages in LNCS format. Authors may decide to include an appendix with additional mat erial.
\n