Antworten
Das Erfüllbarkeitsproblem der Aussagenlogik (kurz SAT, für Satisfiability) ist ein zentrales Entscheidungsproblem der theoretischen Informatik, bei dem geprüft wird, ob eine gegebene aussagenlogische Formel durch eine bestimmte Belegung ihrer Variablen (wahr/falsch) insgesamt wahr wird. Ist dies möglich, ist die Formel erfüllbar; andernfalls ist sie unerfüllbar.
Das Erfüllbarkeitsproblem der Aussagenlogik (SAT-Problem) untersucht, ob es für eine gegebene aussagenlogische Formel eine Belegung der Variablen gibt, die die Formel wahr macht. Eine Formel ist erfüllbar, wenn mindestens eine solche Belegung existiert, andernfalls unerfüllbar.
Beispiel: Die Formel (A∨B)∧(¬A∨C)(A∨B)∧(¬A∨C) ist erfüllbar, etwa wenn A=wahrA=wahr gesetzt wird.
SAT ist das erste bekannte NP-vollständige Problem und spielt eine zentrale Rolle in der theoretischen Informatik. Es gibt keine bekannte effiziente Lösung für alle Fälle, doch Lösungen lassen sich schnell überprüfen.
Praktisch wird SAT in Bereichen wie automatischem Theorembeweis, Software- und Hardware-Verifikation, Planung und künstlicher Intelligenz eingesetzt. Moderne SAT-Solver verwenden heuristische Algorithmen, um große Formeln effizient zu bearbeiten.
Kurz: Das Erfüllbarkeitsproblem entscheidet, ob eine logische Formel durch eine Variablebelegung wahr wird – eine grundlegende Frage für Logik, Komplexität und Anwendungen.
