Towards Certified MaxSAT Solving
: Certified MaxSAT solving with SAT oracles and encodings of pseudo-Boolean constraints

Scriptie/Masterproef: Master's Thesis

Samenvatting

Maximum Satisfiability (MaxSAT) is a combinatorial optimization paradigm where a so-called solver searches for a solution to a propositional formula while simultaneously optimizing a linear objective function. Extensive research in the field has led to highly efficient solving algorithms; an increase in performance of the annual MaxSAT evaluation's participants has been witnessed year after year. Unfortunately, the constant race for more efficient algorithms comes at a price: the development of complex software often leads to the introduction of bugs and erroneous reasoning, which might even result in incorrect outcomes. One way to mitigate this incorrectness is by designing certifying algorithms. A certifying algorithm does not only produce an answer to its input, but also produces an easily verifiable proof, called a certificate, of the correctness of its answer. An independent and simpler proof checker then verifies if the provided certificate indeed proves the correctness of the solver's answer for the given input. In contrast to the success in Satisfiability Checking (SAT), certifying algorithms have not yet had their breakthrough in MaxSAT solving.

This thesis contributes to the introduction of certifying algorithms in the field of MaxSAT solving by showing how to make two out of four well-known types of MaxSAT solvers certifying. To do so, we utilize the VeriPB proof system, which is a proof system for optimization with linear inequalities over Boolean variables.
We prove that the reasoning performed by both model-improving as well as core-guided MaxSAT solvers fits naturally into the VeriPB proof system. We evaluate our approach by implementing certification in the model-improving solver QMaxSAT and the state-of-the-art core-guided solvers RC2 and CGSS. The experiments demonstrate the importance of certifying algorithms; by making RC2 and CGSS certifying, an important bug was revealed which may have led to incorrect results.
With respect to computational overhead, we argue that the overhead incurred by producing proofs of correctness is manageable for most situations; while the resources necessary for checking the produced proofs are still more expensive.
Datum prijs2023
Originele taalEnglish
BegeleiderBart Bogaerts (Promotor)

Citeer dit

'