Im theoretischen Informatikunterricht lernt man Probleme kennen, die
lassen sich im allgemeinen gar nicht mit einer automatischen
Rechenmaschine lösen. Das klassische Beispiel dafür ist das
Halteproblem: Es gibt keinen Algorithmus, der für jedes gegebene
Programm entscheiden kann, ob das Programm für eine gegebene Eingabe
anhält und ein Ergebnis produziert oder ob das Programm sich in einer
Endlosschleife verfängt. Alle Probleme dieser Art nennt man
„unentscheidbar“. Unter den entscheidbaren Problemen macht man dann
noch die Unterscheidung, wie aufwendig deren Lösung inhärent
ist. Eine Klasse von sehr aufwendigen Problemen nennt sich
NP-vollständig. Das prototypische NP-vollständige Problem ist das
sog. Erfüllbarkeitsproblem der Aussagenlogik – kurz SAT. Das
SAT-Problem ist eine Formel bestehend aus Variablen und logischen
Verknüpfungen, so was wie a oder (b und (nicht b)). Ein
SAT-Algorithmus nimmt so eine Formel und entscheidet, ob es eine
Variablenbelegung gibt (hier gibt‘s eine, nämlich a = wahr und b =
wahr), die die Formel zu wahr äquivalent macht. Nun sind die
NP-vollständigen Probleme in der Theorie sehr aufwendig zu lösen, aber
das bezieht sich zum einen nur auf die asymptotische Laufzeit (wo
skalare Faktoren vernachlässigt werden) und zum anderen nur auf den
denkbar schlechtesten Fall. Für jeden gegebenen Algorithmus, der
bspw. das SAT-Problem löst, lassen sich Eingaben finden, für die
dieser Algorithmus ewig braucht. Ob solche hinkonstruierten Probleme
im praktischen Einsatz wirklich auftreten, ist eine andere
Frage. Insbesondere für SAT gibt es SAT-Solver, die bei den
meisten praxisrelevanten Probleme schnell Lösungen finden.
Das SAT-Problem ist nicht nur in der theoretischen Informatik
interessant, sondern es hat eine ganz praktische Relevanz für das
allgemeine Softwareentwicklungsvorhaben. In einem früheren
Artikel
habe ich bereits gezeigt, wie sich SAT-Solver einsetzen lassen, um
Resourcenplanungsprobleme zu beackern. Dort kam
z3 zum Einsatz als direkter
Bestandteil der Software im Betrieb. z3 wird außerdem eingesetzt als
Bestandteil von Programmiersprachen, z.B. bei Liquid Haskell. In
diesem Artikel will ich zeigen, dass z3 darüberhinaus auch als
eigenständiges Werkzeug während der Design- und Entwicklungsphase sehr
nützlich ist – vergleichbar mit Bleistift und Blankopapier.