A verified SAT solver framework with learn, forget, restart, and incrementality
type: Item
instance of: scholarly article
title: A verified SAT solver framework with learn, forget, restart, and incrementality
zbMATH Open document ID: 1448.68457
author: Jasmin Christian Blanchette
author: Mathias Fleury
author: Peter Lammich
author: Christoph Weidenbach
published in: Journal of Automated Reasoning
publication date: 2018-08-21T00:00:00Z
full work available at URL: pmc6044257
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 68T05
Mathematics Subject Classification ID: 68T20
zbMATH DE Number: 6921418
zbMATH Keywords: SAT solvers
zbMATH Keywords: CDCL
zbMATH Keywords: DPLL
zbMATH Keywords: proof assistants
zbMATH Keywords: Isabelle/HOL
describes a project that uses: Isabelle/HOL
describes a project that uses: VAMPIRE
describes a project that uses: z3
describes a project that uses: Imperative Refinement
describes a project that uses: Chaff
describes a project that uses: Autoref
describes a project that uses: DPT
describes a project that uses: Completeness theorem
describes a project that uses: SAT Solver Verification
describes a project that uses: Sledgehammer
describes a project that uses: versat
describes a project that uses: Isar
describes a project that uses: MiniSat
describes a project that uses: Locales
describes a project that uses: IsaFoL
describes a project that uses: AVATAR
describes a project that uses: Archive Formal Proofs
MaRDI profile type: Publication
OpenAlex ID: W2790974881
Wikidata QID: Q64950500
cites work: Resolution theorem proving
cites work: Locales: a module system for mathematical theories
cites work: Q5503674
cites work: Extending Sledgehammer with SMT solvers
cites work: Automatic Proof and Disproof in Isabelle/HOL
cites work: Mechanizing the Metatheory of Sledgehammer
cites work: Semi-intelligible Isar proofs from machine-generated proofs
cites work: A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
cites work: Soundness and completeness proofs by coinductive methods
cites work: Fast LCF-Style Proof Reconstruction for Z3
cites work: Imperative Functional Programming with Isabelle/HOL
cites work: Efficient certified RAT verification
cites work: A machine program for theorem-proving
cites work: Theory and Applications of Satisfiability Testing
cites work: versat: A Verified Modern SAT Solver
cites work: Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Code Generation via Higher-Order Rewrite Systems
cites work: Q4247076
cites work: Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
cites work: Partial Recursive Functions in Higher-Order Logic
cites work: Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
cites work: Optimal speedup of Las Vegas algorithms
cites work: Automatic Data Refinement
cites work: Refinement to Imperative/HOL
cites work: Efficient verified (UN)SAT certificate checking
cites work: Formalization of Abstract State Transition Systems for SAT
cites work: Solving SAT and SAT Modulo Theories
cites work: Concrete Semantics
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Formalization of the Resolution Calculus for First-Order Logic
cites work: Metamathematics, Machines and Gödel's Proof
cites work: The Mechanical Verification of a DPLL-Based Satisfiability Solver
cites work: AVATAR: The Architecture for First-Order Theorem Provers
cites work: Automated Reasoning Building Blocks
cites work: Program development by stepwise refinement
DOI: 10.1007/S10817-018-9455-7
Recommended article: A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
Recommended article: SAT-Based Compositional Verification Using Lazy Learning
Recommended article: versat: A Verified Modern SAT Solver

A verified SAT solver framework with learn, forget, restart, and incrementality (Recommended article)
Recommended article: SAT-Based Scalable Formal Verification Solutions
Similarity Score: 0.8774822
Recommender Run: Recommender Run 2

A verified SAT solver framework with learn, forget, restart, and incrementality (Recommended article)
Recommended article: Formal verification of a generic framework to synthesize SAT-provers
Similarity Score: 0.8717495
Recommender Run: Recommender Run 2

A verified SAT solver framework with learn, forget, restart, and incrementality (Recommended article)
Recommended article: Assessing progress in SAT solvers through the Lens of incremental SAT
Similarity Score: 0.8716097
Recommender Run: Recommender Run 2

A verified SAT solver framework with learn, forget, restart, and incrementality (Recommended article)
Recommended article: Formalization and implementation of modern SAT solvers
Similarity Score: 0.86758554
Recommender Run: Recommender Run 2