Mechanical Verification of SAT Refutations with Extended Resolution

DOI10.1007/978-3-642-39634-2_18zbMath1317.68236OpenAlexW27762129MaRDI QIDQ5327347

Marijn J. H. Heule, Warren A. jun. Hunt, Nathan D. Wetzler

Publication date: 7 August 2013

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-39634-2_18

Mathematics Subject Classification ID

Related Items (9)

Expressing Symmetry Breaking in DRAT Proofs ⋮ How to get more out of your oracles ⋮ Efficient, verified checking of propositional proofs ⋮ An Expressive Model for Instance Decomposition Based Parallel SAT Solvers ⋮ Unnamed Item ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ A flexible proof format for SAT solver-elaborator communication ⋮ Efficient verified (UN)SAT certificate checking ⋮ Formally verifying the solution to the Boolean Pythagorean triples problem

Uses Software

• ACL2
• Coq
• Isabelle/HOL
• PicoSAT
• versat

This page was built for publication: Mechanical Verification of SAT Refutations with Extended Resolution