Erfüllbarkeitsproblem der Aussagenlogik

Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von englisch satisfiability‚ Erfüllbarkeit‘) ist ein Entscheidungsproblem der theoretischen Informatik. Es beschäftigt sich mit der Frage, ob eine gegebene aussagenlogische Formel erfüllbar ist. Mit anderen Worten: Existiert eine Belegung der Variablen von mit den Werten wahr oder falsch, sodass zu wahr ausgewertet wird? SAT gehört zur Komplexitätsklasse NP der Probleme, die von einer nichtdeterministischen Turingmaschine in polynomieller Zeit gelöst werden können. Außerdem war SAT das erste Problem, für das NP-Vollständigkeit nachgewiesen wurde (Satz von Cook). Damit kann jedes Problem aus NP in polynomieller Zeit auf SAT zurückgeführt werden (Polynomialzeitreduktion). NP-vollständige Probleme stellen also eine Art obere Schranke für die Schwierigkeit von Problemen in NP dar. Eine deterministische Turingmaschine (etwa ein konventioneller Computer) kann SAT in exponentieller Zeit entscheiden, zum Beispiel durch das Aufstellen einer Wahrheitstabelle. Es ist kein effizienter Algorithmus für SAT bekannt und es wird allgemein vermutet, dass ein solcher Polynomialzeitalgorithmus nicht existiert. Die Frage, ob SAT in polynomieller Zeit gelöst werden kann, ist äquivalent zum P-NP-Problem, einem der bekanntesten offenen Probleme der theoretischen Informatik Ein Großteil der Forschung beschäftigt sich mit der Entwicklung möglichst effizienter Verfahren zur Lösung von SAT in der Praxis (sogenannter SAT-Solver). Moderne SAT-Solver können Instanzen mittlerer Schwierigkeit mit hunderten Millionen Variablen oder Klauseln in praktikabler Zeit lösen. Das ist ausreichend für praktische Anwendungen, z. B. in der formalen Verifikation, in der künstlichen Intelligenz, in der Electronic Design Automation und in verschiedenen Planungs- und Schedulingalgorithmen. Sie gehören zu den Constraint Satisfaction Problems (CSP).