Revisiting SAT-based Solvers: MaxSAT Rules and Core Sequences

Abstract

In this paper, we revisit the state-of-the-art of MaxSAT solving. We focus on SAT-based MaxSAT solving algorithms, mainly on Core-guided MaxSAT solvers. We show how to describe Core-guided solvers with Non-CNF MaxSAT rules plus the Extension rule. Equipped with these rules, we show how to apply them alternatively to obtain new Core-guided MaxSAT solvers. Since Core-guided solvers essentially solve a sequence of SAT instances, we also discuss how Core-guided MaxSAT solvers traverse the search space of possible sequences of SAT instances, the existence of exponentially harder sequences, and how to avoid them. The experimental investigation shows comparable and complementary performance to state-of-the-art solvers.

This work was supported by the project PROOFS BEYOND (grant number PID2022-138506NB-C21) funded by the AEI.