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



Instance:
Share on: 
07/27/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.


    Contact for scientific information:

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


    Original publication:

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


    More information:

    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...


    Images

    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


    Criteria of this press release:
    Journalists, all interested persons
    Information technology, Mathematics, Physics / astronomy
    transregional, national
    Research results, Scientific Publications
    German


     

    Help

    Search / advanced search of the idw archives
    Combination of search terms

    You can combine search terms with and, or and/or not, e.g. Philo not logy.

    Brackets

    You can use brackets to separate combinations from each other, e.g. (Philo not logy) or (Psycho and logy).

    Phrases

    Coherent groups of words will be located as complete phrases if you put them into quotation marks, e.g. “Federal Republic of Germany”.

    Selection criteria

    You can also use the advanced search without entering search terms. It will then follow the criteria you have selected (e.g. country or subject area).

    If you have not selected any criteria in a given category, the entire category will be searched (e.g. all subject areas or all countries).