ABSTRACT. The nesting of existential and universal quantifiers in Quantified Boolean Formulas (QBFs) causes dependencies among variables that have to be respected by solvers and preprocessing techniques. Given formulas in prenex normal form, standard algorithms implicitly make the most conservative assumption about variable dependencies: variable y depends on variable x whenever x and y are associated with different quantifiers and x precedes y in the quantifier prefix. The resulting set of dependencies is often a coarse overapproximation containing many "spurious" dependencies which lead to unnecessary restrictions that, in turn, inhibit performance. We survey dependency schemes as a means to obtaining more fine-grained overapproximations of a formula's variable dependencies and talk about challenges arising from the integration of dependency schemes into solvers.

ABSTRACT. In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. We establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or expansion-based solving. This both provides the first general lower bound method for QBF calculi as well as largely extends the scope of classical feasible interpolation. We apply our technique to obtain new exponential lower bounds to all resolution-based QBF systems for a new class of QBF formulas based on the clique problem. Finally, we show how feasible interpolation relates to the recently established lower bound method based on strategy extraction.

ABSTRACT. In this work we propose an approach to extract Skolem-functions from CEGAR based QBF solvers (e.g., RareQS) for true QBF formulas containing 2 or 3 quantification levels. We as well propose some optimizations to improve extracted certificates and perform detailed experimental evaluation.

ABSTRACT. In this work, we aim at transforming propositional satisfiability and directed reachability problems into DQBF and therefore provide useful benchmarks to bridge solvers among different complexity classes. With the generated benchmarks, we perform experiments to evaluate DQBF solver IDQ.