Wie viele DVDs darf man höchstens leihen?
Ein Solver ist ein Programm, das zu einer Menge von Regeln Werte findet, die alle Regeln erfüllen, oder meldet, dass es keine gibt. Damit lässt sich eine Behauptung beweisen, ohne einen einzigen Fall durchzuprobieren.
Eine Hochschulbibliothek erlaubt höchstens 5 Medien zugleich und verlangt mindestens 2 Bücher. Folgt daraus, dass niemand mehr als 3 DVDs hat? Der Solver Z3 beantwortet das in einem Augenblick.
Am Ende dieser Lektion
Notiz
Ich kann Z3 fragen, ob eine Behauptung immer gilt.
Schlüsselwörter
| Begriff | Was er bedeutet | Beispiel |
|---|---|---|
| Solver | ein Programm, das Werte für eine Menge von Regeln sucht | Z3 |
| Behauptung | eine Aussage, die aus den Regeln folgen soll | |
| Erfüllbar (sat) | es gibt Werte, die alle Regeln erfüllen | |
| Unerfüllbar (unsat) | es gibt keine solchen Werte | |
| Negation | das Gegenteil einer Aussage | not (y > 3) |
| Modell | die Werte, die der Solver bei sat nennt |
Die Zellen, die Lernende ausfüllen, bleiben in dieser Vorschau leer.
Z3 sucht Werte, die alle Regeln erfüllen
Sie beschreiben Z3 ein Problem in drei Schritten. declare-const legt eine Zahl an, assert fügt eine Regel hinzu, check-sat fragt, ob es Werte gibt.
Z3 schreibt Rechnungen mit dem Zeichen zuerst: (> x 3) heißt x > 3. Antwortet Z3 mit sat, kann get-value die gefundenen Werte zeigen.
So liest man die Eingabesprache von Z3
| In Z3 | Gewohnt | Bedeutung |
|---|---|---|
| (> x 3) | x > 3 | x ist größer als 3 |
| (<= (+ x y) 5) | x + y <= 5 | zusammen höchstens 5 |
| (not (> y 3)) | nicht y > 3 | das Gegenteil |
| (declare-const x Int) | x ist ganze Zahl | legt x an |
Die Zellen, die Lernende ausfüllen, bleiben in dieser Vorschau leer.
Gibt es ein x zwischen 3 und 5?
printf '(declare-const x Int)\n(assert (> x 3))\n(assert (< x 5))\n(check-sat)\n(get-value (x))\n' | z3 -inHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Gibt es ein x zwischen 3 und 4?
printf '(declare-const x Int)\n(assert (> x 3))\n(assert (< x 4))\n(check-sat)\n' | z3 -inHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Eine Behauptung beweist man über ihr Gegenteil
Um zu beweisen, dass eine Behauptung aus den Regeln folgt, fragen Sie Z3 nach dem Gegenteil. Gibt es Werte, die alle Regeln erfüllen und die Behauptung brechen?
Antwortet Z3 unsat, gibt es keine, und die Behauptung ist bewiesen. Antwortet es sat, zeigt das Modell ein Gegenbeispiel.
Bücher x und DVDs y in der Bibliothek
| Schritt | Behauptung: höchstens 3 DVDs | Behauptung: höchstens 2 DVDs |
|---|---|---|
| Regeln | x >= 2 und x + y <= 5 | x >= 2 und x + y <= 5 |
| Gegenteil dazu | y > 3 | y > 2 |
| Antwort von Z3 | unsat | sat mit x = 2 und y = 3 |
| Ergebnis | bewiesen | widerlegt |
Die Zellen, die Lernende ausfüllen, bleiben in dieser Vorschau leer.
Das Gegenteil von höchstens 3 DVDs
printf '(declare-const x Int)\n(declare-const y Int)\n(assert (>= x 2))\n(assert (<= (+ x y) 5))\n(assert (> y 3))\n(check-sat)\n' | z3 -inHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Das Gegenteil von höchstens 2 DVDs
printf '(declare-const x Int)\n(declare-const y Int)\n(assert (>= x 2))\n(assert (<= (+ x y) 5))\n(assert (> y 2))\n(check-sat)\n(get-value (x y))\n' | z3 -inHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Ein häufiger Fehler
Warnung
Viele denken: unsat heißt, die Behauptung ist falsch. Beim Gegenteil einer Behauptung ist es umgekehrt. unsat sagt dort: Das Gegenteil ist unmöglich, also stimmt die Behauptung.
Zwei Fallen: widersprüchliche Regeln und leere Behauptungen
Widersprechen sich die Regeln, ist jedes Gegenteil unsat, denn nichts erfüllt sie. Dann ist jede Behauptung „bewiesen“, auch eine absurde. Fragen Sie deshalb einmal nur nach den Regeln: Antwortet Z3 dort mit sat, passen sie zusammen.
Eine Behauptung, die immer stimmt, beweist ebenso nichts. Ihr Gegenteil ist auch ohne Regeln unsat.
Regeln, die sich widersprechen
printf '(declare-const x Int)\n(declare-const y Int)\n(assert (>= x 2))\n(assert (<= x 1))\n(assert (> y 100))\n(check-sat)\n' | z3 -inHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Eine Behauptung, die immer stimmt
printf '(declare-const y Int)\n(assert (not (or (> y 3) (<= y 3))))\n(check-sat)\n' | z3 -inHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Weiterführend
Schreiben Sie die Regeln einer eigenen Ausleihe, etwa für Laptops und Ladekabel in einem Rechenzentrum, als Z3-Eingabe. Fragen Sie erst nach den Regeln allein. Formulieren Sie dann zwei Behauptungen, eine wahre und eine falsche.
Prüfen Sie beide. Lesen Sie bei der falschen das Modell als Gegenbeispiel.