A verified SAT solver framework with learn, forget, restart, and incrementality
DOI10.1007/S10817-018-9455-7zbMATH Open1448.68457OpenAlexW2790974881WikidataQ64950500 ScholiaQ64950500MaRDI QIDQ1663234FDOQ1663234
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
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)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theory and Applications of Satisfiability Testing
- Automatic Proof and Disproof in Isabelle/HOL
- Edinburgh LCF. A mechanized logic of computation
- Automatic Data Refinement
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Isabelle/HOL. A proof assistant for higher-order logic
- Resolution theorem proving
- Program development by stepwise refinement
- Solving SAT and SAT Modulo Theories
- A machine program for theorem-proving
- Optimal speedup of Las Vegas algorithms
- Extending Sledgehammer with SMT solvers
- Locales: a module system for mathematical theories
- Semi-intelligible Isar proofs from machine-generated proofs
- Concrete Semantics
- Metamathematics, Machines and Gödel's Proof
- Fast LCF-Style Proof Reconstruction for Z3
- AVATAR: The Architecture for First-Order Theorem Provers
- Partial Recursive Functions in Higher-Order Logic
- Code Generation via Higher-Order Rewrite Systems
- versat: A Verified Modern SAT Solver
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Imperative Functional Programming with Isabelle/HOL
- The Mechanical Verification of a DPLL-Based Satisfiability Solver
- Efficient verified (UN)SAT certificate checking
- Formalization of the Resolution Calculus for First-Order Logic
- Refinement to Imperative/HOL
- Efficient certified RAT verification
- Soundness and completeness proofs by coinductive methods
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- Mechanizing the Metatheory of Sledgehammer
- Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
- Formalization of Abstract State Transition Systems for SAT
- Automated Reasoning Building Blocks
Cited In (14)
- Certifying emptiness of timed Büchi automata
- Automated deduction
- Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL
- Verifying the conversion into CNF in dafny
- Title not available (Why is that?)
- Verified verifying: SMT-LIB for strings in Isabelle
- A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
- An Isabelle/HOL Formalization of the SCL(FOL) Calculus
- On enumerating short projected models
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
- versat: A Verified Modern SAT Solver
- Title not available (Why is that?)
- Verified Decision Procedures for Modal Logics.
Uses Software
Recommendations
- SAT-Based Compositional Verification Using Lazy Learning 👍 👎
- Formalization and implementation of modern SAT solvers 👍 👎
- SAT-Based Scalable Formal Verification Solutions 👍 👎
- Formal verification of a generic framework to synthesize SAT-provers 👍 👎
- versat: A Verified Modern SAT Solver 👍 👎
- Assessing progress in SAT solvers through the Lens of incremental SAT 👍 👎
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality 👍 👎
This page was built for publication: A verified SAT solver framework with learn, forget, restart, and incrementality
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663234)
