Invided Talk
Friedrich Slivovsky: Dependency Schemes for Quantified Boolean Formulas
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.
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 |