Never trust your solver: certification for SAT and QBF
From MaRDI portal
Publication:6118810
DOI10.1007/978-3-031-42753-4_2OpenAlexW4386297898MaRDI QIDQ6118810
Publication date: 28 February 2024
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-031-42753-4_2
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Solving QBF with counterexample guided refinement
- The QBF Gallery: behind the scenes
- Backdoor sets of quantified Boolean formulas
- Symmetries of quantified Boolean formulas
- Polynomial-time validation of QCDCL certificates
- A little blocked literal goes a long way
- Short proofs for some symmetric quantified Boolean formulas
- Resolution for quantified Boolean formulas
- Dual proof generation for quantified Boolean formulas with a BDD-based solver
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- On expansion and resolution in CEGAR based QBF solving
- DRAT proofs, propagation redundancy, and extended resolution
- The equivalences of refutational QRAT
- QRAT polynomially simulates \(\forall\)-Exp+Res
- Simulating strong practical proof systems with extended resolution
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- Expansion-based QBF solving versus Q-resolution
- Solution validation and extraction for QBF preprocessing
- Efficient certified RAT verification
- Long-distance Q-resolution with dependency schemes
- Unified QBF certification and its applications
- Short Q-resolution proofs with homomorphisms
- Multi-linear strategy extraction for QBF expansion proofs via local soundness
- SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers
- Inprocessing Rules
- On Unification of QBF Resolution-Based Calculi
- Clause Elimination for SAT and QSAT
- Abstraction-Based Algorithm for 2QBF
- QBF Resolution Systems and Their Proof Complexities
- A Unified Proof System for QBF Preprocessing
- Nenofex: Expanding NNF for QBF Solving
- Contributions to the Theory of Practical Quantified Boolean Formula Solving
- Verifying Refutations with Extended Resolution
- Automated Testing and Debugging of SAT and QBF Solvers
- Integrating Dependency Schemes in Search-Based QBF Solvers
- New Resolution-Based QBF Calculi and Their Proof Complexity
- A Machine-Oriented Logic Based on the Resolution Principle
- Theory and Applications of Satisfiability Testing
- Efficient verified (UN)SAT certificate checking
- Encoding Redundancy for Satisfaction-Driven Clause Learning
- Proof Complexity of Quantified Boolean Logic — A Survey
