A verified SAT solver framework including optimization and partial valuations

DOI10.29007/96WBMaRDI QIDQ7024208zbMATH OpenFDO

Authors Mathias Fleury, Christoph Weidenbach

Publication date 20 February 2025

Full work available at URL https://doi.org/10.29007/96WB

zbMATH Keywords

verificationCDCLCDCL with branch-and-bound

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cites work

• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A formulation of the simple theory of types.
• A framework for certified Boolean branch-and-bound optimization
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Algorithms for selective enumeration of prime implicants
• Backing backtracking
• Concrete semantics. With Isabelle/HOL
• Correct system design. Symposium in honor of Ernst-Rüdiger Olderog on the occasion of his 60th birthday, Oldenburg, Germany, September 8--9, 2015. Proceedings
• Edinburgh LCF. A mechanized logic of computation
• Formalization of the Resolution Calculus for First-Order Logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Reducibility among combinatorial problems
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL

Cited in

(1)

• Certainty in formalising SMT-LIB for strings in Isabelle

This page was built for publication: A verified SAT solver framework including optimization and partial valuations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7024208)