The enhanced performance of today’s MaxSAT solvers has elevated their appeal for many large-scale applications, notably in software analysis and computer-aided design. Our research delves into refining anytime MaxSAT solving by repeatedly identifying and solving with an exact solver smaller subinstances that are chosen based on the graphical structure of the instance. We investigate various strategies to pinpoint these subinstances. This structure-guided selection of subinstances provides an exact solver with a high potential for improving the current solution. Our exhaustive experimental analyses contrast our methodology as instantiated in our tool MaxSLIM with previous studies and benchmark it against leading-edge MaxSAT solvers.
@InProceedings{schidler_et_al:LIPIcs.CP.2024.26, author = {Schidler, Andr\'{e} and Szeider, Stefan}, title = {{Structure-Guided Local Improvement for Maximum Satisfiability}}, booktitle = {30th International Conference on Principles and Practice of Constraint Programming (CP 2024)}, pages = {26:1--26:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-336-2}, ISSN = {1868-8969}, year = {2024}, volume = {307}, editor = {Shaw, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.26}, URN = {urn:nbn:de:0030-drops-207112}, doi = {10.4230/LIPIcs.CP.2024.26}, annote = {Keywords: maximum satisfiability, large neighborhood search (LNS), SAT-based local improvement (SLIM), incomplete MaxSAT, graphical structure, metaheuristic} }
Feedback for Dagstuhl Publishing