Structure-Guided Local Improvement for Maximum Satisfiability

Schidler, André; Szeider, Stefan

doi:10.4230/LIPIcs.CP.2024.26

Record link:

http://hdl.handle.net/20.500.12708/208714

Title:

Structure-Guided Local Improvement for Maximum Satisfiability

Citation:

Schidler, A., & Szeider, S. (2024). Structure-Guided Local Improvement for Maximum Satisfiability. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024) (pp. 26:1-26:23). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CP.2024.26

CatalogPlus:

AC17409099

Publisher DOI:

10.4230/LIPIcs.CP.2024.26

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Schidler, André
Szeider, Stefan

Organisational Unit:

E192-01 - Forschungsbereich Algorithms and Complexity
E056-13 - Fachbereich LogiCS
E056-23 - Fachbereich Innovative Combinations and Applications of AI and ML (iCAIML)

Published in:

30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

ISBN:

978-3-95977-336-2

Volume:

307

Date (published):

2024

Event name:

30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Event date:

2-Sep-2024 - 6-Sep-2024

Event place:

Girona, Catalonia, Spain

Number of Pages:

Publisher:

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Peer reviewed:

Yes

Keywords:

graphical structure; incomplete MaxSAT; large neighborhood search (LNS); maximum satisfiability; metaheuristic; SAT-based local improvement (SLIM)

Abstract:

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.

Research Areas:

Logic and Computation: 100%

Science Branch:

1020 - Informatik: 80%
1010 - Mathematik: 20%

License:

CC BY 4.0