Solution validation and extraction for QBF preprocessing

DOI10.1007/S10817-016-9390-4zbMath1409.68258OpenAlexW2547601025MaRDI QIDQ2362496

Armin Biere, Marijn J. H. Heule, Martina Seidl

Publication date: 10 July 2017

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-016-9390-4

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (7)

Never trust your solver: certification for SAT and QBF ⋮ Towards Uniform Certification in QBF ⋮ Truth Assignments as Conditional Autarkies ⋮ Unnamed Item ⋮ Should Decisions in QCDCL Follow Prefix Order? ⋮ Dual proof generation for quantified Boolean formulas with a BDD-based solver ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers

Uses Software

• sQueezeBF
• Plingeling
• Bloqqer
• QUBOS
• DepQBF
• DRAT-trim
• Treengeling
• Lingeling
• Quantor
• sKizzo

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The QBF Gallery: behind the scenes
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• Resolution for quantified Boolean formulas
• Expansion-based QBF solving versus Q-resolution
• Unified QBF certification and its applications
• Boolean functions as models for quantified Boolean formulas
• On QBF Proofs and Preprocessing
• Inprocessing Rules
• SAT-Based Synthesis Methods for Safety Specs
• Clause Elimination for SAT and QSAT
• Variable Independence and Resolution Paths for Quantified Boolean Formulas
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• A Unified Proof System for QBF Preprocessing
• Evaluating and certifying QBFs: A comparison of state-of-the-art tools
• Expressing Symmetry Breaking in DRAT Proofs
• Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
• Blocked Clause Elimination
• A First Step Towards a Unified Proof Checker for QBF
• Bounded Universal Expansion for Preprocessing QBF
• Verifying Refutations with Extended Resolution
• sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
• Clause Elimination Procedures for CNF Formulas
• Blocked Clause Elimination for QBF
• Automated Deduction – CADE-20
• A Computing Procedure for Quantification Theory
• Theory and Applications of Satisfiability Testing
• Extended Resolution Proofs for Symbolic SAT Solving with Quantification

This page was built for publication: Solution validation and extraction for QBF preprocessing