Das Erfüllbarkeitsproblem der Aussagenlogik – auch als SAT-Problem bezeichnet nach dem englischen Begriff satisfiablity für Erfüllbarkeit – fragt nach der Erfüllbarkeit einer gegebenen aussagenlogischen Formel durch eine geeignete Variablenbelegung. Man kann das Problem natürlich durch Aufstellen einer Wahrheitstabelle lösen, aber dann wächst der Zeitverbrauch exponentiell mit der Anzahl der Variablen. Man weiß bis heute nicht, ob es einen Algorithmus gibt, der das Problem in polynomieller Zeit löst.

Bei einem Symposium der Association for Computing Machinery präsentierte Stephen Cook 1971 eine Arbeit „The complexity of theorem proving procedures“. In dieser Arbeit ging es darum, dass für viele Probleme, deren Lösung man nicht in polynomieller Zeit findet, es aber jedenfalls möglich ist, die Korrektheit einer gefundenen Lösung in polynomieller Zeit zu überprüfen. In der ein Jahr später von Karp eingeführten Terminologie nennt man die Klasse dieser Probleme NP, während P die Klasse der in polynomieller Zeit lösbaren Probleme bezeichnet. Beispielsweise gehört das SAT-Problem zu NP, denn man kann leicht überprüfen, ob eine gegebene Variablenbelegung eine aussagenlogische Formel erfüllt.

Cook bewies überraschend, dass sich jedes Problem, dessen Lösungen in polynomieller Zeit überprüft werden können, auf das SAT-Problem reduzieren läßt, also dass es zu jedem solchen Problem A einen Algorithmus in polynomieller Zeit zur Lösung von A mit Zugang zu einem Orakel für das SAT-Problem gibt. 

Ebenso bewies er, dass sich jedes solche Probleme auch auf das Teilgraphenisomorphismusproblem reduzieren läßt. In diesem Problem geht es darum, für zwei gegebene Graphen G und H zu entscheiden, ob es einen Teilgraphen von G isomorph zu H gibt. In seinem Konferenzbeitrag schrieb er, dass es damit wohl fruchtlos wäre, nach einer Lösung des Teilgraphenproblems in polynomieller Zeit zu suchen, denn das würde polynomielle Algorithmen für viele andere unzugängliche Probleme liefern.

Diese Arbeit wurde zunächst nur von Logikern beachtet. Ein Jahr später erstellte Richard Karp dann aber eine Liste von 21 Problemen, auf die sich jedes Problem aus NP reduzieren läßt. Die meisten der Probleme waren aus der Graphentheorie, bei einigen handelte es sich um in der Realwelt vorkommende Optimierungsprobleme. Karp nannte solche Probleme NP-schwer. Probleme, die sowohl in NP als NP-schwer sind, nannte er NP-vollständig. Seine Liste war also eine Liste von 21 NP-vollständigen Problemen. Weiter erwähnte er einige der Konsequenzen, wenn P=NP wäre. Dieses Problem und die Suche nach NP-vollständigen Problemen wurden in der Folge zur sehr populären Themen der theoretischen Informatik.

Karp bewies beispielsweise, dass sich das Erfüllbarkeitsproblem der Aussagenlogik auf das Cliquenproblem reduzieren läßt. Dieses fragt, ob es zu einem gegebenen Graphen G und einer Zahl n eine Clique (d.h. einen vollständigen Graphen) der Größe n in G gibt. Dieses Problem ist also ebenfalls NP-vollständig.
Das Cliquenproblem wiederum konnte er auf das Knotenüberdeckungsproblem zurückführen: gegeben einen Graphen G und eine Zahl k, gibt es eine Menge von k Knoten, so dass jede Kante mit mindestens einem der k Knoten verbunden ist?
Das Knotenüberdeckungsproblem wiederum führte er zurück auf das Problem, ob es in einem Graphen einen Hamilton-Kreis (einen jeden Knoten genau einmal durchlaufenden Kreis) gibt. Damit sind auch diese beiden Probleme NP-vollständig.
Ein anderes von ihm als NP-vollständig bewiesenes Problem war das 3-SAT-Problem: ist eine in konjunktiver Normalform vorliegende aussagenlogische Formel, die höchstens 3 Literale pro Klausel enthält, erfüllbar? Dieses wiederum läßt sich auf das Graphfärbungsproblem zurückführen und das dann auf das Rucksackproblem, ein klassisches Optimierungsproblem: aus einer Menge von Objekten mit Gewicht und Nutzwert soll unter den ein vorgegebenes Gesamtgewicht nicht überschreitenden Teilmengen die den Nutzwert maximierende gefunden werden. Und dieses Optimierungsproblem läßt sich auf die Konstruktion eines maximalen Schnittes in einem Graphen zurückführen, d.h. die Zerlegung der Knotenmenge eines Graphen, so dass man eine maximale Zahl zwischen den Teilen verlaufender Kanten hat.
Tatsächlich ließ sich mit Ausnahme der 0-1-ganzzahligen Optimierung die NP-Vollständigkeit aller Probleme in seiner Liste auf die NP-Vollständigkeit entweder des Cliquenproblems oder des 3-SAT-Problems zurückführen und diese beiden ebenso wie die 0-1-ganzzahlige Optimierung sich dann schlußendlich auf das Erfüllbarkeitsproblem der Aussagenlogik.

1 / 2 / Auf einer Seite lesen

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. […] 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 […]