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.

Häufig, 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. Stephen A. Cook und Lenonid Levin zeigten (unabhängig voneinander) diese Eigenschaft Anfang der 1970er Jahre. 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 $\backslash mathcal\{P\}\; \backslash neq\; \backslash 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 $\backslash mathcal\{P\}$ (nämlich dann, wenn die Annahme stimmt, dass $\backslash mathcal\{P\}$ eine echte Teilmenge von $\backslash mathcal\{NP\}$ ist).

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.

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.

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ändigem Problem.

Siehe auch

• Resolution (Logik)
• Satz von Cook

Komplexitätstheorie | Logik

Boolean satisfiability problem | Problema de satisfacibilidad booleana | Problème SAT | SAT | 充足可能性問題 | ปัญหาความสอดคล้องแบบบูล