A unified proof system for QBF preprocessing

DOI10.1007/978-3-319-08587-6_7MaRDI QIDQ3192183zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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

Cited in

(29)

• Q-resolution with generalized axioms
• Long distance Q-resolution with dependency schemes
• The QBF Gallery: behind the scenes
• Local redundancy in SAT: generalizations of blocked clauses
• A First Step Towards a Unified Proof Checker for QBF
• Quantified maximum satisfiability
• Conformant planning as a case study of incremental QBF solving
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Hardness and optimality in QBF proof systems modulo NP
• Lifting QBF resolution calculi to DQBF
• Hard QBFs for merge resolution
• 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
• Dual proof generation for quantified Boolean formulas with a BDD-based solver
• On Unification of QBF Resolution-Based Calculi
• Inconsistency proofs for ASP: the ASP-DRUPE format
• Solution validation and extraction for QBF preprocessing
• On QBF Proofs and Preprocessing
• CAQE and QuAbS: Abstraction Based QBF Solvers
• 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

Describes a project that uses

Uses Software

• DepQBF
• Bloqqer
• sQueezeBF

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)