Unifying SAT-Based Approaches to Maximum Satisfiability Solving

Session date: 14 October 2024

Summary:

In this talk I will discuss the paper “Unifying SAT-Based Approaches to Maximum Satisfiability Solving”; the paper explores the differences between the 3 different approaches to MaxSAT (core-guided search, implicit hitting sets and objective bounding) and to what extent they are different.

Each of the 3 aforementioned approaches has its strengths and weaknesses but it is poorly understood in what sense they fundamentally differ and how they could potentially be combined. To this end, the paper proposes a new framework, UniMaxSAT, for unifying these approaches and shows that all 3 approaches can be simulated using this framework. Additionally, the paper shows that this framework can be used to create new variants of the 3 approaches.

Relevant papers

Unifying SAT-based approaches to maximum satisfiability solving

Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo

The journal of artificial intelligence research, "7 " # "jul" 2024

Abs HTML

Maximum satisfiability (MaxSAT), employing propositional logic as the declarative language of choice, has turned into a viable approach to solving NP-hard optimization problems arising from artificial intelligence and other real-world settings. A key contributing factor to the success of MaxSAT is the rise of increasingly effective exact solvers that are based on iterative calls to a Boolean satisfiability (SAT) solver. The three types of SAT-based MaxSAT solving approaches, each with its distinguishing features, implemented in current state-of-the-art MaxSAT solvers are the core-guided, the implicit hitting set (IHS), and the objective-bounding approaches. The objective-bounding approach is based on directly searching over the objective function range by iteratively querying a SAT solver if the MaxSAT instance at hand has a solution under different bounds on the objective. In contrast, both core-guided and IHS are so-called unsatisfiability-based approaches that employ a SAT solver as an unsatisfiable core extractor to determine sources of inconsistencies, but critically differ in how the found unsatisfiable cores are made use of towards finding a provably optimal solution. Furthermore, a variety of different algorithmic variants of the core-guided approach in particular have been proposed and implemented in solvers. It is well-acknowledged that each of the three approaches has its advantages and disadvantages, which is also witnessed by instance and problem-domain specific runtime performance differences (and at times similarities) of MaxSAT solvers implementing variants of the approaches. However, the questions of to what extent the approaches are fundamentally different and how the benefits of the individual methods could be combined in a single algorithmic approach are currently not fully understood. In this work, we approach these questions by developing UniMaxSAT, a general unifying algorithmic framework. Based on the recent notion of abstract cores, UniMaxSAT captures in general core-guided, IHS and objective-bounding computations. The framework offers a unified way of establishing quite generally the correctness of the current approaches. We illustrate this by formally showing that UniMaxSAT can simulate the computations of various algorithmic instantiations of the three types of MaxSAT solving approaches. Furthermore, UniMaxSAT can be instantiated in novel ways giving rise to new algorithmic variants of the approaches. We illustrate this aspect by developing a prototype implementation of an algorithmic variant for MaxSAT based on the framework.