Structure-guided local improvement for maximum satisfiability

Abstract

Stefan Szeider, from the Vienna University of Technology tells that 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

Stefan Szeider, de la Universitat Tècnica de Viena, explica que el rendiment millorat dels solucionadors MaxSAT actuals ha augmentat el seu atractiu per a moltes aplicacions a gran escala, especialment en l'anàlisi de programari i el disseny assistit per ordinador. La seva investigació aprofundeix en perfeccionar en qualsevol moment la resolució de MaxSAT