2026-04-17T07:59:51Zhttps://recercat.cat/oai/request

oai:recercat.cat:10459.1/4698462026-03-30T18:33:38Zcom_2072_3622col_2072_479130

00925njm 22002777a 4500 dc Alòs, Josep author Ansótegui Gil, Carlos José author Torres Montiel, Eduard author 2026 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. https://hdl.handle.net/10459.1/469846 Maximum Satisfiability Satisfiability Revisiting SAT-based Solvers: MaxSAT Rules and Core Sequences