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

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?

    • (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?