Talks and Poster Presentations (without Proceedings-Entry):
"Dependency Schemes for Quantified Boolean Formulas";
Talk: International Workshop on Quantified Boolean Formulas,
Austin, Texas (invited);
The nesting of existential and universal quanti ers in Quanti ed Boolean
Formulas 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: vari-
able y depends on variable x whenever x and y are associated with di erent
quanti ers and x precedes y in the quanti er pre x. The resulting set of de-
pendencies is often a coarse overapproximation containing many \spurious"
dependencies which lead to unnecessary restrictions that, in turn, inhibit
Created from the Publication Database of the Vienna University of Technology.