Verbesserte lokale Suche für MaxSAT dank differenzieller Klauselgewichtung

Partial Maximum Satisfiability (PMS) und Weighted Partial Maximum Satisfiability (WPMS) erweitern das klassische MaxSAT-Problem und finden in vielen praktischen Anwendungen Einsatz. Neuere Fortschritte bei Stochastic Local Search (SLS)-Algorithmen konzentrierten sich vor allem auf Klauselgewichtung, vernachlässigten jedoch häufig die wesentlichen Unterschiede zwischen PMS und WPMS. Dadurch blieben bestehende Verfahren oft ungenau in ihrer Gewichtungsaktualisierung.

Die vorliegende Arbeit stellt ein neues Gewichtungskonzept vor, das die Klauselgewichte für PMS‑ und WPMS‑Instanzen unter jeweils eigenen Bedingungen anpasst. Zusätzlich wird ein innovatives Initialisierungsmuster eingeführt, das die spezifischen Eigenschaften beider Problemtypen besser berücksichtigt. Ergänzend dazu wird ein Decimation‑Ansatz vorgestellt, der unit‑ und hard‑Klauseln priorisiert und so die Effektivität der Gewichtung weiter steigert.

Auf Basis dieser Methoden wurde der SLS‑Solver DeepDist entwickelt. In umfangreichen Benchmarks aus den aktuellen MaxSAT‑Evaluations‑Tracks übertrifft DeepDist die führenden SLS‑Solver. Noch beeindruckender ist die Kombination von DeepDist mit TT‑Open‑WBO‑Inc, die die Leistungen der 2024‑Gewinner SPB‑MaxSAT‑c‑Band und SPB‑MaxSAT‑c‑FPS übertrifft und damit die Wirksamkeit des Ansatzes unter Beweis stellt.

Der komplette Code ist frei verfügbar unter https://github.com/jmhmaxsat/DeepDist.