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

WS24: 1,2, 4 (anstatt 3), 5

  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: offene 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. Modellierung von Puzzles (aus Tatham-Collection)

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

      • Zustand \(=\) Boolesche Matrix,

      • Schritt \(=\) Relation zwischen Matrizen,

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

    • diskutieren Sie Modell für Lunar Lockout, wobei Zustand \(=\) Abbildung von Roboter-Name auf Position (\(\in \mathbb{Z}\times\mathbb{Z}\))

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

    • 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 24: 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 24: Nachdenken: 1, 2, 4, 8, 9; Programmieren: 7, 10

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

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?

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?

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

WS24: empfohlen: 1, 5, 3

  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

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

  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

Aussagenlogische Resolution

Definition: ein Resolutions-Schritt

Variablen-Elimination durch vollst. Resolution

Resolution als Inferenzsystem

mehrere (teilw. sequentielle) Schritte:

Satz (Korrektheit der Resolution): \(M\vdash C \Rightarrow M\models C\)

Beweis: Induktion über Länge der Ableitung

Beachte Unterschiede:

CDCL: Spezifikation, Motivation

conflict driven clause learning (Marques-Silva, Sakallah, 1996): aus Konflikt wird Klausel gelernt, bewirkt Propagationen in anderen Teilen des DPLL-Suchbaums

CDCL: Implementierung, Übung

(Kroening/Strichman Abschn. 2.2.4)

cl := aktuelle Konfliktklausel;
while (cl enthält >= 2 Literale >= aktuell)
  lit := zuletzt zugewiesenes Literal aus cl;
  var := die Variable aus lit;
  ante := die Klausel, die in der Propagation
      benutzt wurde, welche  lit  belegt hat;
  cl := Resolve (ante, cl, var);

Beispiel: \(-1 \vee 2, -1\vee 3\vee 5, -2\vee 4, -3 \vee -4, 1\vee 5\vee -2, 2\vee 3,2\vee -3, 6\vee -5,\dots\). (weitere Klauseln mit anderen Var.)

Entscheidungen: \(\dots,-6,\dots,1\). Welche Klausel wird gelernt? Zu welchem Punkt wird zurückgekehrt?

(vlg. auch Beispiel in Folien v. Nieuvenhuis.)

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:

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.