2019-11-09-einfuehrung-in-sat-solver-1.md

---
layout: video
release_date:   2019-12-15 20:00:00 +0200
recording_date: 2019-11-09 14:00:00 +0200
duration: "90:00"
room: AMS1
title:  "Einführung in SAT-Solver"
subtitle: "Was sind SAT-Solver und wie verwende ich diese?"
persons:
- "Jannis Harder"
fahrplan_url: https://2019.nook-luebeck.de/talks/einfuehrung-in-sat-solver-1/
#https://www.uuidgenerator.net/
uid: 10b03696-9475-4a3a-9cb1-23e22759b3d9
yt: "https://www.youtube.com/watch?v=3O-JWyO1u6o"
mccc: "https://media.ccc.de/v/einfuehrung-in-sat-solver-1"
file: "https://video.chaotikum.net/nook19/2019-11-09-nook-einfuehrung-in-sat-solver.mov"
event: f88922eb-871a-4ada-b952-588332887768
conferences:
- nook2019
- nook
---
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.