SAT (für satisfiability) ist der Name des bekanntesten NP-vollständigen Problems, des Erfüllbarkeitsproblems der Aussagenlogik. Gegeben ist hierbei eine Formel mit Boole'schen Variablen und Verknüpfungen und gesucht wird eine 'Lösung', also eine Wertezuweisung an die Variablen, so dass die Formel wahr wird. Dieses algorithmische Problem ist Dreh- und Angelpunkt für alle NP-Vollständigkeitsnachweise und wurde schon als 'Drosophila' der Algorithmik bezeichnet. Für SAT werden seit einiger Zeit leis ...