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

Abmessungen von Schaltkreisen

Abmessungen von Schaltkreisen: wozu?

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?

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

SAT-Kodierungen von AMO (III) - sqrt

Aufgaben

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

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

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

    untersuchen Sie den Unterschied zwischen der Verwendung von foldr und foldb

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

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

    • 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

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

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

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

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

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

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

Weitere Anwendungen der Resolution

Überblick

Resolution

Variablen-Elimination durch vollst. Resolution

Resolution als Inferenzsystem

mehrere Schritte:

Beachte Unterschiede:

Resolution und Unerfüllbarkeit

Satz: \(\operatorname{Mod}(F)=\emptyset \iff F\vdash \emptyset\) (in Worten: \(F\) in CNF nicht erfüllbar \(\iff\) aus \(F\) kann man die leere Klausel ableiten.)

dabei Induktionsschritt:

Resolution, Bemerkungen

Beweise für Nichterfüllbarkeit

Solver rechnet lange, evtl. Hardwarefehler usw.

Reverse Unit Propagation

http://www.satcompetition.org/2014/certunsat.shtml

RUP proofs are a sequence of clauses that are redundant with respect to the input formula. To check that a clause C is redundant, all literals C are assigned to false followed by unit propagation. In order to verify redundancy, unit propagation should result in a conflict.

\(\curvearrowright\) Konflikt für \(F\wedge \neg C\) \(\curvearrowright\) \(F\wedge\neg C\) ist nicht erfüllbar \(\curvearrowright\) \(\neg F\vee C\) ist allgemeingültig \(\curvearrowright\) \(F\models C\) (aus \(F\) folgt \(C\)) \(\curvearrowright\) \(C\) ist redundant

siehe auch E.Goldberg, Y.Novikov. Verification of proofs of unsatisfiability for CNF formulas. Design, Automation and Test in Europe. 2003, March 3-7,pp.886-891 http://eigold.tripod.com/papers/proof_verif.pdf

Deletion Resolution Asymmetric Tautology

Übungen

WS23: empfohlen: 1, 2, 3, 5, 8

  1. für unserer Microsat-Solver: Unit propagation und vollständige Elimination programmieren, testen, mit Vorverarbeitung von minisat usw. vergleichen.

  2. Beispiele aus DRAT-Papier nachrechnen.

    Wieso gilt the property AT is also known as RUP?

    Den zitierten Satz \(C\notin F\wedge \textsf{RAT}_F(C) \Rightarrow F \equiv_{\text{SAT}} (F \cup \{C\})\) beweisen.

  3. von Cadical einen UNSAT-Beweis ausgeben lassen (für eine kleine CNF),

    von Hand überprüfen, maschinell überprüfen ( https://github.com/marijnheule/drat-trim)

  4. Die Werbung auf Webseite von drat-trim enthält: RAT …permits all known techniques including extended resolution, blocked clause addition, bounded variable addition, extended learning.

    Geben Sie Quellen und (einfache) Beispiele für diese Techniken an. Besonders: bounded variable addition.

  5. für eine Teilformel \(F=F_1\wedge F_2\) 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.)

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

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

  8. Geben Sie ein Polynomialzeit-Entscheidungsverfahren für 2SAT (in der CNF hat jede Klausel \(\le\) 2 Literale) an.

    Sind die Lösungsverfahren (DPLL, DPLL \(+\) CDCL, Variablen-Elimination) für 2SAT polynomiell? (Wenn ja, Beweis; wenn nein, geben Sie eine Familie von nicht erfüllbare 2SAT-Formeln an, für welche die Verfahren lange rechnen)

  9. ich denke, die Giraffe (der \((1,4)\)-Springer) hat keinen Hamiltonpfad auf \(11\times 11\), siehe https://www.imn.htwk-leipzig.de/~waldmann/sat/leaper/. Nachrechnen und schön aufschreiben: Bachelorarbeit.

