Computing Resolution-Path Dependencies in Linear Time

TL;DR

This paper presents a linear-time algorithm for detecting resolution-path dependencies in quantified boolean formulas, improving efficiency in handling variable dependencies in logical evaluations.

Contribution

The paper introduces an algorithm that computes resolution-path dependencies in linear time, addressing a previously open problem in the field.

Findings

Algorithm operates in linear time

Resolves a problem posed by Van Gelder (2011)

Reduces false positives in dependency detection

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).