Einleitung

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))

Industrielle Anwendungen der CP

Industrielle Anwendungen der CP

CP-Anwendung: Polynom-Interpretationen

Constraints in der Unterhaltungsmathematik

Wettbewerbe für Constraint-Solver

Gliederung der Vorlesung

Organisatorisches

Literatur

Hausaufgaben

  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

    Beispiel: Minimum File Transfer Scheduling (node195). Erläutern Sie die Spezifikation an einem Beispiel.

  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: lösen Sie eine der offenen Fragen https://erich-friedman.github.io/mathmagic/unsolved.html )

  3. Aufgabe: formalisieren Sie https://www.janko.at/Raetsel/Wolkenkratzer.

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

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

      \(\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]\).

      entspr. für Spalten

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

      Folge-Aufgabe: geht das auch polynomiell?

  4. 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:

Aussagenlogik: Semantik

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

Programmbeispiel zu Ramsey

Quelltext in Ramsey.hs

num p q = 10 * p + q ; n x = negate x
f = do
  p <- [1..5] ; q <- [p+1 .. 5] ; r <- [q+1 .. 5]
  [    [ num p q, num q r, num p r, 0 ]
     , [ n $ num p q, n $ num q r, n $ num p r, 0 ] ]
main = putStrLn $ unlines $ do
  cl <- f ; return $ unwords $ map show cl

Ausführen:

runghc Ramsey.hs | minisat /dev/stdin /dev/stdout

Benutzung von SAT-Solvern

Eingabeformat: SAT-Problem in CNF:

Beispiel

p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

Löser: minisat input.cnf output.text

Modellierung durch SAT: \(N\) Damen

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

Formulierung von SAT-Problemen mit Ersatz

\(N\)-Queens mit Ersatz

Zusammenfassung Ersatz (bisher)

