Einleitung

Formale Methoden und Werkzeuge …

Die Rolle der Abstraktion

Industrielle Anwendungen von FMW

Industrielle Anwendungen von FMW

Anwendung: Polynom-Interpretationen

Constraint-Programmierung—Beispiel

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

Constraints in der Unterhaltungsmathematik

Wettbewerbe für Constraint-Solver

Gliederung der Vorlesung

Organisatorisches

Literatur

Hausaufgaben

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

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

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

    Beispiele:

    1. Minimum File Transfer Scheduling (node195).

    2. Minimum Dynamic Storage Allocation (node163).

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

  2. Aufgabe: formalisieren Sie Math Magic Februar 2007.

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

    (allgemein für Math Magic: offene Fragen

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

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

    • B={0,1…,n−1}B=\{0,1\dots,n-1\}, Unbekannte: hx,y∈Bh_{x,y}\in B für x,y∈Bx,y\in B

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

      ⋁p∈Permutationen(0,…,n−1),pkompatibel mit Vorgaben⋀y∈{0,…,n−1}(hx,y=p(y))\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=4n=4, Vorgabe links 2, rechts 1, kompatibel sind [0,2,1,3],[2,0,1,3],[2,1,0,3],[2,1,0,3][0,2,1,3],[2,0,1,3],[2,1,0,3],[2,1,0,3].

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

      Folge-Aufgabe: geht das auch polynomiell?

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

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

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

  4. Modellierung von Puzzles (aus Tatham-Collection)

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

      • Zustand == Boolesche Matrix,

      • Schritt == Relation zwischen Matrizen,

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

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

    3. modellieren Sie Untangle

    Vergleichen Sie mit den tatsächlichen Quelltexten

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

  5. Constraint für monotone kompatible Bewertungsfunktion:

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

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

    • Abstieg der so gefundenen Bewertungsfunktion nachrechnen für abab→baab→baba→bbaaabab\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→bbaab\to bba aufstellen und lösen.

Erfüllbarkeit aussagenlogischer Formeln (SAT)

Aussagenlogik: Syntax

aussagenlogische Formel:

damit auch Quantifikation über endlichen Bereich EE

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

Aussagenlogik: Semantik

Formulierung von SAT-Problemen mit Ersatz

Benutzung von SAT-Solvern

SAT-Modellierung für das NN-Damen-Problem

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

wir schreiben Programm,

NN-Damen mit Ersatz

Zusammenfassung Ersatz (bisher)

Modellierung durch SAT: Ramsey

gesucht ist Kanten-2-Färbung des K5K_5 ohne einfarbigen K3K_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 K43K_{43} ohne einfarbigen K5K_{5}?

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

SAT-Modell für Peg-Solitaire

Hausaufgaben

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

  1. unterschiedliche Halbringe auf zwei Elementen?

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

    Variablen: vx,yv_{x,y} für 1≤x≤b,1≤y≤h1\le x\le b, 1\le y \le h

    Constraints:

    • für jedes xx gilt: wenigstens einer von vx,1,vx,2,…,vx,hv_{x,1},v_{x,2},\dots,v_{x,h} ist wahr

    • und für jedes yy gilt: höchstens einer von v1,y,v2,y,…,vb,yv_{1,y},v_{2,y},\dots,v_{b,y} ist wahr

    1. unter welcher Bedingung an b,hb,h ist S(b,h)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)S(b,h) durch ein Programm (Sprache/Bibliothek beliebig)

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

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

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

    • vv vom Typ Relation Int Int (vgl. NN Damen)

    • „für jedes xx“: verwenden Sie rows

    • „für jedes yy“: schreiben und verwenden Sie entsprechende Fkt. columns

    • „höchstens einer“: verwenden Sie „keine zwei“.

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

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

    1. Beweisen Sie:

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

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

      3. R(a+1,b+1)≤R(a,b+1)+R(a+1,b)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)<…R(a+1,b+1)< \dots

    2. Bestimmen Sie damit obere Schranken für R(3,3),R(3,4),R(4,4)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)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 KaK_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):=R(a,b,c):= das kleinste nn mit: jeder Kanten-3-Färbung des KnK_n enthält einen roten KaK_a oder einen grünen KbK_b oder einen blauen KcK_c.

      Ergänzen und beweisen: R(a,b,c)≤R(a,R(b,c))R(a,b,c)\le R(a,R(b,c)), anwenden für R(3,3,3)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,BA,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∈{A,B}P\in \{A,B\}:

