A Unified Proof System for QBF Preprocessing

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

Mathematics Subject Classification ID

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

• sQueezeBF
• Bloqqer
• DepQBF

This page was built for publication: A Unified Proof System for QBF Preprocessing