A verified SAT solver framework with learn, forget, restart, and incrementality

DOI10.1007/S10817-018-9455-7zbMath1448.68457OpenAlexW2790974881WikidataQ64950500 ScholiaQ64950500MaRDI QIDQ1663234

Mathias Fleury, Peter Lammich, Christoph Weidenbach, Jasmin Christian Blanchette

Publication date: 21 August 2018

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

Full work available at URL: http://europepmc.org/articles/pmc6044257

zbMATH Keywords

Isabelle/HOLproof assistantsSAT solversDPLLCDCL

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)

Verifying the conversion into CNF in dafny ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ Unnamed Item ⋮ Verified Decision Procedures for Modal Logics. ⋮ Certifying emptiness of timed Büchi automata ⋮ Unnamed Item ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover

Uses Software

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isar
• z3
• Chaff
• Sledgehammer
• versat
• Locales
• Autoref
• IsaFoL
• DPT
• Completeness theorem
• Archive Formal Proofs
• AVATAR
• SAT Solver Verification
• Imperative Refinement

Cites Work

• Unnamed Item
• 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
• Soundness and completeness proofs by coinductive methods
• Efficient certified RAT verification
• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
• Formalization of the Resolution Calculus for First-Order Logic
• 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
• Refinement to Imperative/HOL
• Automatic Proof and Disproof in Isabelle/HOL
• Formalization of Abstract State Transition Systems for SAT
• Automated Reasoning Building Blocks
• Solving SAT and SAT Modulo Theories
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• Imperative Functional Programming with Isabelle/HOL
• 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
• Theory and Applications of Satisfiability Testing
• Automatic Data Refinement
• Program development by stepwise refinement
• A machine program for theorem-proving
• Fast LCF-Style Proof Reconstruction for Z3
• Efficient verified (UN)SAT certificate checking

This page was built for publication: A verified SAT solver framework with learn, forget, restart, and incrementality