SAT-Basierende lokale Verbesserungsmethoden

Strukturelle Zerlegung ist eine der erfolgreichsten Methoden, um schwere Berechnungsprobleme, die zum Beispiel beim probabilistischen Schliessen auftreten, zu lösen. Das Finden einer geeigneten strukturellen Zerlegung ist aber selbst ein schweres Problem und stellt eine grosse Herausforderung an die Entwicklung von Algorithmen dar. In diesem Forschungsprojekt schlagen wir eine neuartige Herangehensweise zum Finden struktureller Zerlegungen vor. Die Grundidee ist, mittels exakter Methoden, eine heuristisch gefundene suboptimale Zerlegung schrittweise zu verbessern. Dieser Grundidee folgend werden wir neue Zerlegungsmethoden für Graphen, Hypergraphen und anderer Strukturen entwickeln. Wir erwarten, damit bessere Zerlegungen für Eingaben zu finden, die für exakte Methoden zu gross sind. Die geplante Forschung besteht aus einer Kombination von theoretischer Analyse und der empirischen Evaluierung von Prototypen.

Viele schwere Optimierungsprobleme können effizient in das auslagenlogische Erfüllbarkeitsproblem (SAT) übersetzt und dann mit einem leistungsstarken SAT-Solver oder Varianten wie MaxSAT oder QBF-SAT gelöst werden. In manchen Fällen führt die Übersetzung zu einer erheblichen Vergrößerung der Eingabe, sodass diese einmalige Übersetzung nicht durchführbar ist. In diesem Projekt überwinden wir diese Einschränkung, indem wir wiederholt kleine lokale Teile der Probleminstanz nach SAT übersetzen, was es uns ermöglicht, die Leistungsfähigkeit des SAT-Solvers auf große Instanzen zu skalieren. Wir konnten so einen Ansatz erfolgreich für verschiedene wichtige Berechnungsprobleme entwickeln, wie für das Lernen der Struktur eines Bayesschen Netzes, das Induzieren eines interpretierbaren Entscheidungsbaums oder das Minimieren eines Booleschen Schaltkreises.