Computing Resolution-Path Dependencies in Linear Time ,

DOI10.1007/978-3-642-31612-8_6MaRDI QIDQ2843322zbMATH OpenOpenAlexFDO

Authors Friedrich Slivovsky, Stefan Szeider

Publication date 12 August 2013

Published in Theory and Applications of Satisfiability Testing – SAT 2012 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1202.3097

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Complexity of proofs (03F20)

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

Recommendations

• Linear-Time Algorithms for Dominators and Other Path-Evaluation Problems
• Finding Tutte paths in linear time
• A tutorial on time and space bounds in tree-like resolution
• STACS 2004
• Solving the 2-disjoint paths problem in nearly linear time
• Time of computations on linear binary graphs
• A complexity gap for tree resolution
• A simple linear-time algorithm for finding path-decompositions of small width
• scientific article; zbMATH DE number 3849198

Cited in

(13)

• Long distance Q-resolution with dependency schemes
• Dependency schemes for DQBF
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Quantifier reordering for QBF
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• Variable independence and resolution paths for quantified Boolean formulas
• Variable dependencies and Q-resolution
• Efficiently representing existential dependency sets for expansion-based QBF solvers
• Preprocessing for DQBF
• Combining resolution-path dependencies with dependency learning
• Small resolution proofs for QBF using dependency treewidth
• Long-distance Q-resolution with dependency schemes

This page was built for publication: Computing Resolution-Path Dependencies in Linear Time ,

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2843322)