Wer eine Definition von SAT-Solver nachschlägt, erfährt, dass es sich um ein „Entscheidungsverfahren für das Erfüllbarkeitsproblem der Aussagenlogik“ handelt. Das klingt mehr nach Theorie als nach praktischem Einsatz. Tatsächlich versteckt sich hinter dem Begriff jedoch ein vielseitig einsetzbares Werkzeug.
Viele Probleme lassen sich leicht lösen, wenn man einfach alle Möglichkeiten durchprobieren könnte. Beispielsweise bei der Optimierung von Schichtplänen, Logistikrouten oder der Nutzung von Rechenkapazität, Lagerplatz oder anderen Ressourcen. Auch das Finden von Fehlern in Soft- und Hardware wäre leichter, wenn einfach alle Eingaben getestet werden könnten.
Alle Möglichkeiten durchzugehen braucht jedoch meistens viel zu lange. Oft kann hier ein SAT-Solver als Suchmaschine für Lösungen genutzt werden. Die Eingabe für den SAT-Solver ist eine Problembeschreibung und die Ausgabe ist die gesuchte Lösung oder eine Garantie, dass es keine solche Lösung gibt. Ausgehend von der Problembeschreibung, ist ein SAT-Solver selbständig in der Lage, Regeln zu finden, mit denen sich viele Möglichkeiten direkt ausschließen lassen um so schneller eine Lösung zu finden.
Damit ein SAT-Solver eingesetzt werden kann, muss jedoch die Problembeschreibung in eine Form gebracht werden, die der SAT-Solver versteht: die Aussagenlogik. In diesem Vortrag geht es daher um Techniken die dabei helfen Probleme in Aussagenlogik zu formulieren. Das ganze werde ich auch an einem Beispiel demonstrieren. [Der Quellcode zum praktischen Beispiel liegt bei GitHub](https://github.com/jix/sat-intro-nook).
Anschließend erkläre ich in dem nachfolgenden Vortrag wie SAT-Solver funktionieren.