Hausaufgaben

  1. unterschiedliche Halbringe auf zwei Elementen?

  2. für die Formel \(S(b,h)\) (abhängig von zwei 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 (a - Sprache/Bibliothek beliebig, b - Haskell/Ersatz)

      ( \(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 das angegebene Ersatz-Programm zu \(N\)-Queens:

    • welche Größe haben die erzeugten Formeln (unter den assert)? (in Abhängigkeit von \(N\))

    • welche Laufzeit hat das Programm?

  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,b+1)\)

        (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. Realisierung der SAT-Kodierung von \(R(a,b)\): benutzen Sie eine Funktion, die alle Teilfolgen gegebener Länge bestimmt.

    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

    Verwenden Sie subs a [1 .. n] zur Auswahl des \(K_a\) sowie subs 2 xs zur Auswahl der Kanten.

  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)

SAT: Normalformen, Transformationen

Normalformen (DNF, CNF)

Definitionen:

Disjunktion als Implikation: diese Formeln sind äquivalent:

Äquivalenzen

Erfüllbarkeits-Äquivalenz

Tseitin-Transformation

Spezifikation:

Plan:

Realisierung:

Tseitin-Transf. für Schaltkreise

Tseitin-Transformation in Ersatz (Bsp)

And-Inverter-Graphen

Plaisted-Greenbaum-Transformation

Tseitin-Transformation (Aufgaben)

  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 eine 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?

Komplexität der Erfüllbarkeit

Motivation, Begriffe

Wiederholung: NP-Vollständigkeit

Wiederholung: SAT ist NP-vollständig

\(\operatorname{\text{SAT}}\in\operatorname{\text{NP}}\) ist klar (NDTM rät die Belegung)

Sei \(M\in\operatorname{\text{NP}}\), zu zeigen \(M\le_P \operatorname{\text{SAT}}\). Gegeben ist also das Programm einer NDTM, die \(M\) in Polynomialzeit akzeptiert

Die Tseitin-Transformation

Was nützen diese Aussagen?

SAT-Solver

Überblick

Spezifikation:

Verfahren:

Evolutionäre Algorithmen für SAT

Problem: starke Abhängigkeit von Variablenreihenfolge

Lokale Suche (GSat, Walksat)

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

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: Heuristik, Ergänzungen

Semantisches Folgern

Eigenschaften (Übungsaufgaben):

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

Variablen-Elimination durch vollst. Resolution

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. 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?

  3. für eine Teilformel \(F\) wird die Tseitin-Transformation durchgeführt und für die dabei entstehende Variable \(v_F\) (mit \(v_f\leftrightarrow F\)) ein assert.

    Was passiert bei vollständiger Elimination von \(v_F\)?

    (Es ist anzunehmen, daß das alle Solver tun. Deswegen ist für ersatz wohl keine Plaisted-Greenbaum-Transformation (J. Symb. Comp. 2(3) 1986, pp 293-304) https://doi.org/10.1016/S0747-7171(86)80028-1 notwendig.)

  4. Wenn \(G\) aus \(F\) durch vollständige Resolution (Elimination) von \(v\) entsteht: Konstruieren Sie aus einem Modell \(b\) für \(G\) ein Modell für \(F\) (wie ist \(v\) zu belegen?)

  5. für eine unerfüllbare Schubfachschluß-Formel (in jeder Zeile \(1, \dots, H\) höchstens einer wahr, in jeder Spalte \(1, \dots, B\) wenigstens einer wahr, z.B. für \(B=3,H=2\) die Klauselmenge \(\{\overline 1\overline 2,\overline 1\overline 3,\overline 3\overline 3, \overline 4\overline 5,\overline 4\overline 6,\overline 5\overline 6, 12, 34, 56 \}\)

    einen möglichst kurzen Beweis der Unerfüllbarkeit

    1. mit DPLL (ohne Lernen)

    2. mit DPLL und CDCL

    3. …und vorheriger Variablen-Elimination

    4. …nur mit Variablen-Elimination (ohne DPLL)

  6. eine nicht erfüllbare 2SAT-Formel (jede Klausel genau zwei Literale) angeben, für die DPLL möglichst lange braucht. Vergleichen mit DPLL \(+\) CDCL, Variablen-Elimination.

  7. (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\)?

  8. conflict clause minimization (Sörenson, SAT 2005, http://minisat.se/downloads/MiniSat_v1.13_short.pdf): Ein Beispiel angeben. Entsprechende Ergänzung der autotool-Aufgabe vorschlagen.

  9. 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 an/abschalten

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)

SAT-Kodierungen von AMO (II) - log

Propositionale vs. Funktionale Kodierungen

Propositional vs. Funktional

Praktische Eigenschaften von Kodierungen (I)

Praktische Eigensch. (II) – Forcing

SAT-Kodierungen von AMO (III) - sqrt

Aufgaben

  1. Vergleiche Sie die commander-Kodierung für AMO von Klieber und Kwon, Int. Workshop on 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

  2. Für die commander-Kodierung und die sqrt-Kodierung: prüfen Sie, ob die im im Paper angegebene PK tatsächlich aus unserer FK (Beispiel-Quelltexte) entsteht.

    Sehen Sie sich kleine AMO-Formeln an, vermessen Sie größere mittels mini/kissat (Logging des Preprocessing)

  3. Für die sqrt-Kodierung für AMO von Chen 2010:

    Benutzen Sie die gleiche Idee für eine höherdimensionale Anordnung, z.B. AMO von 30 Variablen als \(2 \times 3 \times 5\).

    Teilen Sie AMO für \(2^n\) Variablen in \(2\times\dots\times 2\) ein und vergleichen Sie mit der log-Kodierung.

    (sqrt-AMO ist funktional, log-AMO ist es im Original nicht, aber mit dieser Herleitung doch?)

  4. für die lineare AMO-Kodierung (Addition auf \(\{0,1,\ge 2\}\)):

    untersuchen Sie den Unterschied zwischen der Verwendung von foldr und foldb

  5. für jede der betrachteten AMO-Kodierungen: wie kann mit möglichst wenig Zusatz-Aufwand EXO erhalten?

  6. Für den Rösselsprung:

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

    • AMO und ALO durch EXO ersetzen

    • umbauen, so daß ein kreuzungsfreier Weg der Länge \(=l\) (zusätzlicher Eingabe-Parameter) beschrieben wird.

    • 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/

  7. 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.

  8. (Vorfreude, schönste …) (ab 1. Dezember) https://www.mathekalender.de/wp/de/kalender/

Prädikatenlogik

Plan

(für den Rest der Vorlesung)

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)

Theorien

Def: \(\operatorname{Th}(S) := \{ F \mid S \models F \}\)

(Die Theorie einer Struktur \(S\) ist die Menge der Sätze, die in \(S\) wahr sind.)

Bsp: \(\glqq \forall x:\forall y: x\cdot y=y\cdot x\grqq \in\operatorname{Th}(\mathbb{N},1,\cdot)\)

Für \(K\) eine Menge von Strukturen:

Def: \(\operatorname{Th}(K) := \bigcap_{S\in K} \operatorname{Th}(S)\)

(die Sätze, die in jeder Struktur aus \(K\) wahr sind)

Bsp: \(\glqq \forall x:\forall y: x\cdot y=y\cdot x\grqq \notin \operatorname{Th}(\text{Gruppen})\)

…denn es gibt nicht kommutative Gruppen, z.B. \(\operatorname{SL}(2,\mathbb{Z})\)

Unentscheidbarkeit

Folgerungen aus Unentscheidbarkeit

Suche nach (effizienten) Algorithmen für Spezialfälle

(die trotzdem ausreichen, um interessante Anwendungsprobleme zu modellieren)

Lineare Gleichungen und Ungleichungen

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.

Beispiel LP: monotone Interpretation

Beispiel LP-Solver

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.

Aufgaben

  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.

  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

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

  6. cryptominisat benutzen (Beispiele), verstehen (Paper lesen, wie wird DPLL/CDCL für XOR-Klauseln angepaßt?)

(Integer/Real) Difference Logic

Motivation, Definition

Constraint-Graphen für IDL

Kürzeste Wege in Graphen

Lösungsidee

iterativer Algorithmus mit Zustand \(d : V\to \mathbb{R}\cup \{+\infty\}\).

\(d(s) := 0, \forall x\neq s: d(x) := +\infty\)
while ēs gibt ēine Kante \(i \stackrel{w_{i,j}}\to j\) mit \(d(i)+w_{i,j}< d(j)\)
\(d(j) := d(i) +w_{i,j}\) // Kante \(ij\) wird entspannt

jederzeit gilt die Invariante:

verbleibende Fragen:

Laufzeit

Ganzzahlige lineare Ungleichungen

(Mixed) Integer Programming

MIP-Beispiel

LP-Format mit Abschnitten

Minimize  obj: y
Subject To
 c1: 2 x  <= 1
 c2: - 2 x + 2 y <= 1
 c3:  2 x + 2 y >= 1
General  x y
End

Lösen mit https://projects.coin-or.org/Cbc:

cbc check.lp solve solu /dev/stdout

Ü: ausprobieren und erklären: nur \(x\), nur \(y\) ganzzahlig

MIP-Lösungsverfahren

SAT als IP, Komplexität von IP

Travelling Salesman als MIP

(dieses Bsp. aus Papadimitriou und Steiglitz:
Combinatorial Optimization, Prentice Hall 1982)

Travelling Salesman:

Ansatz zur Modellierung:

Travelling Salesman als MIP (II)

Miller, Tucker, Zemlin: Integer Programming Formulation and Travelling Salesman Problem JACM 7(1960) 326–329

Übung: beweise

Was ist die anschauliche Bedeutung der \(u_i\)?

min und max als MIP

Idee zur Simulation von \(A\le B \vee C \le D\):

Übungen zu DL, MIP (für KW 53)

SMT (Satisfiability Modulo Theories)

Definition, 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)

Aufgaben

  1. 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

    Lösen Sie nun die gleiche Aufgabe mit QF_BV (Bitvektoren)

  2. 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/

  3. wählen Sie zufällig in SMTLIB eine (quantorenfreie) Logik und dort eine Benchmark. Erklären Sie die Benchmark. Wenden Sie verschiedene SMT-Solver an (z.B. Z3 und Z3++) und vergleichen Sie Laufzeiten. Ändern Sie die Formel (vorsichtig), erläutern Sie die Änderungen der Belegung oder Erfüllbarkeit.

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

  5. Eine kompatible arktische Matrix-Interpretation bestimmen für \(a^2 b^2\to b^3 a^3\).

    Warum gibt es keine solche Interpretation für \(ab\to ba\)? Hinweis: weil diese Regel quadratische lange Ableitungen gestattet (geben Sie welche an), aber solche können bei arktischen Interpretationen nicht vorkommen (warum?)

Uninterpretierte Funktionen (UF)

Motivation, Definition

Interpretation \(\models\) Formel,

Interpretation \(=\) (Struktur, Belegung)

Die Theorie \(\operatorname{Th}(S)\) einer Struktur \(S\) ist Menge aller in \(S\) wahren Formeln: \(\operatorname{Th}(S)=\{F \mid \forall b: (S,b) \models F \}\)

Beispiel 1: Formel \(a \cdot b = b \cdot a\) gehört zur \(\operatorname{Th}(\text{$\mathbb{N}$ mit Multipl.})\), aber nicht zu \(\operatorname{Th}(\text{Matrizen über $\mathbb{N}$ mit Multipl.})\).

Beispiel 2: Formel \[(x = y) \Rightarrow f (f (x)) = f (f (y))\] gehört zu jeder Theorie (mit passender Signatur),

Gleichheit von Termen

In jeder Algebra gelten diese Formeln: \[(t_1=s_1) \wedge \ldots \wedge (t_k=s_k) \to f(t_1,\ldots,t_k) = f(s_1,\ldots,s_k)\] (Leibniz-Axiom für die Gleichheit, functional consistency)

Anwendungen

Für jede \(\Sigma\)-Algebra \(S\) gilt:

Vorteil: kein Entscheidungsverfahren für \(S\) nötig

Nachteil: Umkehrung gilt nicht.

Anwendung bei Analyse von Programmen, Schaltkreisen: Unterprogramme (Teilschaltungen) als black box,

Roope Kaivola et al.: Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation, Conf. Computer Aided Verification 2009, http://dx.doi.org/10.1007/978-3-642-02658-4_32

Die Logik QF_UF in SMT-LIB

Ackermann-Transformation

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\).

