Solution validation and extraction for QBF preprocessing
From MaRDI portal
Publication:2362496
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
Never trust your solver: certification for SAT and QBF ⋮ Towards Uniform Certification in QBF ⋮ Truth Assignments as Conditional Autarkies ⋮ Unnamed Item ⋮ Dual proof generation for quantified Boolean formulas with a BDD-based solver ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers
Uses Software
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
