Skip to Main content Skip to Navigation
Conference papers

A Verified SAT Solver Framework including Optimization and Partial Valuations

Abstract : Based on our formal framework for CDCL (conflict-driven clause learning) using the proof assistant Isabelle/HOL, we verify an extension of CDCL computing cost-minimal models called OCDCL. It is based on branch and bound and computes models of minimal cost with respect to total valuations. The verification starts by developing a framework for CDCL with branch and bound, called CDCLBnB, which is then instantiated to get OCDCL. We then apply our formalization to three different applications. Firstly, through the dual rail encoding, we reduce the search for cost-optimal models with respect to partial valuations to searching for total cost-optimal models, as derived by OCDCL. Secondly, we instantiate OCDCL to solve MAX-SAT, and, thirdly, CDCLBnB to compute a set of covering models. A large part of the original CDCL verification framework was reused without changes to reduce the complexity of the new formalization. To the best of our knowledge, this is the first rigorous formalization of CDCL with branch and bound and its application to an optimizing CDCL calculus, and the first solution that computes cost-optimal models with respect to partial valuations.
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/hal-02963986
Contributor : Mathias Fleury <>
Submitted on : Monday, October 12, 2020 - 9:29:24 AM
Last modification on : Monday, October 12, 2020 - 3:25:46 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Mathias Fleury, Christoph Weidenbach. A Verified SAT Solver Framework including Optimization and Partial Valuations. LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, May 2020, Alicante, Spain. pp.212-193, ⟨10.29007/96wb⟩. ⟨hal-02963986⟩

Share

Metrics

Record views

4

Files downloads

5