Theorie-Solver für Gleichheitslogik

DPLL(T), Beispiel QF_LRA

DPLL(T): Einzelheiten, Beispiele

Aufgaben

  1. freie Algebra:

    • weitere freie Algebren zu \(\Sigma=\{f/2\}\) über \(\mathbb{N}\).

    • die von \(\scriptsize F(x)=\begin{pmatrix}1 & 1 \\ 0 & 1\end{pmatrix}x; ~ \scriptsize G(x)=\begin{pmatrix}2 & 0 \\ 0 & 1\end{pmatrix}x; ~ I()=\begin{pmatrix}1 & 0 \\ 0 & 1\end{pmatrix}\) erzeugte Algebra ist frei?

  2. QF_UF:

    1. warum ist diese Formel nicht erfüllbar?

      https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_UF/-/blob/master/TypeSafe/z3.1184163.smt2

    2. Benchmarks

      https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_UF/-/tree/master/eq_diamond

      ausprobieren, angegebene Quelle (SMT 2005) lesen

    3. über alle Benchmarks

      https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_UF/-/tree/master/

      welches ist die schwerste (für Z3, für CVC5)?

    4. Für quantifiers in the UF theory

      https://smt-comp.github.io/2021/system-descriptions/Yices2.pdf

      : Beschreibung und Beispiele suchen, Yices installlieren, Beispiele ausprobieren

  3. inkrementeller Theorie-Solver:

    1. für QF_IDL (Niewenhuis JACM 2006

      https://www.cs.upc.edu/~roberto/papers.html

      ), Unterschiede zu nicht inkrementellem Verfahren.

    2. für QF_LRA: wie kann man Fourier-Motzkin inkrementell verwenden? (Der Anwendungsfall ist: es taucht eine neue Ungleichung auf, in der Variablen vorkommen, die durch Fourier-Motzkin bereits eliminiert wurden)

  4. DPLL(T) in autotool-Aufgabe

  5. Diskussion zu Projekten

