StartseiteMathlog

Theorema Magnum MCMLXXI: NP-Vollständigkeit des SAT-Problems

Von / 25. März 2021 / 15 Kommentare / Seite 2 von 2 / Auf einer Seite lesen
Mehr

Der Satz von Cook wurde unabhängig auch in der Sowjetunion von Leonid Levin, ein Doktoranden Kolmogorows, bewiesen, dessen Promotion in Moskau aber aus politischen Gründen verweigert wurde und dessen Arbeit im Westen lange unbekannt blieb.

Ein anderes Entscheidungsproblem war 1970 von Juri Matijassewitsch in Leningrad negativ gelöst worden: er bewies, dass es für Polynome vom Grad mindestens 4 keinen Algorithmus geben kann, der entscheidet, ob sie ganzzahlige Nullstellen besitzen. (Für Polynome vom Grad höchstens 2 gab Carl Ludwig Siegel 1972 einen solchen Algorithmus an und für Polynome vom Grad 3 ist die Frage offen.) Einen solchen Algorithmus zu finden war eines der von David Hilbert auf dem ICM 1900 in Paris gestellten Probleme gewesen.

Bild: https://commons.wikimedia.org/wiki/File:Stephen_A._Cook_1968_(enlarged_portion).jpg

1 / 2
Stichworte: , , , , , ,
Mehr