Bitblasting

Definition, Motivation, Beispiel

One-Hot-Kodierung mit Ersatz

one-hot-Kodierung

One-Hot-Arithmetik (variable Bitbreite)

Feste (statische) Bitbreite: Zahlen auf Typ-Ebene

Reflektion von Zahlen als Typ-Zahlen

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

Anwendung: Anzahl-Constraints

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.

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)

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.

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

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.

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.

    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

  7. cryptominisat: anwenden, Papier lesen, wie wird DPLL/CDCL für XOR-Klauseln angepaßt?

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

  1. Diskussion, Beispiel für TSP als MIP

    (es wird kein Kreis, sondern ein Weg bestimmt?)

  2. Formulierung eines SAT-Problems als IP, Lösung mit CBC.

  3. Überdeckungsproblem (möglichst wenige Damen, die das gesamte Schachbrett beherrschen) as IP,

    Constraint-System programmatisch erzeugen, z.B. https://hackage.haskell.org/package/limp, Lösen mit https://hackage.haskell.org/package/limp-cbc

    Vergleichen mit SAT-Kodierung, Anzahlconstraint mit Bit-Blasting

  4. Auswertung Adventskalender (Aufgaben: 1, 24)

    Planung Projekte

(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

Aufgaben Differenz-Logik

beachte: hier System \(=\) Konjunktion.
andere Boolesche Kombinationen: später (SMT).

  1. ein unlösbares IDL-System \(S\) angeben,

    (mit 4 Constraints, so daß jedes echte Unter-System \(S'\subsetneqq S\) (mit \(\le 3\) Constraints) lösbar ist)

    Bellmann-Ford für den Graphen dieses \(S\),

    Dijkstra für den Graphen dieses \(S\).

  2. Wie aufwendig ist die Lösung eines IDL-Systems durch Fourier-Motzkin?

    vergleichen mit Laufzeit Bellmann-Ford

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

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

Lösungsverfahren für UF

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

Kombination von Theorien

Beispiele f. Theorie-Kombinationen

(Kroening/Strichman: Kapitel 10)

Anwendung: statische Software-Analyse

Definition f. Theorie-Kombination

(Wdhlg) Signatur \(\Sigma\), Theorie \(T\), Gültigkeit \(T \models \phi\)

Kombination von Theorien:

Aufgabenstellung:

Konvexe Theorien

eine Theorie \(T\) heißt konvex, wenn für jede Konjunktion \(\phi\) von Atomen, Zahl \(n\), Variablen \(x_1,\ldots,x_n,y_1,\ldots,y_n\) gilt:

Ü: warum heißt das konvex?

Beispiele: konvex oder nicht?

Das Nelson-Oppen-Verfahren (Quellen)

Das Nelson-Oppen-Verfahren: purification

purification (Reinigung):

Beispiel:

im Allg. \(\phi \iff \exists a,\ldots: \phi'\)

d. h. \(\phi\) erfüllbar \(\iff\) \(\phi'\) erfüllbar.

Nelson-Oppen für konvexe Theorien

für entscheidbare Theorien \(T_1,\ldots,T_n\) (jeweils \(T_i\) über \(\Sigma_i\))

(Beispiele)

(Beweis)

Nelson-Oppen, Beispiel

(Kroening/Strichman, Ex. 10.8)

NO-Verfahren anwenden auf:

\(x_2 \ge x_1 \wedge x_1-x_3\ge x_2 \wedge x_3\ge 0 \wedge f(f(x_1)-f(x_2)) \neq f(x_3)\)

Diese Beispiel als Constraint-Problem in der geeigneten SMT-LIB-Teilsprache formulieren und mit Z3 Erfüllbarkeit bestimmen.

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

Theorie der Bitvektoren (QF_BV)

Beispiel, Anwendung, Solver

Lazy und Eager Approach für QFBV

QFBV für arithmetische Constraints

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