Erfüllbarkeitsproblem der Aussagenlogik

aus Wikipedia, der freien Enzyklopädie

Du hast neue Nachrichten (Unterschied zur vorletzten Version).

Das Erfüllbarkeitsproblem der Aussagenlogik (oft mit SAT vom Englischen satisfiability notiert) ist ein Entscheidungsproblem der Aussagenlogik. Es fragt, ob eine aussagenlogische Formel erfüllbar ist. Anwendungen davon finden sich unter anderem in der Komplexitätstheorie, Verifikation und im Entwurf von logischen Schaltungen. Insbesondere in der Komplexitätstheorie wird mit SAT auch nur der Spezialfall von Formeln bezeichnet, die in konjunktiver Normalform vorliegen.

Das Erfüllbarkeitsproblem der Aussagenlogik ist NP-vollständig. Anfang der 1970er Jahre zeigten Stephen A. Cook und Lenonid Levin unabhängig voneinander diese Eigenschaft. Ein Problem einer Komplexitätsklasse ist vollständig, wenn man jedes andere Problem dieser Klasse durch eine Polynomialzeitreduktion auf das vollständige Ursprungsproblem (oftmals SAT) übersetzen kann. Cook zeigte hierfür einen Algorithmus auf, mit dem die Berechnungsschritte einer nicht-deterministischen Turingmaschine simuliert werden können. Richard Karp zeigte 1972 die NP-Vollständigkeit weiterer Probleme. Er prägte damit das heutige Verständnis von NP-Vollständigkeit.

NP-Vollständigkeit ist ein Hilfsmittel der Komplexitätstheorie. Da es bis heute keinen Beweis gibt, dass $\mathcal{P} \neq \mathcal{NP}$ (siehe P/NP-Problem), benutzt man die Eigenschaft der NP-Vollständigkeit: Ist ein Problem NP-vollständig, so ist es mit großer Wahrscheinlichkeit nicht in $\mathcal{P}$ , nämlich dann, wenn die Annahme stimmt, dass $\mathcal{P}$ eine echte Teilmenge von $\mathcal{NP}$ ist.

In der Informatik wird SAT intensiv untersucht. Es gibt viele Arbeitsgruppen, die sich mit der Erforschung der Struktur dieses Problems beschäftigen und neue Verfahren für sogenannte SAT-Solver entwickeln. Dies sind Algorithmen bzw. Programme, die möglichst schnell entscheiden sollen, ob eine aussagenlogische Formel erfüllbar ist oder nicht.

[Bearbeiten] Varianten von SAT

SAT kann auf viele Weisen durch Einschränkungen und Verallgemeinerungen variiert werden. Das Problem 3-SAT ist eine Variante, die ebenfalls NP-vollständig ist, da sich SAT in polynomieller Zeit auf 3-SAT reduzieren lässt. Somit ist auch 3-SAT NP-vollständig.

Jedes 3-SAT mit p Variablen und q Klauseln lässt sich auf einen Graphen G mit p+q Knoten abbilden, in dem alle Variablenknoten mit denjenigen Klauselknoten verbunden sind, in denen sie vorkommen. Eine Formel ist in P3SAT, wenn sie in 3-SAT ist, und der Graph planar ist. Auch P3SAT ist NP-vollständig.

Zu vielen weiteren Komplexitätsklassen gibt es Varianten von SAT, die bezüglich dieser Klassen vollständig sind. Beispielsweise führt die Einführung von Quantoren zu QBF (auch QSAT genannt), einem PSPACE-vollständigen Problem.