Methode erlaubt effizientere Lösung von Erfüllbarkeitsproblemen in KI und Softwareentwicklung

Wenn künstliche Intelligenzen lernen und optimale Antworten finden sollen, stecken immer auch mathematischer Erfüllbarkeitsprobleme dahinter. Erst spezielle Algorithmen, die diese sogenannten SAT-Probleme lösen, ermöglichten die Fortschritte der KI. Jetzt haben Forscher eine Methode dieser SAT-Solver entscheidend verbessert und so das Lösen bestimmter Erfüllbarkeitsprobleme effizienter und schneller gemacht. Dies könnte auch der KI-Forschung zugutekommen.

Erfüllbarkeitsprobleme (auch SAT-Probleme, vom englischen „satisfiability“) sind für viele moderne Forschungsbereiche und vor allem die Computertechnik wichtig. Mit ihnen kann man überprüfen, ob ein bestimmtes Computerprogramm die richtige Lösung liefert oder ob ein Computerchip garantiert in jeder logisch möglichen Situation korrekt funktioniert. Auch beim Lernen der KI-Systeme kommen SAT-Probleme zum Tragen. Für ihre Lösung werden sogenannte „SAT-Solver“ eingesetzt – Computerprogramme, die solche logischen Aufgaben möglichst schnell und effizient lösen sollen.

Besonders schwer zu lösen sind Erfüllbarkeitsprobleme dann, wenn sie zeigen sollen, dass ein bestimmter Fall niemals eintreten kann – dass es zum Beispiel keinen logisch möglichen Input gibt, bei dem ein Computerprogramm oder ein Computerchip versagt. „Der Raum der Möglichkeiten wird dann schnell unüberblickbar groß“, erklärt Stefan Szeider von der Technischen Universität Wien. „Man müsste dann weit mehr Möglichkeiten durchprobieren als es Atome im Universum gibt – das ist selbst für die besten Computer praktisch nicht möglich.“

Wettbewerb der SAT-Solver

Deshalb arbeiten Forschungsteams weltweit daran, SAT-Solver zu verbessern. Seit 2002 gibt es sogar jährliche Wettbewerbe, in der SAT-Solver in bestimmten Aufgaben gegeneinander antreten. Ziel ist es, Architekturen und Lösungsroutinen für die SAT-Solver zu ermitteln, die Zeit- und Rechenaufwand minimieren und dennoch die Erfüllbarkeitsprobleme zuverlässig lösen. Dazu gehört die Aufteilung des Gesamtproblems in Einzelschritte, die sich parallel lösen lassen, oder die Entscheidung, welche Variablen wegfallen können.

Auch das Erkennen von Symmetrien kann helfen. Dabei wird beispielsweise eine ganze Liste von Möglichkeiten automatisch falsch, wenn eine andere falsifiziert wurde. In diesem Fall kann man nach einem einzigen Test einen ganzen Zweig von Möglichkeiten ausschließen, ohne sie einzeln ausprobieren zu müssen. Wenn man solche Symmetrien geschickt ausnützt, kann man mit einem SAT-Solver Aufgaben lösen, die sonst völlig unlösbar wären.

Neue Methode macht SAT-Solving effizienter

Das Team unter Leitung von Szeider hat nun eine neue SAT-Solver-Methode vorgestellt, in der solche Symmetrien eine große Rolle spielen. Dafür haben sie die Methode der „SAT modulo Symmetries“ um das sogenannte Co-Learning Certificate erweitert. Dieses erlaubt es, auch SAT-Probleme mit sogenannten alternierenden Suchen zu lösen, bei denen bestimmte Zweige nicht über einfache Symmetrien abdeckbar sind. Wie effektiv ihr SAT-Solver funktioniert, hat das Team am Beispiel des berühmten Kochen-Specker-Theorem aus der Quantenphysik demonstriert.

Das Kochen-Specker-Theorem beschreibt eine Liste von Vektoren im drei- oder höherdimensionalen Raum, die ganz bestimmte logische Relationen zueinander haben. Offen ist jedoch die Frage, wie viele Vektoren man für den mathematischen Beweis benötigt. „Die Frage ist: Für welche möglichst große Zahl von Vektoren kann man lückenlos beweisen, dass sie keine Lösung erlauben?“, erklärt Szeider. Bisher war es gelungen, diesen Beweis mithilfe von SAT-Solvern für mindestens 23 Vektoren zu erbringen.

Wichtig auch für die KI-Technologie

Stefan Szeider und sein Team haben diesen Rekord nun gebrochen: Dank ihrer neu entwickelten SAT-Solver-Methode konnten sie den mathematischen Beweis für das Kochen-Specker-Theorem mit mindestens 24 Vektoren erbringen. „Damit haben wir die bekannte Untergrenze weiter verbessert und bewiesen, dass Kochen-Specker-Graphen mindestens 24 Eckpunkte haben“, erklärt das Team. „Damit zeigen wir, dass SAT modulo Symmetries kombiniert mit Co-Certificate Learning den Suchraum im Vergleich zu alternativen Methoden drastisch reduzieren kann.“

Die neue Methode kann nun dazu beitragen, auch moderne Computeranwendungen und die künstliche Intelligenz voranzubringen. „Die SAT-Entwicklung ist weit weniger bekannt als der gefeierte Erfolg des maschinellen Lernens mit seinem allgegenwärtigen und vielberichteten Konsequenzen für die Technologie und Gesellschaft“, schreiben Szeider und Kollegen in einem Hintergrundartikel zu SAT-Solvern. „SAT ist jedoch entscheidend für den Fortschritt der modernen Informationstechnologie.“ (32nd International Joint Conference on Artificial Intelligence, 2023; Proceedings Preprint; doi: 10.48550/arXiv.2306.10427)

Quelle: Technische Universität Wien