Talks and Poster Presentations (with Proceedings-Entry):
F. Slivovsky, St. Szeider:
"Computing Resolution-Path Dependencies in Linear Time";
Talk: International Conference on Theory and Applications of Satisfiability Testing (SAT),
Trento, Italy;
2012-06-17
- 2012-06-20; in: "Proceedings of the Fifteen International Conference on Theory and Applications of Satisfiability Testing (SAT 2012)",
A. Cimatti, R. Sebastiani (ed.);
LNCS / Springer,
7317
(2012),
ISBN: 978-3-642-31611-1;
58
- 71.
English abstract:
The alternation of existential and universal quantifiers in a quantified boolean formula (QBF) generates dependencies among variables that must be respected when evaluating the formula. Dependency schemes provide a general framework for representing such dependencies. Since it is generally intractable to determine dependencies exactly, a set of potential dependencies is computed instead, which may include false positives. Among the schemes proposed so far, resolution path dependencies introduce the fewest spurious dependencies. In this work, we describe an algorithm that detects resolution-path dependencies in linear time, resolving a problem posed by Van Gelder (CP 2011).
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-642-31612-8_6
Related Projects:
Project Head Stefan Szeider:
The Parameterized Complexity of Reasoning Problems
Created from the Publication Database of the Vienna University of Technology.