[Zurück]


Vorträge und Posterpräsentationen (ohne Tagungsband-Eintrag):

F. Slivovsky:
"Dependency Schemes for Quantified Boolean Formulas";
Vortrag: International Workshop on Quantified Boolean Formulas, Austin, Texas (eingeladen); 23.09.2015.



Kurzfassung englisch:
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
performance.

Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.