A unified proof system for QBF preprocessing

DOI10.1007/978-3-319-08587-6_7zbMATH Open1409.68257OpenAlexW88271430MaRDI QIDQ3192183FDOQ3192183

Authors: 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

Recommendations

• Solution validation and extraction for QBF preprocessing
• On QBF Proofs and Preprocessing
• QRATPre+: effective QBF preprocessing via strong redundancy properties
• Bounded Universal Expansion for Preprocessing QBF
• Blocked clause elimination for QBF

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (28)

• Local redundancy in SAT: generalizations of blocked clauses
• A First Step Towards a Unified Proof Checker for QBF
• The QBF Gallery: behind the scenes
• Conformant planning as a case study of incremental QBF solving
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Quantified maximum satisfiability
• Hardness and optimality in QBF proof systems modulo NP
• Lifting QBF resolution calculi to DQBF
• How QBF expansion makes strategy extraction hard
• Formal correctness of a quadratic unification algorithm
• Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification
• The Qu-Prolog unification algorithm: formalisation and correctness
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• Incremental determinization
• On Unification of QBF Resolution-Based Calculi
• Dual proof generation for quantified Boolean formulas with a BDD-based solver
• Inconsistency proofs for ASP: the ASP-DRUPE format
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Solution validation and extraction for QBF preprocessing
• On QBF Proofs and Preprocessing
• QRATPre+: effective QBF preprocessing via strong redundancy properties
• Bounded Universal Expansion for Preprocessing QBF
• Long-distance Q-resolution with dependency schemes
• SAT-Inspired Eliminations for Superposition
• Moving definition variables in quantified Boolean formulas
• Never trust your solver: certification for SAT and QBF
• Q-resolution with generalized axioms
• Long distance Q-resolution with dependency schemes

Uses Software

• sQueezeBF
• Bloqqer
• DepQBF

This page was built for publication: A unified proof system for QBF preprocessing

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