Erfüllbarkeitsproblem der Aussagenlogik
Das Erfüllbarkeitsproblem der Aussagenlogik (oft mit SAT von englisch satisfiability notiert) beschäftigt sich innerhalb der Logik mit der Frage, 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.
Durch den Beweis, dass das Erfüllbarkeitsproblem der Aussagenlogik NP-vollständig ist, zeigte Stephen A. Cook diese Eigenschaft eines Problems zum ersten Mal anhand eines realen Problems und erleichterte damit alle nachfolgenden Beweise der NP-Vollständigkeit.
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 (Algorithmen bzw. Programme, die möglichst schnell entscheiden sollen, ob eine aussagenlogische Formel erfüllbar ist oder nicht) entwickeln.
SAT kann auf viele Weisen durch Einschränkungen und Verallgemeinerungen variiert werden. Das Problem 3-SAT ist eine Variante, die sich in polynomieller Zeit auf SAT reduzieren lässt. Es ist deshalb auch 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ändigem Problem.