Computing Resolution-Path Dependencies in Linear Time

Details Computing Resolution-Path Dependencies in Linear Time Computing Resolution-Path Dependencies in Linear Time

2012-02-14

arxiv.org/abs/1202.3097v2

Computer Science

Data Structures and Algorithms

14 pages

Scientific paper

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

Affiliated with

Also associated with

No associations

Rating

Computing Resolution-Path Dependencies in Linear Time does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Computing Resolution-Path Dependencies in Linear Time, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Computing Resolution-Path Dependencies in Linear Time will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-90126