Computing Resolution-Path Dependencies in Linear Time
Proceedings of SAT 2012, the Fifteen International Conference on Theory and Applications of Satisfiability Testing June 17-20, 2012, Trento, Italy. Lecture Notes in Computer Science, vol. 7317, pp. 58-71, Springer-Verlag, 2012.
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).
Preprint available from Arxiv.org: 1202.3097.