A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

DOI10.1007/978-3-319-40229-1_4zbMath1475.68432OpenAlexW2468912077MaRDI QIDQ2817909

Mathias Fleury, Christoph Weidenbach, Jasmin Christian Blanchette

Publication date: 5 September 2016

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01336074/file/main.pdf

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) 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 (7)

Soundness and completeness proofs by coinductive methods ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formalization of the resolution calculus for first-order logic ⋮ Efficient, verified checking of propositional proofs ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/Isar
• VAMPIRE
• Mizar
• z3
• HOL
• Chaff
• Sledgehammer
• versat
• Locales
• IsaFoL
• Archive Formal Proofs
• AVATAR
• SAT Solver Verification

Cites Work

• Unnamed Item
• Unnamed Item
• Semi-intelligible Isar proofs from machine-generated proofs
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Optimal speedup of Las Vegas algorithms
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• Extending Sledgehammer with SMT solvers
• Locales: a module system for mathematical theories
• Mechanizing the Metatheory of Sledgehammer
• Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
• versat: A Verified Modern SAT Solver
• AVATAR: The Architecture for First-Order Theorem Provers
• Concrete Semantics
• Automatic Proof and Disproof in Isabelle/HOL
• Unified Classical Logic Completeness
• Automated Reasoning Building Blocks
• Solving SAT and SAT Modulo Theories
• Code Generation via Higher-Order Rewrite Systems
• Partial Recursive Functions in Higher-Order Logic
• Metamathematics, Machines and Gödel's Proof
• The Mechanical Verification of a DPLL-Based Satisfiability Solver
• Theorem Proving in Higher Order Logics
• A machine program for theorem-proving
• Fast LCF-Style Proof Reconstruction for Z3
• A formulation of the simple theory of types

This page was built for publication: A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality