Der Wettlauf um das Kochen-Specker-Theorem

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 etwas verworren, ist aber ein typisches Beispiel für ein Erfüll­barkeits-Problem oder SAT-Problem, vom englischen „satisfi­ability“. Auf solche logischen Probleme stößt man vielen unter­schied­lichen Forschungs­bereichen – etwa in der Software­technik, wenn man beweisen möchte, dass ein bestimmtes Computer­programm 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 „SAT-Solver“ – Computer­programme, die solche logischen Aufgaben möglichst schnell und effizient lösen sollen.

Aber auch Probleme aus anderen Wissen­schaften 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öher­dimen­sio­nalen Raum, die ganz bestimmte logische Relationen zueinander haben. Die Auswirkungen des Kochen-Specker-Theorems sind dabei weit­reichend: Indem man in den 1960er Jahren eine Liste von Vektoren fand, die diese Relation tatsächlich erfüllen, konnte man beweisen, dass sich Quanten­teilchen grund­legend anders verhalten als klassische Objekte, und zwar nicht, weil man irgendetwas über sie noch nicht weiß, sondern weil die Quantenwelt tatsächlich anders funktioniert als die klassische Welt – ein wichtiges Resultat für die Physik und die Wissen­schafts­philosophie.

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 heraus­fordernde Aufgabe, an der man die Leistungs­fähigkeit von hoch­ent­wickelten SAT-Solvern testen kann.

Beim obigen Beispiel mit Alice, Bob und Carla kann man ein bisschen herum­probieren und feststellen, dass die gesamte Aussage wahr ist, wenn Alice und Carla recht haben, und Bob falsch liegt. Doch bei kompli­zier­teren 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 Computer­programm oder ein Computerchip versagt. Um das mit absoluter Sicherheit zu beweisen, müsste man schließlich alle Möglichkeiten durch­probieren.

„Der Raum der Möglich­keiten wird dann schnell unüberblickbar groß“, sagt Stefan Szeider vom Institut für Logic and Computation der TU Wien. „Man müsste dann weit mehr Möglich­keiten durch­probieren als es Atome im Universum gibt – das ist selbst für die besten Computer praktisch nicht möglich.“

Auf der ganzen Welt arbeitet man daher daran, SAT-Solver durch clevere Tricks zu verbessern. Man nützt dabei aus, dass die Frage­stellung eine ganz bestimmte Struktur hat: Manchmal ist es gar nicht nötig, alle logisch denkbaren Möglich­keiten 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öglich­keiten falsch, die bloß ein symmetrisches Abbild der ersten sind. In diesem Fall kann man nach einem einzigen Test einen ganzen Zweig von Möglich­keiten 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 drei­dimen­sio­nalen Raum zu lösen.

„Klar war: Es sind höchstens 31 – denn eine Lösung mit 31 Vektoren ist bekannt“, sagt 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?“

Erst vor kurzem konnte eine Forschungs­gruppe aus Kanada zeigen: Es müssen mindestens 23 Vektoren sein. 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 Szeider -- allerdings würde man dafür wohl 100 bis 200 CPU-Jahre benötigen, was auf einem leistungs­starken Parallel­rechner in wenigen Wochen durch­ge­fü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 eine zentrale Rolle.

Oft werden Probleme aus der Informatik in leichte und schwere Probleme unterteilt, in P- und NP-Probleme. Das Erfüll­bar­keits-Problem ist eines der schwersten Probleme der Komplexitäts­klasse 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.

TU Wien / RK

Weitere Infos

• Originalveröffentlichung
  M. Kirchweger, T. Peitl & S. Szeider: Co-Certificate Learning with SAT Modulo Symmetries, Proceedings of IJCAI 2023, the 32nd International Joint Conference on Artificial Intelligence, August 19-25, 2023, Macao, S.A.R.; DOI: 10.48550/arXiv.2306.10427
• Algorithms and Complexity (S. Szeider), Institut für Logic and Computation, Technische Universität Wien, Österreich

Weitere Beiträge

• O. Gühne und M. Kleinmann, Auf den Kontext kommt es an, Physik Journal,  Februar 2013, S. 25 PDF