Talks and Poster Presentations (with Proceedings-Entry):
F. Slivovsky, St. Szeider:
"Variable Dependencies and Q-Resolution";
Talk: International Workshop on Quantified Boolean Formulas,
Helsinki, Finland;
2013-06-09; in: "International Workshop on Quantified Boolean Formulas 2013 Informal Workshop Report",
F. Lonsing, M. Seidl (ed.);
(2013),
22
- 29.
English abstract:
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.
Related Projects:
Project Head Stefan Szeider:
The Parameterized Complexity of Reasoning Problems
Created from the Publication Database of the Vienna University of Technology.