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 ${\displaystyle F}$ erfüllbar ist. Mit anderen Worten: Existiert eine Belegung der Variablen von ${\displaystyle F}$ mit den Werten wahr oder falsch, sodass ${\displaystyle F}$ 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).

1. ↑ SAT Competition 2020. Abgerufen am 9. November 2020. 
2. ↑ Randal E. Bryant, Steven German, Miroslav N. Velev: Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions. In: Lecture Notes in Computer Science. Springer, Berlin / Heidelberg 1999, ISBN 3-540-66086-0, S. 1–13. 
3. ↑ Henry Kautz, Bart Selman: Planning as satisfiability. In: Proceedings of the 10th European conference on Artificial intelligence (= ECAI ’92). John Wiley & Sons, Wien 1992, ISBN 0-471-93608-1, S. 359–363, doi:10.5555/145448.146725. 
4. ↑ João P. Marques-Silva, Karem A. Sakallah: Boolean satisfiability in electronic design automation. In: Proceedings of the 37th Annual Design Automation Conference (= DAC ’00). Association for Computing Machinery, Los Angeles CA 2000, ISBN 1-58113-187-9, S. 675–680, doi:10.1145/337292.337611. 
5. ↑ Hong Huang, Shaohua Zhou: An efficient SAT algorithm for complex job-shop scheduling. In: Proceedings of the 2018 8th International Conference on Manufacturing Science and Engineering (ICMSE 2018). Atlantis Press, Paris 2018, ISBN 978-94-6252-502-3, doi:10.2991/icmse-18.2018.126.