A Unified Proof System for QBF Preprocessing
From MaRDI portal
Publication:3192183
DOI10.1007/978-3-319-08587-6_7zbMath1409.68257OpenAlexW88271430MaRDI QIDQ3192183
Marijn J. H. Heule, Martina Seidl, Armin Biere
Publication date: 26 September 2014
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-08587-6_7
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (19)
Quantified maximum satisfiability ⋮ Solution validation and extraction for QBF preprocessing ⋮ The QBF Gallery: behind the scenes ⋮ Conformant planning as a case study of incremental QBF solving ⋮ Long-distance Q-resolution with dependency schemes ⋮ Soundness of \(\mathcal{Q}\)-resolution with dependency schemes ⋮ Inconsistency Proofs for ASP: The ASP - DRUPE Format ⋮ Never trust your solver: certification for SAT and QBF ⋮ Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification ⋮ Unnamed Item ⋮ Incremental Determinization ⋮ Q-Resolution with Generalized Axioms ⋮ Lifting QBF Resolution Calculi to DQBF ⋮ Long Distance Q-Resolution with Dependency Schemes ⋮ Dual proof generation for quantified Boolean formulas with a BDD-based solver ⋮ How QBF expansion makes strategy extraction hard ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ SAT-Inspired Eliminations for Superposition ⋮ Hardness and optimality in QBF proof systems modulo NP
Uses Software
This page was built for publication: A Unified Proof System for QBF Preprocessing