Aussagenlog. Formel für I→≤kFI \to^{\le k} F angeben,

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

One-Hot-Kodierung

Übung BMC

Anzahl-Constraints

Definition, Motivation

SAT-Kodierung eines Rösselsprungs

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

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

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

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

SAT-Kodierungen von AMO (II) - log

SAT-Kodierungen von AMO (III) - sqrt

Listen (Generatoren) zur Programmablaufsteuerung

Matrizen als Listen von Listen

Quantifikation über Listen

Iterierte assoziative Verknüpfung

Aufgaben

WS26: 2, 10, 12

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

    für welche Teilmengen gelten EXO-Constraints?

    Hinweis: für 92+3⋅929^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 ∀x0,…∃h0,…:…\forall x_0,\ldots \exists h_0,\ldots:\ldots an.

    d.h., die eine erfüllende Belegung der hih_i bestimmt, falls 𝖠𝖬𝖮(x0,…)\textsf{AMO}(x_0,\dots) wahr ist.

  5. für 𝖠𝖬𝖮\textsf{AMO} über 2k2^k Argumente: verwenden Sie sqrt-Kodierung für Rechteck mit Abmessungen 2×2k−12 \times 2^{k-1}, dann rekursiv über 2k−12^{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)S(n+1,n).

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

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

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

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

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

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

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

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

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

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

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

        (Nein—unsat nach 6 Stunden)

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

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

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

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

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

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

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

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

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

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

  12. SAT-Kodierungen für das NN-Damen-Problem:

    • naiv N4N^4

      für alle aa aus Spielfeld: für alle bb aus Spielfeld: sich aa und bb sehen, dann ¬a∨¬b\neg a \vee \neg b

    • besser N3N^3

      für alle aa aus Spielfeld: für alle bb, die von aa gesehen werden: …

    • noch besser N2N^2

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

Symmetrien

Symmetriebrechungen (Def)

Symmetriebrechungen (Bsp)

Symmetrievermutung

Übung

  1. Symmetriebrechung für verallg. Rösselsprung:

    1. Rotation der Zeit π↦π′\pi\mapsto \pi' mit π′(t)=π(t+Δ)\pi'(t)=\pi(t+\Delta)

      gebrochen durch π(0)=(0,0)\pi(0)=(0,0) (Zeit 0: Pos. oben links)

    2. Spiegelung der Zeit: π′(t)=π(−t)\pi'(t)=\pi(-t)

      kann gebrochen werden durch π(1)<π(−1)\pi(1)<\pi(-1)

      (beweisen, implementieren)

  2. Symmetrievermutung für verallg. Rösselsprung:

    Bsp: Drehung um 180180 Grad und Zeitverschiebung um halbe Periode (bei Quadrat: 90/viertel)

  3. Welche Symmetrien? Bsp. N=2,Q=3N=2, Q=3.

    https://erich-friedman.github.io/mathmagic/0207.html

    Lösen Sie die offenen Fälle (Bachelorarbeit, SAT-Kodierung von Anzahl-Constraints)

SAT: Normalformen, Transformationen

Normalformen (DNF, CNF)

Definitionen:

Disjunktion als Implikation: diese Formeln sind äquivalent:

Äquivalenzen

Erfüllbarkeits-Äquivalenz

Tseitin-Transformation

Tseitin-Transf. für Schaltkreise

Visualisierung von Schaltkreisen

Tseitin-Transformation in Ersatz (Bsp)

Abmessungen von Schaltkreisen

Abmessungen von Schaltkreisen: wozu?

Aufgaben zu Tseitin-Transformation

  1. für diese Formeln:

    • (x1↔x2)↔(x3↔x4)(x_1 \leftrightarrow x_2) \leftrightarrow (x_3 \leftrightarrow x_4)

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

      (r↔(¬(x↔y)))∧(c↔(x∧y))(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 bb (Bsp: {(x1,1),(x3,0)}\{(x_1,1),(x_3,0)\}): Klausel cc ist

Eigenschaften: für CNF FF und partielle Belegung bb:

DPLL-Algorithmus

Eingabe: CNF FF,
Ausgabe: Belegung bb mit b⊨Fb\models F oder UNSAT.

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

DPLL: Eigenschaften

wird bewiesen durch Invariante

Satz (Ü): für alle endlichen VV: <lex<_\text{lex} ist eine wohlfundierte Relation auf der Menge der partiellen VV-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 b0b_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?