2026-07-23T21:02:50Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23760 2025-11-12T13:00:16Z ddc:004 open_access

Analyzing Reformulation Performance in Core-Guided MaxSAT Solving Schidler, André Szeider, Stefan maximum satisfiability OLL core-guided Core-guided algorithms like OLL are among the best methods for solving the Maximum Satisfiability problem (MaxSAT). Although some performance characteristics of OLL have been studied, a comprehensive experimental analysis of its reformulation behavior is still missing. In this paper, we present a large-scale study on how different reformulations of a MaxSAT instance produced by OLL affect solver performance. By representing these reformulations as a directed acyclic graph (DAG), we isolate the impact of structural features - such as the size and interconnectivity of unsatisfiable cores - on solver runtime. Our extensive experimental evaluation of over 600k solver runs reveals clear correlations between DAG properties and performance outcomes. These results suggest a new avenue for designing heuristics that steer the solver toward more tractable reformulations. All OLL DAGs and performance data from our experiments are publicly available to foster further research. Schloss Dagstuhl – Leibniz-Zentrum für Informatik André Schidler and Stefan Szeider 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.26 urn:nbn:de:0030-drops-237605 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.26 eng https://creativecommons.org/licenses/by/4.0/legalcode