A Verified SAT Solver Framework including Optimization and Partial Valuations

Based on the formal framework for CDCL (conflict-driven clause learning) verified by Blanchette et al. using the proof assistant Isabelle/HOL, we verify an optimizing extension of CDCL based on branch and bound, called OCDCL, first by developing a framework for CDCL with branch and bounds, called CDCLBnB. OCDCL computes models of minimal cost with respect to total valuations. 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. OCDCL can also be used to solve further optimization tasks such as MAX-SAT and CDCLBnB can be used to find a set of covering models. A large part of the original CDCL framework could be reused without changes to reduce the complexity of the new formalization. To the best of our knowledge, this is the first rigorous formalization of an optimizing CDCL calculus and the first solution that computes cost-optimal models with respect to partial valuations.