Mechanical verification of SAT refutations with extended resolution
From MaRDI portal
Recommendations
- Verifying Refutations with Extended Resolution
- The mechanical verification of a DPLL-based satisfiability solver
- Efficient, verified checking of propositional proofs
- Producing and verifying extremely large propositional refutations
- A verified SAT solver framework with learn, forget, restart, and incrementality
Cited in
(17)- Efficiently checking propositional refutations in HOL theorem provers
- How to get more out of your oracles
- Efficient, verified checking of propositional proofs
- A flexible proof format for SAT solver-elaborator communication
- Generating extended resolution proofs with a BDD-based SAT solver
- Formally verifying the solution to the Boolean Pythagorean triples problem
- Functional encryption for inner product with full function privacy
- Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
- An expressive model for instance decomposition based parallel SAT solvers
- Verification in ACL2 of a generic framework to synthesize SAT-provers
- Expressing symmetry breaking in DRAT proofs
- Verifying Refutations with Extended Resolution
- A flexible proof format for SAT solver-elaborator communication
- The mechanical verification of a DPLL-based satisfiability solver
- SAT-enhanced Mizar proof checking
- Efficient verified (UN)SAT certificate checking
- Producing and verifying extremely large propositional refutations
This page was built for publication: Mechanical verification of SAT refutations with extended resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327347)
