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

(28)

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

Describes a project that uses

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)