Angenommen, Alice, Bob und Carla beantworten eine Frage. Jede der drei Antworten ist entweder richtig oder falsch. Ist es logisch möglich, dass mindestens zwei der Antworten richtig sind, mindestens eine falsch ist und außerdem gilt: Weder trifft es zu, dass Bob und Carla beide richtig liegen, noch dass Alice und Bob beide richtig liegen?

Das klingt vielleicht etwas verworren, ist aber ein typisches Beispiel für ein Erfüllbarkeitsproblem (auch SAT-Problem, vom englischen „satisfiability“). Auf solche logischen Probleme stößt man vielen unterschiedlichen Forschungsbereichen – etwa in der Softwaretechnik, wenn man beweisen möchte, dass ein bestimmtes Computerprogramm immer garantiert die richtige Lösung liefert. Oder in der Chip-Industrie, wenn man zeigen soll, dass ein Computerchip garantiert in jeder logisch möglichen Situation korrekt funktioniert. Man verwendet dafür sogenannte „SAT-Solver“ – Computerprogramme, die solche logischen Aufgaben möglichst schnell und effizient lösen sollen.

Die Merkwürdigkeit der Quanten

Aber auch Probleme aus anderen Wissenschaften lassen sich in SAT-Probleme übersetzen, etwa das berühmte Kochen-Specker-Theorem aus der Quantenphysik. Seine Formulierung ist etwas abstrakt – es geht dabei um eine Liste von Vektoren im drei- oder höherdimensionalen Raum, die ganz bestimmte logische Relationen zueinander haben.

Die Auswirkungen des Kochen-Specker-Theorems sind aber sehr weitreichend: Indem man in den 1960erjahren eine Liste von Vektoren fand, die diese Relation tatsächlich erfüllen, konnte man beweisen: Dass sich Quantenteilchen grundlegend anders verhalten als klassische Objekte liegt nicht daran, dass man irgendetwas über sie noch nicht weiß, sondern die Quantenwelt funktioniert tatsächlich anders als die klassische Welt – ein wichtiges Resultat für die Physik und die Wissenschaftsphilosophie.

Nachdem man das bewiesen hatte, kann man aber auch die mathematisch hochkomplexe Frage stellen: Was ist die kompakteste Art, diesen Beweis zu führen? Wie viele dieser Vektoren braucht man dafür mindestens?

Für die Informatik ist das eine herausfordernde Aufgabe, an der man die Leistungsfähigkeit von hochentwickelten SAT-Solvern testen kann.

Herumprobieren ist nicht genug

Beim obigen Beispiel mit Alice, Bob und Carla kann man ein bisschen herumprobieren und feststellen, dass die gesamte Aussage wahr ist, wenn Alice und Carla recht haben, und Bob falsch liegt. Doch bei komplizierteren SAT-Problemen (wie etwa bei der Suche nach passenden Vektoren für das Kochen-Specker-Theorem) ist das nicht möglich.

Besonders schwierig ist es, wenn man nicht nur eine bestimmte Lösung finden soll, sondern stattdessen zeigen soll, 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. Um das mit absoluter Sicherheit zu beweisen, müsste man schließlich alle Möglichkeiten durchprobieren.

„Der Raum der Möglichkeiten wird dann schnell unüberblickbar groß“, sagt Prof. Stefan Szeider vom Institut für Logic and Computation der TU 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.“

Clevere Tricks, weniger Rechenaufwand

Auf der ganzen Welt arbeitet man daher daran SAT-Solver durch clevere Tricks zu verbessern. Man nützt dabei aus, dass die Fragestellung eine ganz bestimmte Struktur hat: Manchmal ist es gar nicht nötig, alle logisch denkbaren Möglichkeiten zu testen. Manchmal lässt sich zeigen, dass manche von ihnen symmetrisch zueinander sind: Wenn eine falsch ist, dann ist auch eine ganze Liste von Möglichkeiten falsch, die bloß ein symmetrisches Abbild der ersten sind. 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. Und so konnte man sich auch Schritt für Schritt durch fortlaufende Verbesserung der SAT-Technologie der Frage annähern, wie viele Vektoren man braucht, um das berühmte Kochen-Specker-Theorem der Quantenphysik (im dreidimensionalen Raum) zu lösen.

„Klar war: Es sind höchstens 31 – denn eine Lösung mit 31 Vektoren ist bekannt“, sagt Stefan Szeider. „Die Frage ist aber nun: Wie viele Vektoren brauch man mindestens? Für welche möglichst große Zahl von Vektoren kann man lückenlos beweisen, dass sie keine Lösung erlaubt?“

Weltrekord!

Erst vor kurzem konnte eine Forschungsgruppe aus Kanada zeigen: Es müssen mindestens 23 Vektoren sein. Stefan Szeider konnte mit seinem Team diesen Rekord nun brechen: Es müssen mindestens 24 sein, so der neue Beweis. Auch der Beweis für 25 sollte mit der an der TU Wien entwickelten Methode "SAT modulo Symmetries" möglich sein, meint Stefan Szeider -- allerdings würde man dafür wohl 100 bis 200 CPU-Jahre benötigen, was auf einem leistungsstarken Parallelrechner in wenigen Wochen durchgeführt werden kann.

Das lohnt sich nicht wirklich – schließlich geht es nicht um das Ergebnis selbst, sondern vielmehr um die Technologie dahinter. SAT-Solver sind aus der modernen Technik nicht mehr wegzudenken, auch im Bereich der künstlichen Intelligenz spielen sie heute eine zentrale Rolle.

Oft werden Probleme aus der Informatik in leichte und schwere Probleme unterteilt – in sogenannte P und NP-Probleme. Das Erfüllbarkeitsproblem ist eines der schwersten Probleme der Komplexitätsklasse NP und daher im Allgemeinen vermutlich schwer zu lösen. Aber die aktuellen Durchbrüche in der SAT-Technologie zeigen: Diese Zweiteilung ist noch nicht die ganze Geschichte. Auch wenn man es mit besonders schwierigen Problemen zu tun hat, kann man ihre Struktur manchmal auf kluge Weise ausnutzen, um berechenbar werden zu lassen, was auf den ersten Blick völlig hoffnungslos erscheint.

Weiterführende Links

Frei zugängliche Version des aktuellen Artikels:
https://arxiv.org/abs/2306.10427, öffnet eine externe URL in einem neuen Fenster

Programm und Dokumentation zu SAT modulo Symmetries:
https://sat-modulo-symmetries.readthedocs.io/en/latest/, öffnet eine externe URL in einem neuen Fenster

Übersichtsartikel zu SAT:
https://cacm.acm.org/magazines/2023/6/273222-the-silent-revolution-of-sat/fulltext, öffnet eine externe URL in einem neuen Fenster

Rückfragehinweis

Prof. Stefan Szeider
Institut für Logic and Computation
Technische Universität Wien
+43 1 58801 192100
stefan.szeider@tuwien.ac.at

Aussender:

Dr. Florian Aigner
Büro für Öffentlichkeitsarbeit
Technische Universität Wien
Resselgasse 3, 1040 Wien
+43 1 58801 41027
florian.aigner@tuwien.ac.at