Bitblasting

Motivation: SMT über Bitvektoren

SMT-Logik QF_BV motiviert durch (Rechner-)Schaltkreis- und (Maschinen-)Programmverifikation

Constraint-Bereich: Bit-Vektoren mit statisch bekannter Breite \(w\)

(declare-fun a () (_ BitVec 12))
(declare-fun b () (_ BitVec 12))
(assert (and (bvult (_ bv1 12) a) 
             (bvult (_ bv1 12) b)
             (= (_ bv1001 12) (bvmul a b))))

Lazy und Eager Approach für QFBV

Bit-Blasting für FD-Constraints

(Wertebereich jeder Unbekannten ist endlich, FD \(=\) Finite Domain) Ansatz:

Realisierungen:

Bit-Blasting für unendliche Bereiche?

Anwendung: Graceful Labeling

one-hot-Kodierung

One-Hot-Kodierung mit Ersatz

One-Hot-Arithmetik (variable Bitbreite)

Feste (statische) Bitbreite: Zahlen auf Typ-Ebene

Reflektion von Zahlen als Typ-Zahlen

Aufgaben

  1. Überprüfen Sie generalized arc-consistency (forcing) für sym_diff_eq a b c (Semantik: \(|a-b|=c\)) für One-Hot-Kodierung.

    Bsp.: Bitbreite 4 (für Bereich \(\{0, 1, 2, 3\}\)), partielle Belegung \(a_0=0, a_1=0, b_0=0, b_1=0\). Welche \(c_i\) sind dadurch (semantisch) bestimmt? Erhält man diese durch Unit-Propagation? (nehmen Sie dabei an, daß die verwendete Kodierung von exactly-one forcierend ist).

  2. zu D. E. Knuth: TAOCP Fasc. 7A (Version 18. Nov. 2022), S. 16 ff: Graph labeling

    Diskutieren/realisieren Sie Bitblasting (SAT-Kodierung) für das reverse model (S. 19)

