Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Certified Branch-and-Bound MaxSAT Solving (Extended Version)

Dieter Vandesande, Jordi Coll, Bart Bogaerts

TL;DR

MaxSAT solvers are powerful but prone to correctness errors in safety-critical contexts. The paper develops VeriPB-based proof logging for certifying branch-and-bound MaxSAT solving, covering look-ahead bounding and CNF encodings based on BDDs and MDDs, implemented within the MaxCDCL solver. It provides formal certification results for the look-ahead core derivations and the MDD/BiDD encodings, and reports practical overheads that are generally manageable, with proof-checking remaining an area for improvement. This work enables auditable, certifiable MaxSAT solving in real-world applications and sets the stage for future enhancements in proof checking and broader certification across search paradigms.

Abstract

Over the past few decades, combinatorial solvers have seen remarkable performance improvements, enabling their practical use in real-world applications. In some of these applications, ensuring the correctness of the solver's output is critical. However, the complexity of modern solvers makes them susceptible to bugs in their source code. In the domain of satisfiability checking (SAT), this issue has been addressed through proof logging, where the solver generates a formal proof of the correctness of its answer. For more expressive problems like MaxSAT, the optimization variant of SAT, proof logging had not seen a comparable breakthrough until recently. In this paper, we show how to achieve proof logging for state-of-the-art techniques in Branch-and-Bound MaxSAT solving. This includes certifying look-ahead methods used in such algorithms as well as advanced clausal encodings of pseudo-Boolean constraints based on so-called Multi-Valued Decision Diagrams (MDDs). We implement these ideas in MaxCDCL, the dominant branch-and-bound solver, and experimentally demonstrate that proof logging is feasible with limited overhead, while proof checking remains a challenge.

Certified Branch-and-Bound MaxSAT Solving (Extended Version)

TL;DR

MaxSAT solvers are powerful but prone to correctness errors in safety-critical contexts. The paper develops VeriPB-based proof logging for certifying branch-and-bound MaxSAT solving, covering look-ahead bounding and CNF encodings based on BDDs and MDDs, implemented within the MaxCDCL solver. It provides formal certification results for the look-ahead core derivations and the MDD/BiDD encodings, and reports practical overheads that are generally manageable, with proof-checking remaining an area for improvement. This work enables auditable, certifiable MaxSAT solving in real-world applications and sets the stage for future enhancements in proof checking and broader certification across search paradigms.

Abstract

Over the past few decades, combinatorial solvers have seen remarkable performance improvements, enabling their practical use in real-world applications. In some of these applications, ensuring the correctness of the solver's output is critical. However, the complexity of modern solvers makes them susceptible to bugs in their source code. In the domain of satisfiability checking (SAT), this issue has been addressed through proof logging, where the solver generates a formal proof of the correctness of its answer. For more expressive problems like MaxSAT, the optimization variant of SAT, proof logging had not seen a comparable breakthrough until recently. In this paper, we show how to achieve proof logging for state-of-the-art techniques in Branch-and-Bound MaxSAT solving. This includes certifying look-ahead methods used in such algorithms as well as advanced clausal encodings of pseudo-Boolean constraints based on so-called Multi-Valued Decision Diagrams (MDDs). We implement these ideas in MaxCDCL, the dominant branch-and-bound solver, and experimentally demonstrate that proof logging is feasible with limited overhead, while proof checking remains a challenge.

Paper Structure

This paper contains 22 sections, 15 theorems, 68 equations, 2 figures, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Pseudo-Boolean Optimization and MaxSAT
  4. The VeriPB Proof System
  5. Certifying Branch-And-Bound with Look-Ahead
  6. Certifying CNF Encodings based on (Multi-Valued) Decision Diagrams
  7. Certification
  8. Generalization to MDDs
  9. Experiments
  10. Overhead in proof logging
  11. Overhead in proof checking
  12. Conclusion
  13. Preliminaries
  14. Certifying Branch-And-Bound with Look-Ahead
  15. Proof logging
  16. ...and 7 more sections

Key Result

Proposition 3

Let $\mathcal{Q}\xspace$ be an $\mathcal{O}\xspace$-compatible set of weighted local cores and assume $\beta\xspace$ is any total assignments that refines $\alpha\xspace$ and satisfies $F\xspace$.

Figures (2)

  • Figure 1: Comparison of solving time with and without proof logging.
  • Figure 2: Comparison of solving time (with proof logging enabled) with proof checking time.

Theorems & Definitions (28)

  • Definition 1
  • Definition 2
  • Proposition 3
  • Proposition 4
  • proof : Proof sketch
  • Theorem 5
  • Example 6
  • Proposition 7: ANORM12NewLookBDDsPseudo-BooleanConstraints
  • Proposition 8
  • Proposition 9
  • ...and 18 more