Invided Talk

Friedrich Slivovsky: Dependency Schemes for Quantified Boolean Formulas


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.
This talk is based upon work supported by Austrian Science Fund FWF under grant number P27721.

Accepted Papers

Olaf Beyersdorff, Leroy Chew, Meena Mahajan and Shukla Anil Feasible Interpolation for QBF Resolution Calculi
Valeriy Balabanov, Jie-Hong Roland Jiang and Christoph Scholl Skolem functions computation for CEGAR based QBF solvers
Valeriy Balabanov and Jie-Hong Roland Jiang Reducing Satisfiability and Reachability to DQBF


The program is available at

Workshop Summary

A summary of the QBF workshop.