Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
F. Slivovsky, St. Szeider:
"Variable Dependencies and Q-Resolution";
Vortrag: International Workshop on Quantified Boolean Formulas,
Helsinki, Finland;
09.06.2013; in: "International Workshop on Quantified Boolean Formulas 2013 Informal Workshop Report",
F. Lonsing, M. Seidl (Hrg.);
(2013),
S. 22
- 29.
Kurzfassung englisch:
We propose Q(D)-resolution, a proof system for Quantified Boolean Formulas. Q(D)-resolution is a generalization of Q-resolution parameterized by a dependency scheme D. This system is closely related to search-based QCNF solvers that use dependency schemes to generalize the QDPLL algorithm, such as DepQBF. We prove that Q(Dstd)-resolution is sound by presenting a transformation of Q(Dstd)-resolution refutations into ordinary Q-resolution refutations, where Dstd denotes the so-called Standard Dependency Scheme.
Zugeordnete Projekte:
Projektleitung Stefan Szeider:
The Parameterized Complexity of Reasoning Problems
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.