Kommentare (15)

  1. #1 Karl Mistelberger
    mistelberger.net
    25. März 2021

    Mit den meisten hier vorgestellten mathematischen Themen fange ich nichts an. Das liegt daran, dass Mathematiker auf Teufel komm raus ohne Rücksicht auf Anwendungen produzieren.

    Erfüllbarkeit spielt aber bei der Wartung von Betriebssystemen eine große Rolle. Richtige Betriebssysteme sind modular aufgebaut (Windows scheidet daher aus) und bestehen selbst im einfachsten Fall aus tausenden Paketen. Die Aktualisierung bereitete um die Jahrtausendwende große Frustration. Der Zustand besserte sich schneller als erwartet. Kluge Köpfe hatten sich des Problems angenommen:

    Using SAT solver algorithms solve many of the problems the old solver had

    •speed: magnitudes faster

    •reliable results

    •extendibility: implementation of complex dependencies is easy

    •sensible error reports

    https://en.opensuse.org/images/b/b9/Fosdem2008-solver.pdf

  2. #2 hwied
    25. März 2021

    Wenn ich es richtig verstehe, dann geht es um Aussagenlogik , um Logikbausteinen , um Software, die von einem bestehenden Ergebnis ausgeht, vielleicht 20 verschiedene Variablen und dazu eine logische Gleichung sucht, die zu der vorgegebenen Lösung führt.
    Bei wenig Variablen kann das der Computer durch Versuch und Irrtum lösen, bei einer hohen Anzahl von Variablen ist der Rechenaufwand zu hoch.
    Ein praktisches Bespiel wäre jetzt nützlich.

  3. #3 Karl Mistelberger
    mistelberger.net
    25. März 2021

    Auf meinem Rechner sind momentan 3660 Softwarepakete installiert, von denen viele voneinander abhängen. Die Pakete können aktualisiert, entfernt oder neue installiert werden:

    https://doc.opensuse.org/documentation/leap/reference/html/book.opensuse.reference/cha-sw-cl.html#sec-zypper

    https://en.wikipedia.org/wiki/ZYpp#SAT_solver_integration

    https://en.opensuse.org/openSUSE:Libzypp_satsolver_basics

  4. #4 hwied
    25. März 2021

    K,M.
    Sie haben Windows als Betriebssystem? Die Softwarepakete werden über .dll mit Windows verknüpft.

  5. #5 Jolly
    25. März 2021

    @hwied

    Sie haben Windows als Betriebssystem?

    Ja, hat er. Seine Links zu openSUSE sollen uns auf eine falsche Fährte locken.

    Der (NP-)Vollständigkeit halber: Sie sind echt ein Knaller.

  6. #6 Jolly
    25. März 2021

    @Karl Mistelberger

    Richtige Betriebssysteme sind modular aufgebaut (Windows scheidet daher aus)

    Wurde eigentlich schon bewiesen, dass Probleme mit dem Betriebssystem Linux stets zur Komplexitätsklasse P gehören, die meisten unter Windows aber NP-vollständig sind?

  7. #7 Jens
    26. März 2021

    Nur falls außer mir noch jemand etwas verwirrt war über den letzten Absatz: Es geht um Polynome in mehreren Variablen. Für Polynome beliebigen Grads in einer Variablen gibt es einen solchen Algorithmus.

  8. #8 rolak
    26. März 2021

    unter Windows aber NP-vollständig

    Joi Jolly, niedlicher Tippfehler – die sind selbstverständlich XP-vollständig.

  9. #9 Karl Mistelberger
    mistelberger.net
    26. März 2021

    > #6 Jolly, 25. März 2021
    > Wurde eigentlich schon bewiesen, dass Probleme mit dem Betriebssystem Linux stets zur Komplexitätsklasse P gehören, die meisten unter Windows aber NP-vollständig sind?

    Die Komplexität von Windows ist gewollt, Teil der Geschäftsstrategie. Die Auswüchse sind bekannt. Aus gutem Grund machten viele einen Bogen um die Aktualisierung von Microsoft Exchange, mit erheblichen Nebenwirkungen:

    https://en.wikipedia.org/wiki/2021_Microsoft_Exchange_Server_data_breach

    Selbst die Aktualisierung des Drucksystems führt zum totalen Systemabsturz:

    https://borncity.com/win/2021/03/16/windows-10-out-of-band-update-for-blue-screen-printing-bug/

    Benutzer berichteten, dass die Behebung des Fehlers auch schon das installieren von 500 GB Software zur Folge hatte.

    Beide Systeme sind unter Linux mit minimalem Aufwand zu warten. Der Mail Server ist kein Einfallstor für Schadsoftware und das Drucksystem hat noch nie den Rechner zum Absturz gebracht.

  10. #10 Joachim
    27. März 2021

    Die Aussage, eine beliebige Software (wie Mail Server oder Druckersystem) hätten unter Linux noch nie den Rechner zum Absturz gebracht, würde ich bezweifeln. Komplexe Programme wie sendmail, die praktisch eine Programmiersprache eingebaut haben, sind vom “Halteproblem” betroffen. Sie sind also beweisbar (oder gerade nicht beweisbar) grundsätzlich gefährdet. Dazu kommt, dass immer wieder scheinbar harmlose usermode-Programme Sicherheitslücken eröffnen. Dies gerade dann, wenn sie z.B. die graphische Benutzeroberfläche (ein window) verwenden.

    Ich mag ja auch kein MS-Win. Aber wir wollen es nun mal lieber nicht übertreiben.

  11. #11 Joachim
    27. März 2021

    Jetzt habe ich doch glatt vor lauter Linux vergessen mich für den schönen Artikel zur NP-Vollständigkeit des SAT-Problems zu bedanken.

  12. #12 Karl Mistelberger
    mistelberger.net
    27. März 2021

    > #10 Joachim, 27. März 2021
    > Komplexe Programme wie sendmail, die praktisch eine Programmiersprache eingebaut haben, sind vom “Halteproblem” betroffen. Sie sind also beweisbar (oder gerade nicht beweisbar) grundsätzlich gefährdet.

    In Erinnerung an Wolfgang Pauli formuliere ich: Das ist ja nicht einmal eine Aussage zum Thema. Oder aktueller: steckt da Biden-Strategie dahinter? Die Zeit schrieb “in dem er vage blieb glückte sie [die Pressekonferenz]”.

    Es gibt ja bekanntlich nichts Praktischeres als eine gute Theorie. Doch wenn sie nicht anwendbar ist hilft sie nicht weiter. Seit einem Jahrzehnt erledigt systemd die Ressourcenverwaltung, so dass kein außer Kontrolle geratener Prozess das System gefährdet.

    Bleibt hinzuzufügen, dass der größte Fortschritt seit der Entwicklung von Unix bei einem sichtlich überfordertem Publikum einen sinnlosen Proteststurm hervorrief. Das Lieblingsziel des Pöbels wurde Lennart Poettering, der ursprüngliche Autor von systemd.

  13. #13 Joachim
    27. März 2021

    Wenn ich mich nicht irre ist die Windows/Linux Diskussion hier am Thema vorbei?

    Es sei denn, es geht darum, für zwei gebebene Graphen L und W zu entscheiden, ob es einen Teilgraphen von L isomorph zu W gibt. Könnte W für Wine stehen? Welcher Teilgraph wäre dann systemd?

    Noch eins, weil du gerade fragtest: :(){ :|: & };:
    Klar soweit? Probiere mal aus, ob du die ulimits richtig gesetzt hast.

  14. #14 Karl Mistelberger
    mistelberger.net
    29. März 2021

    > Noch eins, weil du gerade fragtest: :(){ :|: & };:

    Zumindest eine Ansage, die sich mir ohne Grübeln sofort erschließt. Im denkbar schlimmsten Fall mit Vordergrundpriorität in konsole aufgerufen werden hier 10000 bashs gestartet. Dann erscheint im journal die trockene Meldung:

    3400G kernel: cgroup: fork rejected by pids controller

    Die Systemauslastung steigt von 0.5 auf 300. Wird konsole beendet ist der Spuk schneller vorbei als er aufgetreten ist. systemd tut bei diesem Experiment genau das, was er soll. Alle wissen das. Nur die Feucht-Träumer wollen es nicht wahrhaben.

  15. #15 Theorema Magnum – Mathlog
    26. April 2021

    […] Konvergente Differenzenschemata der Navier-Stokes-Gleichung Die Jacquet-Langlands-Korrespondenz NP-Vollständigkeit des SAT-Problems Dualität des BMO-Raums zum Hardy-Raum Die LBB-Bedingung Die Weil-Vermutungen Der […]