Program

Program in Easychair

Invited Presenations

• Meena Mahajan: Lower Bound Techniques for QBF Proof Systems
  Slides
• Ralf Wimmer, Sven Reimer, Karina Wimmer, Christoph Scholl and Bernd Becker: Preprocessing for (D)QBF
• Markus Rabe, Leander Tentrup, Cameron Rasmussen and Sanjit A. Seshia: Understanding and Extending Incremental Determinization for 2QBF
• Luca Pulina: QBFEval 2018

Contributed Presentations

• Martin Suda: Towards the Semantics of QBF Clauses
  Abstract: While a substantial progress in terms of understanding these calculi has al- ready been made on the front of proof complexity, the question of semantics of the involved intermediate clauses has until now re- ceived comparatively less attention. In many cases, the semantics is left only implicit, determined by the way in which the clauses are allowed to interact via inferences. This is in stark contrast with propositional or rst-order logic, in which a clause can always be identied with the set of its models. In my talk, I would like to expand on why I find this situation unsatisfying, give examples of what I thought a uniform underlying semantics of QBF clauses could be, and, as a teaser for our talk at SAT, brie y explain what I and Bernhard Gleiss finally identified as a viable candidate.
• Joshua Blinkhorn, Olaf Beyersdorff and Luke Hinde: Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs
  Abstract: We present a new technique for proving proof-size lower bounds in P+$\forall$red. The technique relies only on two semantic measures: the cost of a QBF, and the capacity of a proof. Our central result, the Size-Cost-Capacity Theorem, states that proof-size in P+$\forall$red is at least the ratio of cost to capacity. By examining the capacity of proofs in several concrete systems (the universal reduction extensions of Resoution, Cutting Planes and Polynomial Calculus) we obtain lower bounds based solely on cost. Our technique provides genuine lower bounds in the sense that they continue to hold if P+$\forall$red is given access to an NP oracle [BeyersdorffHP17]. As applications of the technique, we first prove exponential lower bounds for the equality formulas, a new QBF family based on a simple two-player game. The main application is in proving exponential lower bounds with high probability for a class of randomly generated QBFs, the first genuine lower bounds of this kind. Finally, we employ the technique to give a simple proof of hardness for the prominent formulas of Kleine Büning, Karpinski and Flögel.
• Judith Clymo: Short Proofs in QBF Expansion
  Abstract: We examine the relationship between Q-Res and Exp+Res under the natural and practically important restriction to families of QBFs with bounded quantifier complexity. We show that (dag-like) Q-Res is p-simulated by Exp+Res in this case.
• Martina Seidl and Manuel Kauers: The Symmetry Rule for Quantified Boolean Formulas
  Abstract: We extend QBF resolution with a rule for exploiting symmetries and analyze the impact on the power of the new proof system.
• Martin Diller and Uwe Egly: Initial study on the effect of different QBF solvers and preprocessors on link-information sensitive QBF encodings for Abstract Dialectical Frameworks
  Abstract: We implemented link-sensitive encodings for the admissible, preferred, and stable semantics for Abstract Dialectical Frameworks. We carried out a preliminary empirical evaluation to determine the performance of diㄦent QBF solvers and preprocessors on our new link-sensitive encodings vs. encodings known from the literature.
• Florent Capelli and Stefan Mengel: Tractability results for structured quantified CNF-formulas via knowledge compilation
  Abstract: We show how knowledge compilation can be used as a tool for QBF. More precisely, we show that certain one can apply quantification on certain data structures used in knowledge compilation which in combination with the fact that restricted classes of CNF-formulas can be compiled into these data structures can be used to show fixed-parameter tractable results for QBF.
• Matthias van der Hallen and Gerda Janssens: A Grounder From Second-Order Logic To QBF
  Abstract: Recent solver research has developed powerful QBF solvers. Alas, we know of few tools that provide a modelling language on a higher level, translating this to QBF. This is surprising, as in the closely related field of SAT solvers, research has gone hand in hand with the develop- ment of such systems. This extended abstract on work in progress reports on a system that allows the use of second-order logic as a high-level modelling language and that grounds (translates) models written in such a language to a QBF formula. We provide an example encoding, outline the grounding process and propose further research and experiments.
• Holger Hoos, Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider: Portfolio-Based Algorithm Selection for Circuit QBFs
  Quantified Boolean Formulas (QBFs) are a generalization of propositional formulae that admits succinct encodings of verification and synthesis problems. Given that modern QBF solvers are based on different architectures with complementary performance characteristics, a portfolio-based approach to QBF solving is particularly promising. We define a natural set of features of circuit QBFs and show that they can be used to construct portfolio-based algorithm selectors of state-of-the-art circuit QBF solvers that are close to the virtual best solver. We further demonstrate that most of this performance can be achieved using surprisingly small subsets of cheaply computable and intuitive features.

Presenation of QBFEval'18 Contributions

• Simon Cooksey, Mark Batty, Radu Grigore and Mikolas Janota: PrideMM: QBFEVAL Benchmarks
• Tomas Peitl: Chess Solving and Composing
• Florian Lonsing: DepQBF
• Mikolas Janota: RAReQS, QFUN, QESTO
• Friedrich Slivovsky: Qute