idw – Informationsdienst Wissenschaft

Nachrichten, Termine, Experten

Grafik: idw-Logo
Grafik: idw-Logo

idw - Informationsdienst
Wissenschaft

Science Video Project
idw-Abo

idw-News App:

AppStore

Google Play Store



Instanz:
Teilen: 
27.07.2023 10:43

Der Wettlauf um das Kochen-Specker-Theorem

Dr. Florian Aigner PR und Marketing
Technische Universität Wien

    Ein Weltrekord beim Lösen von Erfüllbarkeitsproblemen gelang an der TU Wien – er ist recht abstrakt, aber die Technologie dahinter ist äußerst wichtig für Hard- und Softwareindustrie.

    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.


    Wissenschaftliche Ansprechpartner:

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


    Originalpublikation:

    Frei zugängliche Version des Artikels: https://arxiv.org/abs/2306.10427


    Weitere Informationen:

    http://Programm und Dokumentation zu SAT modulo Symmetries:
    https://sat-modulo-symmetries.readthedocs.io/en/latest/, öffnet eine externe URL in einem neuen Fenster
    http://Übersichtsartikel zu SAT:
    https://cacm.acm.org/magazines/2023/6/273222-the-silent-revolution-of-sat/fullte...


    Bilder

    Das Forschungsteam: Tomas Peitl, Stefan Szeider, Markus Kirchweger (v.l.n.r)
    Das Forschungsteam: Tomas Peitl, Stefan Szeider, Markus Kirchweger (v.l.n.r)
    TU Wien
    TU Wien


    Merkmale dieser Pressemitteilung:
    Journalisten, jedermann
    Informationstechnik, Mathematik, Physik / Astronomie
    überregional
    Forschungsergebnisse, Wissenschaftliche Publikationen
    Deutsch


     

    Hilfe

    Die Suche / Erweiterte Suche im idw-Archiv
    Verknüpfungen

    Sie können Suchbegriffe mit und, oder und / oder nicht verknüpfen, z. B. Philo nicht logie.

    Klammern

    Verknüpfungen können Sie mit Klammern voneinander trennen, z. B. (Philo nicht logie) oder (Psycho und logie).

    Wortgruppen

    Zusammenhängende Worte werden als Wortgruppe gesucht, wenn Sie sie in Anführungsstriche setzen, z. B. „Bundesrepublik Deutschland“.

    Auswahlkriterien

    Die Erweiterte Suche können Sie auch nutzen, ohne Suchbegriffe einzugeben. Sie orientiert sich dann an den Kriterien, die Sie ausgewählt haben (z. B. nach dem Land oder dem Sachgebiet).

    Haben Sie in einer Kategorie kein Kriterium ausgewählt, wird die gesamte Kategorie durchsucht (z.B. alle Sachgebiete oder alle Länder).