Computing resolution-path dependencies in linear time

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). © 2012 Springer-Verlag.