Variable Independence and Resolution Paths for Quantified Boolean Formulas

DOI10.1007/978-3-642-23786-7_59zbMath1273.68188OpenAlexW182482375MaRDI QIDQ3169452

Allen van Gelder

Publication date: 23 September 2011

Published in: Principles and Practice of Constraint Programming – CP 2011 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-23786-7_59

Mathematics Subject Classification ID

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

Related Items (11)

Solution validation and extraction for QBF preprocessing ⋮ Quantifier reordering for QBF ⋮ Preprocessing for DQBF ⋮ Exploiting Resolution-Based Representations for MaxSAT Solving ⋮ 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: Variable Independence and Resolution Paths for Quantified Boolean Formulas