2026-04-14T03:55:48Zhttps://recercat.cat/oai/request

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

Revisiting SAT-based Solvers: MaxSAT Rules and Core Sequences Alòs, Josep Ansótegui Gil, Carlos José Torres Montiel, Eduard Maximum Satisfiability Satisfiability 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. 2026 info:eu-repo/semantics/article info:eu-repo/semantics/publishedVersion https://doi.org/10.1613/jair.1.19525 1943-5037 https://hdl.handle.net/10459.1/469846 https://hdl.handle.net/10459.1/469846 eng info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2021-2023/PID2022-138506NB-C21/ES/SATISFACTIBILIDAD Y OPTIMIZACION CON CERTIFICADOS DE PRUEBA MAS ALLA DE RESOLUCION - APLICACIONES (PROOFS BEYOND-A)/ Reproducció del document publicat a https://doi.org/10.1613/jair.1.19525 Journal of Artificial Intelligence Research, 2026, vol. 85, Article 16 cc-by (c) Josep Alòs, Carlos Ansótegui, Eduard Torres, 2026 Attribution 4.0 International info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/4.0/ AI Access Foundation