Die Übung vor der ersten Vorlesung

Organisation

Hausaufgaben

WS 25: 1b, 5, 4a, 2.

  1. Pierluigi Crescenzi, Viggo Kann A compendium of NP optimization problems

    https://web.archive.org/web/20200227195925/http://www.nada.kth.se/~viggo/problemlist/compendium.html

    Beispiele:

    1. Minimum File Transfer Scheduling (node195).

    2. Minimum Dynamic Storage Allocation (node163).

    Erläutern Sie die Spezifikation an einem Beispiel. Geben Sie eine lösbare Instanz sowie dafür zwei Lösungen mit unterschiedlichem Maß an.

  2. Aufgabe: formalisieren Sie Math Magic Februar 2007.

    Was ist dabei für Springer und König einfacher als für Dame, Läufer, Turm?

    (allgemein für Math Magic: offene Fragen

    https://erich-friedman.github.io/mathmagic/unsolved.html)

  3. Aufgabe: formalisieren Sie Wolkenkratzer oder Towers (was ist der Unterschied?) https://www.janko.at/Raetsel/Wolkenkratzer https://www.chiark.greenend.org.uk/~sgtatham/puzzles/js/towers.html

    • \(B=\{0,1\dots,n-1\}\), Unbekannte: \(h_{x,y}\in B\) für \(x,y\in B\)

    • Constraint für eine Zeile \(x\): (entspr. für Spalte)

      \(\bigvee_{p\in\text{Permutationen}(0,\dots,n-1), p \text{kompatibel mit Vorgaben}} \bigwedge_{y\in\{0,\dots,n-1\}} (h_{x,y} = p(y))\)

      Bsp: \(n=4\), Vorgabe links 2, rechts 1, kompatibel sind \([0,2,1,3],[2,0,1,3],[2,1,0,3],[2,1,0,3]\).

    • diese Formel wird exponentiell groß (wg. Anzahl Permutationen),

      Folge-Aufgabe: geht das auch polynomiell?

    • Geben Sie eine Aufgabenstellung der Größe \(w\times w\) an mit \(4\cdot w\) Vorgaben (d.h., alle Vorgaben), die mehr als eine Lösung hat.

      …für \(w=4\), für größere \(w\) (einige, alle)

    • (offene Frage?) Geben Sie eine eindeutig lösbare Instanz mit möglichst wenigen Vorgaben an. (Sind \(w-1\) Vorgaben für \(w\times w\) immer möglich?)

  4. Modellierung von Puzzles (aus Tatham-Collection)

    1. geben Sie ein Modell an für Pegs (Solitaire). Hinweise:

      • Zustand \(=\) Boolesche Matrix,

      • Schritt \(=\) Relation zwischen Matrizen,

      • Lösung \(=\) Schrittfolge (\(\Rightarrow\) Zustandsfolge). Wieviele Schritte?

    2. Modell für Unruly. (keine Zustandsfolge, sondern direkt die Lösung. Welches sind die Unbekannten, welches sind ihre Beziehungen, untereinander und zur Vorgabe)

    3. modellieren Sie Untangle

    Vergleichen Sie mit den tatsächlichen Quelltexten

    https://git.tartarus.org/?p=simon/puzzles.git

  5. Constraint für monotone kompatible Bewertungsfunktion:

    • lösen Sie mit Z3 (ist im Pool installiert, vgl. https://www.imn.htwk-leipzig.de/~waldmann/etc/pool/)

    • eine kleinste Lösung finden (Summe von \(P,Q,R,S\) möglichst klein) — dafür Assert(s) hinzufügen.

    • Abstieg der so gefundenen Bewertungsfunktion nachrechnen für \(abab\to baab \to baba\to bbaa\)

    • gibt diese Bewertungsfunktion die maximale Schrittzahl genau wieder? (nein)

    • Folge-Aufgabe: entspr. Constraint-System für Bewertungsfunktion für \(ab\to bba\) aufstellen und lösen.

Einleitung

Formale Methoden und Werkzeuge …

Die Rolle der Abstraktion

Industrielle Anwendungen von FMW

Industrielle Anwendungen von FMW

Anwendung: Polynom-Interpretationen

Constraint-Programmierung—Beispiel

(set-logic QF_NIA)(set-option :produce-models true)
(declare-fun P () Int) (declare-fun Q () Int)
(declare-fun R () Int) (declare-fun S () Int)
(assert (and (< 0 P) (<= 0 Q) (< 0 R) (<= 0 S)))
(assert (> (+ (* P S) Q) (+ (* R Q) S)))
(check-sat)(get-value (P Q R S))

Constraints in der Unterhaltungsmathematik

Wettbewerbe für Constraint-Solver

Gliederung der Vorlesung

Organisatorisches

Literatur

Hausaufgaben

WS 25: 1b, 5, 4a, 2.

  1. Pierluigi Crescenzi, Viggo Kann A compendium of NP optimization problems

    https://web.archive.org/web/20200227195925/http://www.nada.kth.se/~viggo/problemlist/compendium.html

    Beispiele:

    1. Minimum File Transfer Scheduling (node195).

    2. Minimum Dynamic Storage Allocation (node163).

    Erläutern Sie die Spezifikation an einem Beispiel. Geben Sie eine lösbare Instanz sowie dafür zwei Lösungen mit unterschiedlichem Maß an.

  2. Aufgabe: formalisieren Sie Math Magic Februar 2007.

    Was ist dabei für Springer und König einfacher als für Dame, Läufer, Turm?

    (allgemein für Math Magic: offene Fragen

    https://erich-friedman.github.io/mathmagic/unsolved.html)

  3. Aufgabe: formalisieren Sie Wolkenkratzer oder Towers (was ist der Unterschied?) https://www.janko.at/Raetsel/Wolkenkratzer https://www.chiark.greenend.org.uk/~sgtatham/puzzles/js/towers.html

    • \(B=\{0,1\dots,n-1\}\), Unbekannte: \(h_{x,y}\in B\) für \(x,y\in B\)

    • Constraint für eine Zeile \(x\): (entspr. für Spalte)

      \(\bigvee_{p\in\text{Permutationen}(0,\dots,n-1), p \text{kompatibel mit Vorgaben}} \bigwedge_{y\in\{0,\dots,n-1\}} (h_{x,y} = p(y))\)

      Bsp: \(n=4\), Vorgabe links 2, rechts 1, kompatibel sind \([0,2,1,3],[2,0,1,3],[2,1,0,3],[2,1,0,3]\).

    • diese Formel wird exponentiell groß (wg. Anzahl Permutationen),

      Folge-Aufgabe: geht das auch polynomiell?

    • Geben Sie eine Aufgabenstellung der Größe \(w\times w\) an mit \(4\cdot w\) Vorgaben (d.h., alle Vorgaben), die mehr als eine Lösung hat.

      …für \(w=4\), für größere \(w\) (einige, alle)

    • (offene Frage?) Geben Sie eine eindeutig lösbare Instanz mit möglichst wenigen Vorgaben an. (Sind \(w-1\) Vorgaben für \(w\times w\) immer möglich?)

  4. Modellierung von Puzzles (aus Tatham-Collection)

    1. geben Sie ein Modell an für Pegs (Solitaire). Hinweise:

      • Zustand \(=\) Boolesche Matrix,

      • Schritt \(=\) Relation zwischen Matrizen,

      • Lösung \(=\) Schrittfolge (\(\Rightarrow\) Zustandsfolge). Wieviele Schritte?

    2. Modell für Unruly. (keine Zustandsfolge, sondern direkt die Lösung. Welches sind die Unbekannten, welches sind ihre Beziehungen, untereinander und zur Vorgabe)

    3. modellieren Sie Untangle

    Vergleichen Sie mit den tatsächlichen Quelltexten

    https://git.tartarus.org/?p=simon/puzzles.git

  5. Constraint für monotone kompatible Bewertungsfunktion:

    • lösen Sie mit Z3 (ist im Pool installiert, vgl. https://www.imn.htwk-leipzig.de/~waldmann/etc/pool/)

    • eine kleinste Lösung finden (Summe von \(P,Q,R,S\) möglichst klein) — dafür Assert(s) hinzufügen.

    • Abstieg der so gefundenen Bewertungsfunktion nachrechnen für \(abab\to baab \to baba\to bbaa\)

    • gibt diese Bewertungsfunktion die maximale Schrittzahl genau wieder? (nein)

    • Folge-Aufgabe: entspr. Constraint-System für Bewertungsfunktion für \(ab\to bba\) aufstellen und lösen.

Erfüllbarkeit aussagenlogischer Formeln (SAT)

Aussagenlogik: Syntax

aussagenlogische Formel:

damit auch Quantifikation über endlichen Bereich \(E\)

\((\forall x\in E: F)\) ist (endliche!) Konjunktion \(\bigwedge_{x\in E} F\)

Aussagenlogik: Semantik

Formulierung von SAT-Problemen mit Ersatz

Benutzung von SAT-Solvern

SAT-Modellierung für das \(N\)-Damen-Problem

stelle möglichst viele Damen auf \(N\times N\)-Schachbrett,
die sich nicht gegenseitig bedrohen.

wir schreiben Programm,

\(N\)-Damen mit Ersatz

Zusammenfassung Ersatz (bisher)

Modellierung durch SAT: Ramsey

gesucht ist Kanten-2-Färbung des \(K_5\) ohne einfarbigen \(K_3\).

das ist ein Beispiel für ein Ramsey-Problem

(F. P. Ramsey, 1903–1930) http://www-groups.dcs.st-and.ac.uk/~history/Biographies/Ramsey.html

diese sind schwer, z. B. ist bis heute unbekannt: gibt es eine Kanten-2-Färbung des \(K_{43}\) ohne einfarbigen \(K_{5}\)?

http://www1.combinatorics.org/Surveys/ds1/sur.pdf

SAT-Modell für Peg-Solitaire

Hausaufgaben

WS 25: 2,3,4 (5, 7, 8 siehe Repo)

  1. unterschiedliche Halbringe auf zwei Elementen?

  2. für die Formel \(S(b,h)\) (abhängig von Parametern \(b,h\in \mathbb{N}\))

    Variablen: \(v_{x,y}\) für \(1\le x\le b, 1\le y \le h\)

    Constraints:

    • für jedes \(x\) gilt: wenigstens einer von \(v_{x,1},v_{x,2},\dots,v_{x,h}\) ist wahr

    • und für jedes \(y\) gilt: höchstens einer von \(v_{1,y},v_{2,y},\dots,v_{b,y}\) ist wahr

    1. unter welcher Bedingung an \(b,h\) ist \(S(b,h)\) erfüllbar?

      Für den erfüllbaren Fall: geben Sie ein Modell an.

      Für den nicht erfüllbaren Fall: einen Beweis.

    2. Erzeugen Sie (eine konjunktive Normalform für) \(S(b,h)\) durch ein Programm (Sprache/Bibliothek beliebig)

      ( \(b,h\) von der Kommandozeile, Ausgabe nach stdout)

    3. Lösen Sie \(S(b,h)\) durch minisat (kissat, Z3, …), vergleichen Sie die Laufzeiten (auch im nicht erfüllbaren Fall).

  3. Für \(S(b,h)\) (vorige Aufgabe): Formel-Konstruktion, Löser-Aufruf mit Ersatz.

    • \(v\) vom Typ Relation Int Int (vgl. \(N\) Damen)

    • für jedes \(x\): verwenden Sie rows

    • für jedes \(y\): schreiben und verwenden Sie entsprechende Fkt. columns

    • höchstens einer: verwenden Sie keine zwei.

  4. Für \(a,b\ge 2\): die Ramsey-Zahl \(R(a,b)\) ist die kleinste Zahl \(n\), für die gilt: jede rot-blau-Kantenfärbung eines \(K_n\) enthält einen roten \(K_a\) oder einen blauen \(K_b\).

    (Der Satz von Ramsey ist, daß es für jedes \(a,b\) tatsächlich solche \(n\) gibt.)

    1. Beweisen Sie:

      1. \(R(a,b)=R(b,a)\)

      2. \(R(2,b)=b\)

      3. \(R(a+1,b+1)\le R(a,b+1)+R(a+1,b)\)

        (das liefert einen Beweis des Satzes von Ramsey)

      4. wenn dabei beide Summanden rechts gerade Zahlen sind, dann \(R(a+1,b+1)< \dots\)

    2. Bestimmen Sie damit obere Schranken für \(R(3,3), R(3,4), R(4,4)\) und vergleichen Sie mit den unteren Schranken durch SAT-Kodierung.

  5. SAT-Kodierung für \(R(a,b)\) mit Ersatz:

    • main = ramsey 3 3 5

ramsey a b n = do
  out <- solveWith (cryptominisat5Path "kissat") $ do
    r <- R.symmetric_relation ((1,1),(n,n))
    assert $ flip all (subs a [1 .. n]) $ \ c ->
      flip any (subs 2 c) $ \ [x,y] ->
         r R.! (x,y)
    assert $ flip all (subs b [1 .. n]) $ \ c ->
      flip any (subs 2 c) $ \ [x,y] ->
         not $ r R.! (x,y)
    return r
  ...

    • Hilfsfunktion: verteilten Teilfolgen gegebener Länge:

      Beispiel: subs 3 [1,2,3,4,5] = [[1,2,3],[1,2,4],[1,2,5],...,[3,4,5]] (nicht notwendig in dieser Reihenfolge)

      subs :: Int -> [a] -> [[a]]
subs 0 xs = [ [] ]  ;   subs k [] = []
subs k (x:xs) = map _  _  <> subs k xs

      mit subs a [1 .. n] zur Auswahl des \(K_a\) sowie subs 2 c zur Auswahl der Kanten.

    • Diskutieren Sie Existenz (obere Schranke) und SAT-Kodierung für dreifarbigen Ramsey:

      \(R(a,b,c):=\) das kleinste \(n\) mit: jeder Kanten-3-Färbung des \(K_n\) enthält einen roten \(K_a\) oder einen grünen \(K_b\) oder einen blauen \(K_c\).

      Ergänzen und beweisen: \(R(a,b,c)\le R(a,R(b,c))\), anwenden für \(R(3,3,3)\).

  6. Modellierung als aussagenlogisches Constraint:

    Vorgehen bei Modellierung:

    • welches sind die Unbekannten, was ist deren Bedeutung?

      (Wie rekonstruiert man eine Lösung aus der Belegung, die der Solver liefert?)

    • welches sind die Constraints?

      (wie stellt man sie in CNF dar? — falls nötig)

  7. Unruly (S. Tatham Puzzles)

    u1 = M.fromList -- eine Aufgabe (8 x 8)
  $ map (,False) [(1,7),(3,2),(5,1),(5,3),(5,4),(5,7),(6,7)]
  <> map (,True) [(1,4),(6,2),(6,3),(7,5),(8,4),(8,5)]
unruly u = do
  let bnd = ((1,1),(8,8))
  out <- solveWith (cryptominisat5Path "kissat") $ do
    b <- R.relation bnd
    assert $ flip all (M.toList u) $ \ (k,v) ->
      b R.! k === encode v
    assert $ flip all (rows b <> columns b) $ \ rc ->
      balanced rc && mixed 3 rc
    ...

    wie kann man feststellen, daß es genau eine Lösung gibt? (Solver nochmals aufrufen für modifizierte Formel.)

  8. Peg (S. Tatham Puzzles)

    peg b = do
  let bnd = ((1,1),(b,b))
      full = A.genArray bnd $ \ i -> True
      start :: A.Array (Int,Int) Bool
      start = full A.// [((1,2), False)]
  out <- solveWith (cryptominisat5Path "kissat") $ do
    boards <- replicateM (b*b - 1) $ R.relation bnd
    assert $ R.equals (head boards) (encode start)
    assert $ all step $ zip boards $ drop 1 boards
    return boards
  ...
type Board = R.Relation Int Int

step :: (Board, Board) -> Bit
move :: Board -> (Int,Int) -> (Int,Int) -> Board -> Bit

Anwendg.: Bounded Model Checking

Begriff, Motivation

Literatur, Software

BMC für Mutual Exclusion-Protokolle

System mit zwei (gleichartigen) Prozessen \(A,B\):

A0: maybe goto A1
A1: if l goto A1 else goto A2
A2: l := 1; goto A3
A3: [critical;] goto A4
A4: l := 0; goto A0

B0: maybe goto B1
B1: if l goto B1 else goto B2
B2: l := 1; goto B3
B3: [critical;] goto B4
B4: l := 0; goto B0

Schließen sich A3 und B3 gegenseitig aus? (Nein.)

(nach: Donald E. Knuth: TAOCP, Vol. 4 Fasz. 6, S. 20ff)

Modell: Zustandsübergangssystem

Zustände:

Übergangsrelation (nichtdeterministisch): für \(P\in \{A,B\}\):

Aussagenlog. Formel für \(I \to^{\le k} F\) angeben,

deren Erfüllbarkeit durch SAT- oder SMT-Solver bestimmen

One-Hot-Kodierung

Übung BMC

Anzahl-Constraints

Definition, Motivation

SAT-Kodierung eines Rösselsprungs

let n = height * width; places = [0 .. n-1]

let decode p = divMod p width
    edge p q =
        let (px,py) = decode p; (qx,qy) = decode q
        in  5 == (px-qx)^2 + (py-qy)^2
    rotate (x:xs) = xs <> [x]

a <- replicateM n $ replicateM n $ exists @Bit
assert $ all exactly_one a
assert $ all exactly_one $ transpose a
assert $ flip all (zip a $ rotate a) $ \ (e, f) ->
  flip all places $ \ p ->  e!!p  ==>
    flip any (filter (edge p) places) (\ q -> f!!q)

SAT-Kodierungen von AMO (I) (quad, lin)

SAT-Kodierungen von AMO (II) - log

SAT-Kodierungen von AMO (III) - sqrt

Listen (Generatoren) zur Programmablaufsteuerung

Matrizen als Listen von Listen

Quantifikation über Listen

Iterierte assoziative Verknüpfung

Aufgaben

WS 25: 2, 7, 11

  1. Modellierung Sudoku: Kodierung eines (ausgefüllten) Schemas durch \(9\times 9\times 9\) unbekannte Bit mit \(u_{x,y,z} \iff\) auf Koordinate \((x,y)\) steht Zahl \(z\).

    für welche Teilmengen gelten EXO-Constraints?

    Hinweis: für \(9^2 + 3\cdot 9^2\) Mengen, jede mit 9 Elementen.

  2. geben Sie Beispiele aus Rätsel-Sammlungen von Nikoli, Janko, Tatham, bei deren SAT-Kodierung AMO- oder EXO-Constraints vorkommen sollten

  3. Vergleiche Sie die commander-Kodierung für AMO von Klieber und Kwon, Int. Workshop Constraints in Formal Verification, 2007, mit Kodierungen aus dem Skript.

    a) auf dem Papier, b) praktisch: mit ersatz implementieren, Formelgrößen messen, auch nach Vorverarbeitung durch minisat

  4. für AMO-log: geben Sie eine Skolem-Funktion für \(\forall x_0,\ldots \exists h_0,\ldots:\ldots\) an.

    d.h., die eine erfüllende Belegung der \(h_i\) bestimmt, falls \(\textsf{AMO}(x_0,\dots)\) wahr ist.

  5. für \(\textsf{AMO}\) über \(2^k\) Argumente: verwenden Sie sqrt-Kodierung für Rechteck mit Abmessungen \(2 \times 2^{k-1}\), dann rekursiv über \(2^{k-1}\).

    Vergleichen Sie mit der log-Kodierung.

  6. für AMO-lin: untersuchen Sie den Unterschied zwischen der Verwendung von foldr (von rechts) und foldb (balanciert)

    welche Maße der erzeugten Formel stimmen überein, welche unterscheiden sich?

  7. vergleichen Sie Formelgrößen und Solver-Laufzeiten für unterschiedliche AMO-Kodierungen für die Spalten in den unlösbaren Schubfach-Formeln \(S(n+1,n)\).

  8. für die AMO-Kodierungen linear und sqrt: wie kann man mit möglichst wenig Zusatz-Aufwand EXO erhalten?

  9. ordnen Sie die EXO-Kodierung im Bounded Model Checker (boumchak) in die Systematik der VL ein.

  10. Für den Rösselsprung (Code in fmw-24/leap)

    • gegebene EXO-Implementierung diskutieren, durch andere ersetzen, Formelgröße/Solverlaufzeit beobachten

    • zusätzliches assert $ a !! 0 !! 0 diskutieren

    • andere Sprung-Distanzen (Giraffe usw., siehe unten)

    • Kamel (1,3)-Sprung (auf nur schwarzen? oder weißen?) Feldern implementieren

    • andere Kodierung für Hamiltonkreis: Neng-Fa Zhou: In Pursuit of an Efficient SAT Encoding for the Hamiltonian Cycle Problem, CP 2020, ModRef 2019, https://www.sci.brooklyn.cuny.edu/~zhou/

    • Anwendung: George Jelliss: Leapers at Large, 2001, 2022 http://www.mayhematics.com/t/pl.htm

      Resultate zur Existenz von Hamilton-Pfaden (HP) und -Kreisen (HC) nachrechnen und ergänzen, Bsp.:

      • HP für Giraffe \((1,4)\) auf 11\(\times\) 11?

        (Nein—unsat nach 6 Stunden)

      • HP für Zebra \((2,3)\) auf 13 \(\times\) 13?

      • HP für Antilope \((3,4)\) auf 20 \(\times\) 20?

      vgl. Donald Knuth: Leaper Graphs, 1994, https://arxiv.org/abs/math/9411240

  11. Plan SAT-Kodierung Skyline (Towers, Wolkenkratzer)

    Jede Zahl (jedes Haus) wird one-hot-kodiert, dann

    type Haus=[Bit];type Zeile=[Haus];type Stadt=[Zeile]

    • (ohne Vorgaben) welche AMO-Constraints gelten? Eine Matrix, die diese Constraints erfüllt, heißt lateinisches Quadrat (Anzahl der lateinischen Quadrate: https://oeis.org/A002860)

    • (mit Vorgaben) Implementieren Sie die Berechnung der (von links) sichtbaren Dächer einer Zeile sicht :: Zeile -> [Bit]. Das Resultat soll der Bitvektor \(s\) sein mit \(s_i\iff\) Dach der Höhe \(i\) ist sichtbar.

    • für die anderen Blickrichtungen: die Funktion sicht bleibt, die Stadt wird transformiert. Wie?

    • Benutzen Sie eine SAT-Kodierung, um zu beweisen: jedes lateinische Quadrate der Seitenlänge 6 enthält wenigstens eine Zelle, die von keiner Seite sichtbar ist.

  12. SAT-Kodierungen für das \(N\)-Damen-Problem:

    • naiv \(N^4\)

      für alle \(a\) aus Spielfeld: für alle \(b\) aus Spielfeld: sich \(a\) und \(b\) sehen, dann \(\neg a \vee \neg b\)

    • besser \(N^3\)

      für alle \(a\) aus Spielfeld: für alle \(b\), die von \(a\) gesehen werden: …

    • noch besser \(N^2\)

      AMO-Constraints (jeweils lineare Formelgröße) über geeigneten (linear vielen) Mengen

SAT: Normalformen, Transformationen

Normalformen (DNF, CNF)

Definitionen:

Disjunktion als Implikation: diese Formeln sind äquivalent:

Äquivalenzen

Erfüllbarkeits-Äquivalenz

Tseitin-Transformation

Tseitin-Transf. für Schaltkreise

Visualisierung von Schaltkreisen

Tseitin-Transformation in Ersatz (Bsp)

Abmessungen von Schaltkreisen

Abmessungen von Schaltkreisen: wozu?

Aufgaben zu Tseitin-Transformation

  1. für diese Formeln:

    • \((x_1 \leftrightarrow x_2) \leftrightarrow (x_3 \leftrightarrow x_4)\)

    • Halb-Adder (2 Eingänge \(x,y\), 2 Ausgänge \(r,c\))

      \((r\leftrightarrow (\neg(x\leftrightarrow y))) \wedge (c \leftrightarrow (x\wedge y))\)

    • Full-Adder (3 Eingänge, 2 Ausgänge)

    jeweils:

    • führe die Tseitin-Transformation durch

    • gibt es kleinere erfüllbarkeitsäquivalente CNF? (deren Modelle Erweiterungen der Original-Modelle sind)

  2. data Bit hat weitere Konstruktoren (Xor, Mux).

    Wo werden diese benutzt?

    Helfen sie tatsächlich bei der Erzeugung kleiner CNFs?

SAT-Solver

Spezifikation

Implementierung eines naiven SAT-Solvers

Lösungsverfahren

Evolutionäre Algorithmen für SAT

Lokale Suche (GSat, Walksat)

Bart Selman, Cornell University,
Henry Kautz, University of Washington

https://web.archive.org/web/20070311005144/http://www.cs.rochester.edu/u/kautz/walksat/

Algorithmus:

Problem: lokale Optima — Lösung: Mutationen.

DPLL

Davis, Putnam (1960), Logeman, Loveland (1962),

http://dx.doi.org/10.1145/321033.321034 http://dx.doi.org/10.1145/368273.368557

Zustand \(=\) partielle Belegung

DPLL-Begriffe

für partielle Belegung \(b\) (Bsp: \(\{(x_1,1),(x_3,0)\}\)): Klausel \(c\) ist

Eigenschaften: für CNF \(F\) und partielle Belegung \(b\):

DPLL-Algorithmus

Eingabe: CNF \(F\),
Ausgabe: Belegung \(b\) mit \(b\models F\) oder UNSAT.

\(\operatorname{DPLL}(b)\) (verwendet Keller für Entscheidungspunkte):

DPLL: Eigenschaften

wird bewiesen durch Invariante

Satz (Ü): für alle endlichen \(V\): \(<_\text{lex}\) ist eine wohlfundierte Relation auf der Menge der partiellen \(V\)-Belegungen:

DPLL-Beispiel

[[2,3],[3,5],[-3,-4],[2,-3,-4]
,[-3,4],[1,-2,-4,-5],[1,-2,4,-5]]

decide belegt immer die kleinste freie Variable, immer zunächst negativ

DPLL-Beispiel (Lösung)

[[2,3],[3,5],[-3,-4],[2,-3,-4]
,[-3,4],[1,-2,-4,-5],[1,-2,4,-5]]

[Dec (-1),Dec (-2),Prop 3,Prop (-4),Back
,Dec 2,Dec (-3),Prop 5,Prop (-4),Back
,Dec 3,Prop (-4),Back,Back,Back
,Dec 1,Dec (-2),Prop 3,Prop (-4),Back
,Dec 2,Dec (-3),Prop 5]

DPLL: Implement., Heuristik, Ergänzungen

Aufgaben

  1. Geben Sie eine erfüllbare CNF an, für die monotone lokale Suche

    improve n cnf b0 = ...
      let b1 = S.insert (negate l) $ S.delete l b0
      if badness cnf b1 <= badness cnf b0
        then improve n cnf b1
        else improve n cnf b0

    nicht funktioniert: es gibt eine Belegung \(b_0\), von der aus keine zulässige Schrittfolge zu einer erfüllenden Belegung führt. Hinweis: z.B., weil es überhaupt keine erlaubten Schritte gibt.

    Wie behandeln gsat/walksat diesen Fall?

  2. wenden Sie den SAT-Solver mit lokaler Suche auf realistische CNFs an, z.B. aus Kodierung Rösselsprung.

  3. wie werden in minisat (kissat, …) Einheits- und Konfliktklauseln erkannt? (Hinweis: two watched literals)

  4. unit propagation (UP) implementieren:

    • Einheitsklauseln erkennen:

      type Literal = Int
units :: CNF -> [Literal]
units [[1,2],[-3],[3,4]] = [-3]

    • ein Literal belegen:

      assign :: Literal -> CNF -> CNF
assign (-3) [[1,2],[-3],[3,4]] = [[1,2],[4]]

    Wo stehen die entsprechenden Funktionen im Quelltext der Autotool-Aufgabe zu DPLL?

SAT-Solver (fortgeschrittene Techniken)

Plan

Semantisches Folgern

Eigenschaften (Übungsaufgaben):

Resolution (Syntaktisches Schließen)

Variablen-Elimination durch vollst. Resolution

SAT-Lösen durch iterierte vollst. Resolution

DPLL mit CDCL (Plan)

conflict driven clause learning –

bei jedem Konflikt eine Klausel \(C\) hinzufügen, die

Eigenschaften/Anwendung:

Naives Lernen

Lernen (Implementierung) und Backjump

Beweise der Nichterfüllbarkeit

Widerlegungsvollständigkeit der Resolution

Die Größe von Widerlegungen

Aufgaben

  1. (Knuth Aufgabe 254) Für \(\{ 12, \overline{1} 3, 2\overline{3},\overline{2}\overline{4}, \overline{3}4\}\): nach der Entscheidung \(1\): welche Klausel wird gelernt?

    D. E. Knuth, TAOCP Vol. 4, Fasc. 6, Satisfiability, 2015.

  2. für die vorige CNF: lösen durch iterierte vollständige Elimination

  3. Schleife verlassen, wenn \(c\) nur noch ein Literal der aktuellen Entscheidungstiefe …:

    1. wieso ist die Bedingung anfangs falsch? (es kann nicht sein, daß die originale Konflikt-Klausel \(c\) gelernt wird)

    2. wieso wird diese Bedingung wahr? (es kann nicht sein, daß es immer \(\ge 2\) solche Literale sind oder plötzlich gar keines)

    3. wieso wird immer eine Klausel gelernt, die bisher nicht zur Klauselmenge gehört?

  4. (Knuth Aufgabe 378) blocked clause elimination:

    Für Klauselmenge \(F\): eine Klausel \(C=(l \vee l_1\vee \dots\vee l_k)\)

    heißt blockiert durch Literal \(l\),

    falls für jede Klausel \(D\in F\) mit \(\overline{l}\in D\) gilt: \(\exists i: \overline{l_i}\in D\).

    1. ein Beispiel angeben.

    2. beweisen: \(F\setminus\{C\}\) erfüllbar \(\Rightarrow\) \(F\) erfüllbar.

    3. ist jedes Modell \(b\) von \(F\setminus\{C\}\) auch ein Modell von \(F\)?

  5. hier besprochene Heuristiken und Ergänzungen

    • in den Protokollen von minisat, kissat wiederfinden

      (z.B. wieviele Klauseln werden gelernt? wie groß sind diese? wann vergessen?)

    • durch Optionen von kissat o. cadical an/abschalten

  6. conflict clause minimization (Sörenson, SAT 2005,

    http://minisat.se/downloads/MiniSat_v1.13_short.pdf):

    Ein Beispiel angeben.

  7. einen SAT-Solver, der UNSAT-Beweise ausgeben kann, auf Schubfach-Formeln anwenden und Beweis-Länge betrachten. (Diese sollte exponentiell ansteigen.)

  8. reverse unit propagation (RUP) für CNF \(M\), Klausel \(C\)

    \(\overline{C}:=\) die Menge der Negationen der Literale aus \(C\),

    \((M\cup\overline{C})\vdash_U \emptyset\), dabei nur unit-propagations-Schritte.

    1. Beweisen: dann folgt \(M\models C\). Beispiel angeben.

    2. Beispiel angeben für eine gültige Folgerung, die so nicht beweisbar ist (UP-Schritte reichen nicht aus)

    NB: in autotool-Aufgabe zu CDCL wird für (behauptete) gelernte Klausel geprüft, ob sie durch RUP folgt.

Bit-Blasting für Arithmetik

Bausteine für Zahlenrechnungen

Praktische Eigenschaften von Kodierungen (I)

Praktische Eigensch. (II) – Forcing

Aufgaben

  1. Ist die Kodierung des Halb-Addierers \(\textsf{HA}(x,y;c,r)\) durch \((r\leftrightarrow x \oplus y) \wedge (c \leftrightarrow x\wedge y)\) (Tseitin-Kodierung ohne weitere Hilfsvariablen) forcing?

    Ist die Kodierung des Voll-Addierers \(\textsf{FA}(x,y,z;c,r)\) durch \(\textsf{HA}(x,y;c_1,r_1)\wedge\textsf{HA}(r_1,z;c_2,r)\wedge (c\leftrightarrow c_1\vee c_2)\) forcing?

    Desgl. für die Kodierung von \(\textsf{ITE}(i,t,e;x)\) (if-then-else) durch \((i\wedge t\rightarrow x)\wedge (i\wedge \overline t\rightarrow \overline x) \wedge (\overline i\wedge e\rightarrow x)\wedge (\overline i\wedge \overline e\rightarrow \overline x)\)

    Lesen Sie dazu auch Een und Sörenson: Translating Pseudo-Boolean Constraints into SAT, JSAT 2006, (http://minisat.se/Papers.html) Abschnitt 5.1.

    Vergleichen Sie mit den Quelltexten von ersatz.

Binärzahlen, Vergleich, Addition

Anw.: Rösselsprung (alternative Kodierung)

Binäre Multiplikation

\([x_0,\ldots]_2 \cdot [y_0,\ldots]_2=[z_0,\ldots]_2\),

Anwendung: Anzahl-Constraints

Ausblick: Prädikatenlogik, SMT

Aufgaben

WS25: 3,4,6,7, 8

  1. zu alternative Kodierung Rösselsprung: welches Constraint-System entsteht, wenn die unbekannten \(t_p\) one-hot-kodiert werden?

  2. ist Implementierung von atmost-1, atmost-\(k\) durch binäre Addition forcierend?

  3. für Binärzahlen (Typ Bits): implementieren Sie

    • min, max

    • Vorgänger (:: Bits -> (Bits, Bit), zusätzlich ein Bit, das Unterlauf anzeigt, d.h., falls Argument \(=0\))

    • Auswahl (if-then-else :: Bit -> Bits -> Bits -> Bits)

  4. Kodierung von vorzeichenbehafteten Zahlen (mit variabler Bitbreite): zur Basis -2, Bsp. \(-5 = 1 -2 +4 -8= 1\cdot (-2)^0 + 1\cdot(-2)^1 + 1\cdot(-2)^3 + 1\cdot(-2)^3\)

    Instanzen für Ersatz (Codec, Equatable, Orderable, Num)

  5. benutzen Sie microsat (Repo dieser VL) (evtl. passend modifiziert), um experimentell zu überprüfen:

    • Konflikt wird durch UP erkannt?

      x <- unknown 10; y <- unknown 10
assert $ x + y /== y + x

    • Lösung wird durch UP bestimmt?

      x <- unknown 10;
assert $ encode 13 + x === encode 31

    ähnlich für Multiplikation

  6. Implementieren Sie die Multiplikation für Binarzahlen nach der Schulmethode. (Anders als plus:) Die Funktion times ist rekursiv und benutzt keine lokale Hilfsfunktion.

    times :: Boolean b => [b] -> [b] -> [b]
times [] ys = _
times (x:xs) ys = _

instance Num Nat where
  ...
  Nat xs * Nat ys = Nat (times xs ys)

    Anwendungen:

    • Finden Sie eine ganzzahlige Lösung von \(x^2 - Dy^2=1 \wedge y\neq 0\)

      für: \(D=5\), \(D=13\), \(D=61\), \(D=71\).

    • Finden Sie eine (oder die kleinste) natürliche Zahl, die auf zwei verschiedene Weisen als Summe von Kuben darstellbar ist.

  7. Implementieren Sie die Funktion sumBits :: [Bit] -> Nat mit der Eigenschaft: sumBits xs ist die (Binärdarstellung der) Anzahl der wahren Bit aus xs.

    Das geht offensichtlich mit foldl oder foldr, aber ein balaciertes fold ist besser, warum? (Betrachten Sie die notwendige und tatsächliche Bitbreite des Resultates.)

  8. (ab 1. Dez. 16 Uhr, täglich) https://www.mathekalender.de/wp/de/kalender/ Adventskalender, Technische Universität Berlin, The Berlin Mathematics Research Center MATH+

    In der Übung können jederzeit Aufgabenlösungen mit Methoden der Vorlesung präsentiert und diskutiert werden.

Prädikatenlogik

Übersicht

Syntax der Prädikatenlogik

Semantik der Prädikatenlogik

die Modell-Relation \((S,b) \models F\) sowie \(S\models F\)

Erfüllbarkeit, Allgemeingültigkeit (Def, Bsp)

SMT (SAT modulo Theory)

Beispiel

Bitvektor-Logik (QF_BV)

Definition SMT, Lösungsverfahren (Plan)

SMT-{LIB,COMP}

Beispiel queen10-1.smt2 aus SMT-LIB

(set-logic QF_IDL) (declare-fun x0 () Int)
(declare-fun x1 () Int) (declare-fun x2 () Int)
(declare-fun x3 () Int) (declare-fun x4 () Int)
(assert (let ((?v_0 (- x0 x4)) (?v_1 (- x1 x4))
(?v_2 (- x2 x4)) (?v_3 (- x3 x4)) (?v_4 (- x0 x1))
(?v_5 (- x0 x2)) (?v_6 (- x0 x3)) (?v_7 (- x1 x2))
(?v_8 (- x1 x3)) (?v_9 (- x2 x3))) (and (<= ?v_0 3)
(>= ?v_0 0) (<= ?v_1 3) (>= ?v_1 0) (<= ?v_2 3) (>=
?v_2 0) (<= ?v_3 3) (>= ?v_3 0) (not (= x0 x1))
(not (= x0 x2)) (not (= x0 x3)) (not (= x1 x2))
(not (= x1 x3)) (not (= x2 x3)) (not (= ?v_4 1))
(not (= ?v_4 (- 1))) (not (= ?v_5 2)) (not (= ?v_5
(- 2))) (not (= ?v_6 3)) (not (= ?v_6 (- 3))) (not
(= ?v_7 1)) (not (= ?v_7 (- 1))) (not (= ?v_8 2))
(not (= ?v_8 (- 2))) (not (= ?v_9 1)) (not (= ?v_9
(- 1)))))) (check-sat) (exit)

Umfang der Benchmarks (2014)

http://www.cs.nyu.edu/~barrett/smtlib/?C=S;O=D

QF_BV_DisjunctiveScheduling.zip           2.7G  
QF_IDL_DisjunctiveScheduling.zip          2.4G  
incremental_Hierarchy.zip                 2.1G  
QF_BV_except_DisjunctiveScheduling.zip    1.6G  
QF_IDL_except_DisjunctiveScheduling.zip   417M  
QF_LIA_Hierarchy.zip                      294M  
QF_UFLRA_Hierarchy.zip                    217M  
QF_NRA_Hierarchy.zip                      170M  
QF_LRA_Hierarchy.zip                      160M

Anwendung zur Terminations-Analyse

e-DSLs für Constraint-Prog.

Wiederholung: ersatz als e-DSL für SAT

Beispiel: Python-Bindung für Z3

Haskell-Bindungen für SMTLIB (Bsp. 1)

Haskell-Bindungen für SMTLIB (Bsp. 2)

Haskell-Bindungen für SMTLIB (Bsp. 3)

Aufgaben

WS 25: 1, 2, 3

  1. für jede der Logiken QF-LIA, LRA, NIA: ein kleines Constraint-System (mit kleinen Koeffizienten) angeben, das erfüllbar ist, aber nur durch Modelle mit sehr großen Zahlen.

  2. Bestimmen Sie:

    die kleinste natürliche Zahl, die sich auf zwei verschiedene Weisen als Summe von zwei Kuben schreiben läßt

    mit einem SMT-Solver. Schreiben Sie das Constraint-System von Hand. Benutzen Sie Logiken QF_NIA (Polynom-Arithmetik) (Warum nicht QF_LRA?)

    Hinweis: die Bedingung die kleinste kann man nicht hinschreiben, aber durch systematisches Probieren realisieren

  3. die vorige Aufgabe mit QF_BV (Bitvektoren). Dabei müssen Überläufe durch weitere Constraints verhindert werden. Wie geht das?

  4. Dieses Beispiel in QF_NIA ist wohl zu schwer für heutige Solver:

    Andrew R. Booker, Andrew V. Sutherland: On a question of Mordell, https://arxiv.org/abs/2007.01209

    John Pavlus: Sum-of-Three-Cubes Problem Solved for ‘Stubborn’ Number 33, https://www.quantamagazine.org/sum-of-three-cubes-problem-solved-for-stubborn-number-33-20190326/

  5. wählen Sie zufällig in SMTLIB eine (quantorenfreie) Logik und dort eine Benchmark. Erklären Sie die Benchmark.

    Beispiel: Queens (siehe Folie)

    Wenden Sie verschiedene SMT-Solver an (z.B. Z3, CVC5, opensmt) und vergleichen Sie Laufzeiten.

    Ändern Sie die Formel (vorsichtig), erläutern Sie die Änderungen der Belegung oder Erfüllbarkeit.

    Erzeugen Sie das Constraint durch Hasmtlib.

  6. die zitierte Hamiltonkreis-Kodierung (oder die früher zitierte MIP-Kodierung dafür) in SMTLIB-Syntax hinschreiben (in möglichst einfacher Logik) und ausprobieren.

  7. Eine kompatible arktische Matrix-Interpretation für \(aa\to aba\) (das Bsp. auf Folie) durch Lösen eines LIA-Systems bestimmen

    Desgl. für \(a^2 b^2\to b^3 a^3\) (größere Dimension verwenden).

    Warum gibt es keine solche Interpretation für \(ab\to ba\)?

    Hinweis: weil diese Regel quadratische lange Ableitungen gestattet (von welchen Startwörtern?),

    aber solche können bei arktischen Interpretationen nicht vorkommen (warum?)

  8. Adventskalender der DMV https://www.mathekalender.de/wp/de/kalender/

    Wenden Sie SAT oder SMT an, um Aufgaben zu modellieren und zu lösen.

DPLL(T) (Modulo Theories)

DPLL(T), Prinzip

für jedes T.Atom \(A = P(t_1,\ldots,t_k)\)
eine boolesche Unbek. \(p_A \leftrightarrow A\).

DPLL(T): Datenmodell, Semantik für Formel

DPLL(T): Datenmodell, Semantik für Lösung

DPLL(T): Einzelheiten, Beispiele

Lineare Gleichungen und Ungleichungen

Beispiel LP: monotone Interpretation

Beispiel LP-Solver

Syntax, Semantik

Beispiel: \(4y \le x \wedge 4x\le y-3 \wedge x+y \ge 1 \wedge x-y \ge 2\)

Semantik: Wertebereich für Unbekannte ist \(\mathbb{Q}\) (äquiv: \(\mathbb{R}\))

Normalformen

Lösung von linearen (Un-)Gl.-Sys. mit Methoden der linearen Algebra

Hintergründe

Warum funktioniert das alles?

Wann funktioniert es nicht mehr?

Lineare Gleichungssysteme

Lineare Ungleichungen und Optimierung

Entscheidungsproblem:

Optimierungsproblem:

Standard-Form des Opt.-Problems:
\(A\cdot x^T=b, x^T\ge 0\), minimiere \(c\cdot x^T\).

Ü: reduziere OP auf Standard-OP, reduziere EP auf OP

Lösungsverfahren für lin. Ungl.-Sys.

Fourier-Motzkin-Verfahren

Def.: eine Ungls. ist in \(x\)-Normalform, wenn jede Ungl.

Satz: jedes Ungls. besitzt äquivalente \(x\)-Normalform.

Def: für Ungls. \(U\) in \(x\)-Normalform:

\(U_x^\downarrow := \{ A \mid (x\ge A) \in U\},~ U_x^\uparrow := \{ B \mid (x\le B) \in U\},\)

\(U_x^- = \{ C \mid C\in U, \text{$C$ enthält $x$ nicht} \}.\)

Def: (\(x\)-Eliminations-Schritt) für \(U\) in \(x\)-Normalform:

\(U \to_x \{ A \le B \mid A\in U_x^\downarrow, B\in U_x^\uparrow \} \cup U_x^-\)

Satz: (\(U\) erfüllbar und \(U\to_x V\)) \(\iff\) (\(V\) erfüllbar).

FM-Verfahren: Variablen nacheinander eliminieren.

Fourier-Motzkin: Datenmodell lineare Fkt.

Fourier-Motzkin: Implementierung

Aufgaben

WS 24: 1, 2, 5

  1. Finden Sie eine monotone Interpretation durch eine Gewichtsfunktion für das Wortersetzungssystem

    (RULES
a a a -> b b,
b b b -> c d ,
c -> a a ,
d -> c )

    (Quelle: SRS/Zantema/z116.srs aus https://www.lri.fr/~marche/tpdb/tpdb-2.0/, vgl. https://termination-portal.org/wiki/TPDB)

    Stellen Sie das passende Ungleichungssystem auf, geben Sie eine (geratene) Lösung an.

  2. Führen Sie das Fourier-Motzkin-Verfahren für dieses Ungleichungssystem durch.

  3. Bestimmen Sie eine Lösung mit GLPK

  4. Bestimmen Sie eine Lösung mit hmatrix-glpk.

    Alberto Ruiz, Dominic Steinitz, 2010-2018, Simple interface to linear programming functions provided by GLPK. https://hackage.haskell.org/package/hmatrix-glpk

  5. Finden Sie weitere Systeme aus SRS/Zantema/z101 …z112 mit Gewichtsfunktion.

    Vergleichen Sie mit den Lösungen, die in der letzten Termination Competition gefunden wurden. https://termination-portal.org/wiki/Termination_Competition

  6. Vorverarbeitung eines Terminationsproblems durch sparse tiling, dann Gewichtsfunktion: siehe Geser, Hofbauer, Waldmann FSCD 2019 https://drops.dagstuhl.de/opus/volltexte/2019/10528/

    beruht auf einer alten und einfachen Idee, Beispiel: 2-Kachelung für \(aa\to aba\) ergibt \(\{[aa]\to[ab][ba]\}\), Anzahl der \([aa]\) nimmt ab,

    das klappt aber nicht immer so einfach (wann nicht?), läßt sich leicht reparieren (wie?)

    in zitierter Quelle: Einschränkung der Kachelmenge

Programm \(=\) Beweis

Plan, Motivation

Konjunktion \(=\) Kreuzprodukt

Implikation \(=\) Funktionstyp

Disjunktion \(=\) disj. Vereinigung

Schrittweise Beweis-Konstrukion

Ziel: Lücken in Programmen durch diese Befehle nach unten (in Teilterme) schieben und schließlich entfernen

Sprachmodelle und Formale Methoden

Das Falsche, das Wahre

Die Negation

Die Peano-Zahlen

Eigenschaften von Zahlen (Bsp. 1)

Die Sprache/Das System Agda

Aufgaben

exakt formalisieren, Beweis schrittweise entwickeln

Code aus VL verwenden (d.h., keine Standardbibliothek)

(möglichst viel C-c .., möglichst wenig selbst schreiben)

  1. Assoziativität des Oder

  2. \(\neg\neg\neg a \to \neg a\)

  3. Varianten von de Morgan

  4. für Nat: definiere odd (ungerade) (direkt, nicht als Negation von gerade), zeige: {x : Nat} -> even x -> odd x -> Falsch

  5. zeige: ungerade plus ungerade ergibt gerade

  6. definiere Multiplikation,

    zeige: ungerade mal ungerade ergibt ungerade

Note: Assoziativität der Addition (usw.) noch nicht, weil wir die Gleichheit noch nicht definiert haben.