Efficient certified RAT verification

DOI10.1007/978-3-319-63046-5_14zbMath1494.68284arXiv1612.02353OpenAlexW2564212270MaRDI QIDQ2405252

Luís Cruz-Filipe, Peter Schneider-Kamp, Marijn J. H. Heule, Warren A. jun. Hunt, Matt Kaufmann

Publication date: 22 September 2017

Full work available at URL: https://arxiv.org/abs/1612.02353

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (29)

Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Efficient, verified checking of propositional proofs ⋮ Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ Inconsistency Proofs for ASP: The ASP - DRUPE Format ⋮ Never trust your solver: certification for SAT and QBF ⋮ Towards Uniform Certification in QBF ⋮ Unnamed Item ⋮ QMaxSATpb: a certified MaxSAT solver ⋮ Simulating strong practical proof systems with extended resolution ⋮ Truth Assignments as Conditional Autarkies ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Certified dominance and symmetry breaking for combinatorial optimisation ⋮ Certified Core-Guided MaxSAT Solving ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ Propositional proof skeletons ⋮ Unsatisfiability proofs for distributed clause-sharing SAT solvers ⋮ Clausal proofs for pseudo-Boolean reasoning ⋮ Explainable online monitoring of metric temporal logic ⋮ SAT modulo symmetries for graph generation and enumeration ⋮ The resolution of Keller's conjecture ⋮ A flexible proof format for SAT solver-elaborator communication ⋮ Generating extended resolution proofs with a BDD-based SAT solver ⋮ Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker ⋮ Efficient verified (UN)SAT certificate checking ⋮ Formally verifying the solution to the Boolean Pythagorean triples problem ⋮ The resolution of Keller's conjecture ⋮ Flexible proof production in an industrial-strength SMT solver ⋮ Clause redundancy and preprocessing in maximum satisfiability

Uses Software

• DRAT-trim
• LRAT
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Efficient certified RAT verification