Computing Resolution-Path Dependencies in Linear Time ,

DOI10.1007/978-3-642-31612-8_6zbMath1273.68187arXiv1202.3097OpenAlexW1492210508MaRDI QIDQ2843322

Stefan Szeider, Friedrich Slivovsky

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)

Related Items (9)

Quantifier reordering for QBF ⋮ Preprocessing for DQBF ⋮ Small Resolution Proofs for QBF using Dependency Treewidth ⋮ Long-distance Q-resolution with dependency schemes ⋮ Soundness of \(\mathcal{Q}\)-resolution with dependency schemes ⋮ Dependency Schemes for DQBF ⋮ Long Distance Q-Resolution with Dependency Schemes ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1

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