Bitblasting für Arithmetik

Treppen-Kodierung (order encoding)

Addition für Treppenkodierung

Binär-Kodierung, Addition

Binäre Multiplikation

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

Arithmetik für (statisch) fixierte Bitbreite

Aufgaben

  1. sind angegeben Implementierungen der binären Arithmetik und Vergleichsrel. fixierter Breite forcierend?

  2. Binärzahlen (statt one-hot) für Graceful labeling.

  3. Kodierung von vorzeichenbehafteten Zahlen

    1. feste Bitbreite: im Zweierkomplement

    2. variable 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)

  4. Diskutieren Sie richtige Propagation von Überläufen bei Kodierung von Zahlen aus \(\{-B, \dots, B\}\) für Operationen plus, mal, kleiner, gleich.

  5. weitere Beispiele und Aufgaben zu Bitblasting-Arithmetik:

    https://www.imn.htwk-leipzig.de/~waldmann/talk/22/isr/#solving-qf_nia-by-bit-blasting

    (ISR 2022)

  6. Realisieren Sie die Berechnung des Überlaufs bei

    1. Addition

    2. Multiplikation

    in QF_BV durch möglichst kleine Formel.

    Damit können Sie ein Constraint \(P\) in QF_NIA, QF_LIA in Constraints \(P_w\) in QF_BV (mit Bitbreite \(w\)) übersetzen, und evtl. Glück haben, wie in VL beschrieben.

    Probieren Sie für einfache (handgeschriebene) Constraints \(P\) aus, ob (z.B. Z3) für \(P\) oder \(P_1, P_2, \dots\) schneller ist.

Paralleles SAT-Lösen

Paralleles SAT-Lösen (Grundlagen)

Paralleles SAT-Lösen (heute)

Anw: Schaltkreisverifikation

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

Übung BMC

Zusammenfassung, Ausblick

Kernaussagen

Kernthemen

Aussagenlogik (SAT)

Prädikatenlogik: Bereiche und -spezifische Verfahren:

Prädikatenlogik: allgemeine und spezielle Verfahren:

Typische Anwendungen

Geschichte der Constraint-Progr. (I)

Geschichte der Constraint-Progr. (II)

Constraints für (baum)strukturierte Daten

SAT-Kodierung von Bäumen

Spezifikation, Implementierung, Korrektheit, Anwendungsfälle (Terminations-Analyse, RNA-Design), Messungen, Verbesserungen, Erweiterungen.

siehe Publikationen auf http://abau.org/co4.html

Themen für Bachelor/Master-Arbeiten