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

automatische Analyse des Resourcenverbrauchs von Programmen

mittels Bewertungen von Programmzuständen:

Parameter der Bewertung werden durch Constraint-System beschrieben.

CP-Anwendung: Polynom-Interpretationen

Wettbewerbe für Constraint-Solver

Gliederung der Vorlesung

Organisatorisches

Literatur

Ausblick

ich betreue gern

Masterprojekte/-Arbeiten zur Constraint-Programmierung, z.B.

Übung KW41 (Aufgaben)

Übung KW41 (Diskussion)

Constraint-System für Hochhaus-Rätsel:

Constraint für monotone kompatible Bewertungsfunktion:

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.

Normalformen (DNF, CNF)

Definitionen:

Disjunktion als Implikation: diese Formeln sind äquivalent:

Äquivalenzen

Def: Formeln \(F\) und \(G\) heißen äquivalent, wenn \(\operatorname{Mod}(F)=\operatorname{Mod}(G)\).

Satz: zu jeder Formel \(F\) existiert äquivalente Formel \(G\) in DNF.

Satz: zu jeder Formel \(F\) existiert äquivalente Formel \(G'\) in CNF.

aber …wie groß sind diese Normalformen?

Erfüllbarkeits-Äquivalenz

Def: \(F\) und \(G\) erfüllbarkeitsäquivalent, wenn \(\operatorname{Mod}(F)\neq\emptyset \iff \operatorname{Mod}(G)\neq\emptyset\).

Satz: es gibt einen Polynomialzeit-Algorithmus, der zu jeder Formel \(F\) eine erfüllbarkeitsäquivalente CNF-Formel \(G\) berechnet.

(Zeit \(\ge\) Platz, also auch \(|G| = \text{Poly}(|F|)\))

Beweis (folgt): Tseitin-Transformation

Tseitin-Transformation

Gegeben \(F\), gesucht erfüllbarkeitsäquivalentes \(G\) in CNF.

Berechne \(G\) mit \(\operatorname{Var}(F)\subseteq\operatorname{Var}(G)\) und \(\forall b: b\models F \iff \exists b' : b \subseteq b' \wedge b'\models G\).

Plan:

Realisierung:

Tseitin-Transformation (Übung)

Übungen (Hausaufgabe, ggf. autotool):

für diese Formeln:

jeweils:

Aufgaben zur SAT-Modellierung

Vorgehen bei Modellierung:

Formulierung von SAT-Problemen mit Ersatz

http://hackage.haskell.org/package/ersatz, Edward Kmett,

import Prelude hiding ((&&),(||),not )
import Ersatz
solveWith minisat $ do 
  p <- exists ; q <- exists 
  assert $ p && not q
  return [p,q::Bit]

Unbekannte erzeugen (exists), Formel konstruieren (&&,…), assertieren, lösen

zu Implementierung vgl. auch http://www.imn.htwk-leipzig.de/~waldmann/etc/untutorial/ersatz/

ABC End View

mögliche Kodierung:

\(v(x,y,z)\iff\) an Position \((x,y)\) steht Zeichen \(z\),

wobei \(0=\)leer, \(1=a, 2=b, 3=c\)

v <- replicateM 4 $ replicateM 4 
   $ replicateM 4 exists
forM (entries v) $ \ e -> assert $ exactly_one e
forM (rows v) $ \ r ->    assert $ all_different r
forM (cols v) $ \ c ->    assert $ all_different c
assert $ see c $ left 1 v ; assert $ see b $ top 0 v

SAT-Kodierung: Hamiltonkreis

Übungsaufgaben

zum Basteln:

schriftlich, empfohlen:

SAT-Kodierungen

Beispiele:

damit ist das Thema theoretisch komplett gelöst,

aber praktisch kommt es doch auf kunstvolle Kodierungen an, weitere Einzelheiten dazu später (Bit-Blasting für SMT)

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

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: Heuristiken, Modifikationen

alles vorbildlich implementiert und dokumentiert in Minisat http://minisat.se/ (seit ca. 2005 sehr starker Solver)

Semantisches Folgern

Eigenschaften (Übungsaufgaben):

DPLL mit CDCL (Plan)

conflict driven clause learning –

bei jedem Konflikt eine Klausel \(C\) hinzufügen, die

Eigenschaften/Anwendung:

Der Konflikt-Graph

bei DPLL für CNF \(F\):

bei Konflikt für Variable \(k\)
mit aktueller Belegung \(b\)

bestimme Konflikt-Graph \(G\):

Eigenschaften von \(G\):

Lernen aus dem Konflikt-Graphen (Korrektheit)

Satz: für Konflikt-Graphen \(G\) mit Konflikt \(k\) für CNF \(F\) bei Belegung \(b\) gilt: für jede Klausel \(C\) gilt:

Beweis: betrachte \(\operatorname{Var}(C)\subseteq V(G)\). Von dort aus kann man Unit-Propagationen ausführen, die zu einem Widerspruch in \(k\) führen. (Die Information, die man aus den Decide-Knoten benötigt, ist bereits in \(\operatorname{Var}(C)\) enthalten.)

Lernen aus dem Konflikt-Graphen (Termination)

Satz: unter Vorauss. wie eben:

Beweis: …denn sie wird durch Unit-Propagation mit \(C\) verhindert.

Lernen (Implementierung)

Wie wählt man \(C\)? (widersprechende) Ziele sind:

mögliche Implementierung

c := Klausel, die zu Konflikt führte,
while (...) { 
  l := das in c zuletzt belegte Literal
  d := Klausel, durch die var(l) belegt wurde
  c := resolve (c,d,var(l)); }

Korrektheit folgt aus Eigenschaften der Resolution.

verschiedene Heuristiken zum Aufhören.

UnSAT-Solver

Beweise für Nichterfüllbarkeit

Solver rechnet lange, evtl. Hardwarefehler usw.

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

Vorverarbeitung

Niklas Eén, Armin Biere: Effective Preprocessing in SAT Through Variable and Clause Elimination. SAT 2005: 61-75 http://dx.doi.org/10.1007/11499107_5 http://minisat.se/downloads/SatELite.pdf

Implementierung muß Subsumption von Klauseln sehr schnell feststellen (wenn \(C_1\subseteq C_2\), kann \(C_2\) entfernt werden)

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

DRAT (Deletion Resolution Asymmetric Tautology)

http://www.cs.utexas.edu/~marijn/drat-trim/

dazu ggf. Übungsaufgaben

Variablen-Elimination nach Fourier-Motzkin

Übung Variablen-Elimination

SAT-Kodierung von Anzahl-Constraints

Binäre Kodierung

Propagierbarkeit

Übung Anzahl-Constraints

Modellierung:

Lösungsverfahren:

Binäre Entscheidungsgraphen (Grundlagen)

Motivation: aussagenlog. Formeln

Literatur: D. E. Knuth: TAOCP (4A1) 7.1.4;
Kroening, Strichman: Decision Procedures, 2.4. naive Ansätze (Ü: bestimme o.g. Eigenschaften):

Darstellung von Modellmengen

Ordnung auf Variablen festlegen: \(x_n > \ldots > x_2 > x_1\)

und dann binärer Entscheidungsbaum:

Für jede Formel \(F\) exist. genau ein solcher Baum \(B\) mit \([B] = \operatorname{Mod}(F)\).

Jeder Pfad von Wurzel zu 1 repräsentiert ein \(b\in \{x_1,\ldots,x_k\}\to\mathbb{B}\) (ein Modell).

Entscheidungsgraphen mit Sharing

DAG (gerichteter kreisfreier Graph) \(G=(V,E)\) heißt geordnetes binäres Entscheidungsdiagramm, falls:

heißt geordnet, falls Variablen auf jedem Pfad absteigen

heißt reduziert (ROBDD), falls außerdem

Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation.

IEEE Trans.Comp., C-35(8):677-691, 1986 http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf

ROBDD - Beispiel

import qualified OBDD as O
import qualified OBDD.Data as O

let d = O.or [ O.unit 3 True, O.unit 5 False ]

import System.Process
readProcess "dot" [ "-Tx11" ] $ O.toDot $ d

ROBDD - Anwendung

Eigenschaften von ROBDDs

Operationen mit ROBDDs (Plan)

binäre boolesche Operation \(f(n_1,n_2)\):

mit \(s(n_i)=(l_i,x_i,r_i)\)

Operationen mit ROBDDs (Implementierung)

ROBDD-Anwendungen: Modelle zählen

typische Anwendungen von ROBDD …

diese Zahlen bottom-up dranschreiben: Linearzeit

dabei beachten, daß bei der Konstruktion evtl. Variablen verschwunden sind

Beispiel (Übung) Anzahl der Lösungen des \(n\)-Damen-Problems

ROBBD-Implementierungen

Übung BDD

Binäre Entscheidungsgraphen (Ergänzungen)

ROBDDs und Automaten

Modelle zählen und würfeln

Binäre lineare Optimierung (Ü)

Gib einen Algorithmus an, der das folgende Problem
mit Hilfe eines BDD für \(F\) effizient löst:

Implementierung: http://hackage.haskell.org/package/obdd-0.5.0/docs/OBDD-Linopt.html

Anwendungen: z.B. …möglichst viele, so daß…

Die Größe von BDDs

Beispiele, Einfluß der Variablenordnung

Bestimme das ROBDD für \((a_1\wedge b_1)\vee (a_2\wedge b_2)\vee (a_3\wedge b_3)\)

Funktionen mit exponentieller ROBDD-Größe
für jede Variablenordnung: Bryant 1991

(

http://www.cs.cmu.edu/~bryant/pubdir/ieeetc91.pdf

)

Das Umordnen von Variablen in BDDs

Anwendung BDD: Optimales Sortieren

BDDs zum Abzählen von Permutationen

Übung BDD

Forschungsaufgaben BDD

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

(Alonzo Church 1938, Alan Turing 1937)

Das folgende Problem ist nicht entscheidbar:

Beweis: man kodiert das Halteproblem für ein universelles Berechnungsmodell als eine logische Formel.

Für Turingmaschinen braucht man dafür nur eine zweistellige Funktion

\(f(i,t)=\) der Inhalt von Zelle \(i\) zur Zeit \(t\).

Beachte: durch diese mathematische Fragestellung (von David Hilbert, 1928) wurde die Wissenschaft der Informatik begründet.

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 (und Ausdrücke) ist \(\mathbb{Q}\) oder \(\mathbb{Z}\)

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

Lösung nach Gauß-Verfahren:

vgl. mit Elimination einer Variablen im Unifikations-Algorithmus

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.

(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

gesucht ist Funktion \(T : \text{CNF} \to \text{IP}\) mit

Lösungsidee:

Komplexität von MIP

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 lin. Gl./Ungl.

(Integer/Real) Difference Logic

Motivation, Definition

viele Scheduling-Probleme enthalten:

das führt zu Constraintsystem:

STM-LIB-Logik QF_IDL, QF_RDL:

boolesche Kombination von \(\text{Unbekannte} \ge \text{Unbekannte} + \text{Konstante}\)

Lösung von Differenz-Constraints

Constraint-Graphen für IDL

Für gegebenes IDL-System \(S\) konstruiere gerichteten kantenbewerteten Graphen \(G\)

beachte: Gewichte \(d\) können negativ sein. (wenn nicht: Problem ist trivial lösbar)

Satz: \(S\) lösbar \(\iff\) \(G\) besitzt keinen gerichteten Kreis mit negativem Gewicht.

Implementierung: Information über Existenz eines solchen Kreises fällt bei einem anderen Algorithmus mit ab.

Kürzeste Wege in Graphen

(single-source shortest paths)

äquivalent: Eingabe ist Matrix \(w : V\times V \to \mathbb{R}\cup\{+\infty\}\)

bei (von \(s\) erreichbaren) negativen Kreisen gibt es \(x\) mit \(D(x)=-\infty\)

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

jederzeit gilt die Invariante:

verbleibende Fragen:

Laufzeit

exponentiell viele Relaxations-Schritte:

besser:

SMT, DPLL(T)

SMT \(=\) Satisfiability modulo Theory

Literatur: Kroening/Strichman, Kap. 11

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

DPLL(T), Prinzip

Ansatz: für jedes Atom \(A = P(t_1,\ldots,t_k)\)
eine neue boolesche Unbekannte \(p_A \leftrightarrow A\).

naives Vorgehen:

Realisierung mit DPLL(T):

DPLL(T), Beispiel QF_LRA

DPLL(T): Einzelheiten, Beispiele

Literatur: Robert Nievenhuis et al.: http://www.lsi.upc.edu/~roberto/RTA07-slides.pdf

Univ. Barcelona, Spin-Off: Barcelogic,

Anwendung: http://barcelogic.com/en/sports

…software for professional sports scheduling. It has been successfully applied during the last five years in the Dutch professional football (the main KNVB Ere- and Eerste Divisies).

An adequate schedule is not only important for sportive and economical fairness among teams and for public order. It also plays a very important role reducing costs and increasing revenues, e.g., the value of TV rights.

Übung DPLL(T)

Übung SMT-LIB

Aufgaben passend zur Jahreszeit

https://www.mathekalender.de/index.php?page=calendar

Löse die Aufgabe mit der jeweils passenden Methode der Constraint-Programmierung:

Übung SMT-LIB und -Solver

Polynomgleichungen

Hilberts 10. Problem

Entscheidung der Lösbarkeit einer diophantischen Gleichung.

Eine diophantische Gleichung mit irgendwelchen Unbekannten und mit ganzen rationalen Zahlkoefficienten sei vorgelegt: man soll ein Verfahren angeben, nach welchem sich mittels einer endlichen Anzahl von Operationen entscheiden lässt, ob die Gleichung in ganzen rationalen Zahlen lösbar ist.

(Vortrag vor dem Intl. Mathematikerkongreß 1900, Paris)

http://www.mathematik.uni-bielefeld.de/~kersten/hilbert/rede.html

Probleme als Motor und Indikator des Fortschritts in der Wissenschaft

Hilbert 1900. — (vgl. auch Millenium Problems http://www.claymath.org/millennium/)

Beispiele f. Polynomgleichungen

Einzelbeispiele:

Verknüpfungen:

Teilbereiche:

Geschichte

Lösbarkeit in reellen Zahlen: ist entscheidbar

Lösbarbeit in ganzen Zahlen: ist nicht entscheidbar

Polynomgleichungen über \(\mathbb{R}\)

…trotzdem kann man reelle Nullstellen zählen!

Quantoren-Elimination über \(\mathbb{R}\)

implementiert in modernen Computeralgebra-Systemen, vgl.http://www.singular.uni-kl.de/Manual/3-1-3/sing_1815.htm

Polynomgleichungen über \(\mathbb{Z}\)

Def: eine Menge \(M\subseteq \mathbb{Z}^k\) heißt diophantisch,

wenn ein Polynom \(P\) mit Koeffizienten in \(\mathbb{Z}\) existiert,

so daß \(M =\)

\(\{ (x_1,\ldots,x_i) \mid \exists x_{i+1}\in \mathbb{Z},\ldots,x_k\in \mathbb{Z}: P( x_1,\ldots,x_k) = 0 \}\)

Beispiele:

Abschluß-Eigenschaften? (Durchschnitt, Vereinigung, …)

Diophantische Mengen

Satz (Davis, Matiyasevich, Putnam, Robinson; \(\approx\) 1970)

\(M\) diophantisch \(\iff\) \(M\) ist rekursiv aufzählbar

http://logic.pdmi.ras.ru/~yumat/H10Pbook/

positive Werte dieses Polynoms \(=\) Menge der Primzahlen

\((k+2) (1 – (wz+h+j–q)^2 – ((gk+2g+k+1)(h+j)+h–z)^2 – (2n+p+q+z–e)^2 – (16(k+1)^3(k+2)(n+1)^2+1–f^2)^2 – (e^3(e+2)(a+1)^2+1–o^2)^2 – ((a^2–1)y^2+1–x^2)^2 – (16r^2y^4(a^2–1)+1–u^2)^2 – (((a+u^2(u^2–a))^2 –1)(n+4dy)^2 + 1 – (x+cu)^2)^2 – (n+l+v–y)^2 – ((a^2–1)l^2+1–m^2)^2 – (ai+k+1–l–i)^2 – (p+l(a–n–1)+b(2an+2a–n^2–2n–2)–m)^2 – (q+y(a–p–1)+s(2ap+2a–p^2–2p–2)–x)^2 – (z+pl(a–p)+t(2ap–p^2–1)–pm)^2)\)

(challenge: …find some) http://primes.utm.edu/glossary/xpage/MatijasevicPoly.html

Presburger-Arithmetik

Definition, Resultate

(nach Mojżesz Presburger, 1904–1943)

Resultate:

Beispiele f. Presburger-Formeln

Beispiele:

definierbare Funktionen und Relationen:

kann man noch größere Zahlen durch kleine Formeln definieren?

Entscheidungsverfahren (Ansatz)

Def.: Menge \(M\subset \mathbb{N}^k\) heißt P-definierbar

\(\iff\) es gibt eine P-Formel \(F\) so daß \(M = \operatorname{Mod}(F)\)

wobei \(\operatorname{Mod}(F) := \{ m \in \mathbb{N}^k \mid \{ x_1\mapsto m_1,\ldots, x_k\mapsto m_k\}\models F \}\)

für \(F\) mit freien Var. \(x_1,\ldots,x_k\),

Satz: jede solche Modellmenge \(\operatorname{Mod}(F)\) ist effektiv regulär:

Folgerung: Allgemeingültigkeit ist entscheidbar:

\(\operatorname{Lang}(A)=\emptyset\) gdw. \(\operatorname{Mod}(F)=\emptyset\) gdw. \(F\) ist widersprüchlich gdw. \(\neg F\) ist allgemeingültig.

Entscheidungsverfahren (Kodierung)

Kodierung ist nötig,

denn \(\operatorname{Mod}(F)\subseteq \mathbb{N}^k\), aber \(\operatorname{Lang}(A)\subseteq \Sigma^*\).

wählen \(\Sigma=\{0,1\}^k\), benutze Ideen:

Beispiele: Automat oder reg. Ausdruck für

Formeln und Modellmengen

Idee: logische Verknüpfungen \(\Rightarrow\) passende Operationen auf (kodierten) Modellmengen

zu zeigen ist, daß sich diese Operationen effektiv realisieren lassen (wobei Ein- und Ausgabe durch endl. Automaten dargestellt werden)

Ü: warum werden andere Verknüpfungen nicht benötigt?

Automaten (Definition)

Def: \(A=(\Sigma,Q, I,\delta,F)\) mit

daraus abgeleitet:

Automaten (Operationen: Durchschnitt)

Eingabe: \(A_1=(\Sigma,Q_1,I_1,\delta_1,F_1), A_2=(\Sigma,Q_2,I_2,\delta_2,F_2)\),

Ausgabe: \(A\) mit \(\operatorname{Lang}(A)=\operatorname{Lang}(A_1)\cap\operatorname{Lang}(A_2)\)

Lösung durch Kreuzprodukt-Konstruktion: \(A=(\Sigma,Q,I,\delta,F)\) mit

Korrektheit: \(\forall w\in\Sigma^*: w\in\operatorname{Lang}(A)\iff w\in\operatorname{Lang}(A_1) \wedge w\in\operatorname{Lang}(A_2)\)

Komplexität: \(|Q| = |Q_1|\cdot |Q_2|\) (hier: Zeit \(=\) Platz)

Automaten (Operationen: Komplement)

Eingabe: \(A_1=(\Sigma,Q_1,I_1,\delta_1,F_1)\),

Ausgabe: \(A\) mit \(\operatorname{Lang}(A)=\Sigma^* \setminus \operatorname{Lang}(A_1)\)

Lösung durch Potenzmengen-Konstruktion: \(A=(\Sigma,Q,I,\delta,F)\) mit

Korrektheit: \(\forall w\in\Sigma^*: w\in\operatorname{Lang}(A)\iff w\notin\operatorname{Lang}(A_1)\)

Komplexität: \(|Q| = 2^{|Q_1|}\) (hier: Zeit \(=\) Platz)

Automaten (Operationen: Projektion)

Eingabe: Automat \(A_1=(\Sigma^k,Q_1,I_1,\delta_1,F_1)\), Zahl \(i\)

Ausgabe: \(A\) mit \(\operatorname{Lang}(A)= \operatorname{Lang}(\text{proj}_i(A_1))\)

Lösung: \(A=(\Sigma^{k-1},Q,I,\delta,F)\) mit

Korrektheit: \(\forall w\in\Sigma^*: w\in\operatorname{Lang}(A)\iff w\operatorname{Lang}(\text{proj}_i(A_1))\)

Komplexität: \(|Q| = |Q_1|\) (hier: Zeit \(=\) Platz)

Zusammenfassung Entscheidbarkeit

durch Automaten-Operationen sind realisierbar:

Folgerungen

die Komplexität des hier angegeben Entscheidungsverfahrens ist hoch, geht das besser?

Eine untere Schranke

Fischer und Rabin 1974: http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps

Für jedes Entscheidungsverfahren \(E\)
für Presburger-Arithmetik existiert eine Formel \(F\),

so daß \(E(F)\) wenigstens \(2^{2^{|F|}}\) Rechenschritte benötigt.

Beweis-Plan: Diagonalisierung (vgl. Halteproblem):

wende solch ein Entscheidungsverfahren auf sich selbst an.

Dazu ist Kodierung nötig (Turing-Programm \(\leftrightarrow\) Zahl)

Untere Schranke

Für Maschine \(M\) und Eingabe \(x\) sowie Funktion \(f:\mathbb{N}\to\mathbb{N}\) (z. B. \(n\mapsto 2^{2^n}\)) konstruiere Formel \(D(M,x)\) mit

Für jedes Entscheidungsverfahren \(E\) für Presburger-Arithmetik:

bleibt zu zeigen, daß man solche \(D\) konstruieren kann.

Presburger-Arithmetik und große Zahlen

(folgende Konstruktion ist ähnlich zu der, die im tatsächlichen Beweis verwendet wird)

es gibt eine Folge von P-Formeln \(F_0, F_1,\ldots\) mit

Realisierung

Semilineare Mengen

Dieser Satz ist effektiv:

Gleichheits-Constraints

(Dis)Equality Constraints (Bsp, Def)

\[\begin{aligned} && (a_0=b_0 \wedge b_0=a_1 \vee a_0=c_0 \wedge c_0=a_1) \wedge \ldots\\ & \wedge& (a_n=b_n \wedge b_n=a_{n+1} \vee a_n=c_n \wedge c_n=a_{n+1}) \\ & \wedge& a_{n+1} \neq a_0\end{aligned}\] (Quelle: Strichman, Rozanov, SMT Workshop 2007,

http://www.lsi.upc.edu/~oliveras/espai/smtSlides/ofer.ppt, http://smtexec.org/exec/smtlib-portal-benchmarks.php?download&inline&b=QF_UF/eq_diamond/Feq_diamond10.smt2

Formel \(\exists x_1,\ldots,x_n : M\) mit \(M\) in negationstechnischer Normalform über Signatur:

Lösungsplan: SAT-Kodierung

Ansatz:

EQUALITY_CONSTRAINTS ist NP-vollständig, denn:

Verbesserungen (durch Analyse des Gleichheitsgraphen):

Gleichheitsgraph (equality graph)

(logische Verknüpfungen werden ignoriert!)

Widerspruchskreis:

falls die Kanten eines solchen Kreise mit und verknüpft sind, dann ist die Formel nicht erfüllbar.

Vereinfachen von Formeln

Satz: Falls \(M\) eine Teilformel \(T\) (also \(x=y\) oder \(x\neq y\)) enthält, die auf keinem Widerspruchskreis vorkommt,

dann ist \(M' := M[T/\text{True}]\) erfüllbarkeitsäquivalent zu \(M\).

Beweis: eine Richtung ist trivial,

für die andere: konstruiere aus erfüllender Belegung von \(M'\) eine erfüllende Belegung von \(M\).

Algorithmus: solange wie möglich

Reduktion zu Aussagenlogik (I)

Reduktion zu Aussagenlogik (II)

Satz (Bryant und Velev, CAV-12, LNCS 1855, 2000):

es genügt, Transitivitäts-Constraints für sehnenlose Kreise hinzuzufügen.

Satz (Graphentheorie/Folklore):

zu jedem Graphen \(G\) kann man in Polynomialzeit einen chordalen Obergraphen \(G'\) konstruieren (durch Hinzufügen von Kanten).

Graph \(G\) heißt chordal, wenn er keinen sehnenlosen Kreis einer Länge \(\ge 4\) enthält.

Vorsicht: chordal \(\neq\) trianguliert, Beispiel.

Algorithmus: wiederholt: einen Knoten entfernen,
dessen Nachbarn zu Clique vervollständigen.

Ausflug Graphentheorie

Chordale Graphen \(G\) sind perfekt: für jeden induzierten Teilgraphen \(H \subseteq G\) ist die Cliquenzahl \(\omega(H)\) ist gleich der chromatischen Zahl \(\chi(H)\).

Weiter Klassen perfekter Graphen sind:

Strong Perfect Graph Theorem (Vermutung: Claude Berge 1960, Beweis: Maria Chudnovsky und Paul Seymor 2006):

\(G\) perfekt \(\iff\) \(G\) enthält kein \(C_{2k+1}\) oder \(\overline{C_{2k+1}}\) für \(k\ge 2\).

http://users.encs.concordia.ca/~chvatal/perfect/spgt.html

Kleine Welt

für Gleichheits-Constraints mit \(n\) Variablen \(x_1,\ldots, x_n\):

die hier gezeigte Kodierung benutzt \(n^2\) boolesche Variablen \(b_{i,j} \iff (x_i = x_j)\)

das kann man reduzieren:

Wenn ein solches Gleichheits-System erfüllbar ist, dann besitzt es auch ein Modell mit \(\le n\) Elementen.

(Beweis-Idee: schlimmstenfalls sind alle Variablenwerte verschieden)

Den Wert jeder Variablen kann man also mit \(\log n\) Bits kodieren.

Erweiterung: man kann für jede Variable einen passenden (evtl. kleineren) Bereich bestimmen.

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 \[(\forall x: g(g(x))=x \wedge g(h(x))=x) \rightarrow (\forall x: h(g(x))= x)\] gehört zu jeder Theorie (mit passender Signatur),

weil sie zur Theorie der freien Termalgebra gehört.

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

Terme

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)

Die Logik QF_UF in SMT-LIB

Bsp: die Formel \((x=y) \wedge (f(f(g(x))) \neq f(f(g(y))))\)

(set-logic QF_UF) (declare-sort U 0)
(declare-fun f (U) U) (declare-fun g (U) U)
(declare-fun x () U) (declare-fun y () U)
(assert (and (= x y) 
          (not (= (f (f (g x))) (f (f (g y)))))))
(check-sat)

ist nicht erfüllbar, d. h. das Gegenteil ist allgemeingültig:

\[\forall f,g,x,y: ((x=y)\rightarrow (f(f(g(x))) = f(f(g(y))))\]

Ackermann-Transformation

…von Formel \(F\) in QF_UF nach Formel \(F'\) in equalitiy logic (\(=\) QF_UF mit nur nullstelligen Symbolen)

Satz: \(F\) erfüllbar \(\iff\) \(F'\) erfüllbar.

Programme mit Arrays

Definition


John McCarthy and James Painter: Correctness of a Compiler for Arithmetic Expressions, AMS 1967,

http://www-formal.stanford.edu/jmc/mcpain.html, http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2

Array-Logik (Beispiel mit Quantoren)

(aus Kroening/Strichman, Kap. 7)

Gültigkeit der Invariante \(\forall x: 0\le x< i \Rightarrow a[x]=0\) für die Schleife

for (int i = 0; i<N; i++) {
  a[i] = 0;
}

folgt aus Gültigkeit der Formel

\[\begin{aligned} && (\forall x: (0\le x\wedge x < i) \Rightarrow \operatorname{select}(a,x)=0 )\\ &\wedge& (a' = \operatorname{store}(a,i,0)) \\ &\Rightarrow& \dots\end{aligned}\]

Array-Logik (Beispiel QF_AX)

(set-logic QF_AX)
(declare-sort Index 0) 
(declare-sort Element 0) 
(declare-fun a () (Array Index Element)) 
(declare-fun i () Index) 
(declare-fun x () Element) 
(declare-fun y () Element) 
(assert (not (= (store (store a i x) i y)
                (store a i y))))
(check-sat)

Array-Logik (Beispiel QF_AUFLIA)

(set-logic QF_AUFLIA)
(declare-fun a () (Array Int Int)) 
(declare-fun b () (Array Int Int)) 
(declare-fun i () Int) 
(declare-fun j () Int) 
(declare-fun k () Int) 
(assert (< i j))
(assert (< (select a i) (select a j)))
(assert (= b (store a k 0)))
(assert (> i k))
(assert (> (select b i) (select b j)))
(check-sat)

Definition von Array-Formeln

(nach Kroening/Strichman Kap. 7.3)

wir betrachten boolesche Kombinationen in negationstechnischer Normalform (NNF)

von Formeln der Gestalt \(\forall i_1, \ldots, i_k: (I \Rightarrow V),\) wobei

NNF: \(\wedge/\vee\) beliebig, \(\neg\) nur ganz unten, keine anderen Operatoren.

Vereinfachung von Array-Formeln:

Für Startformel \(F\) der Array-Logik in NNF:

Verfahren erzeugt erfüllbarkeitsäquivalente Formel \(F'\)

mit Index-Prädikaten und uninterpretierten Funktionen.

\(\Rightarrow\) Betrachtung von Theorie-Kombinationen

Übung Array-Formeln/NNF

Sind die folgenden Eigenschaften durch Array-Formeln beschreibbar?

Kombination von Theorien

Motivation

(Kroening/Strichman: Kapitel 10)

Definition

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

Finite Domain Constraints

Einleitung, Definition

das ist die historische Form der Constraint-Programmierung,

modern dargestellt in Krzysztof R. Apt: Principles of Constraint Progr., Cambridge Univ. Press 2003

CNF-SAT als FD-Constraint-Problem

übersetze CNF \((p\vee \neg q)\wedge (q\vee r)\)

in äquivalentes FD-Problem \(O(p,N(q))\wedge O(q,r)\)

Algorithmen für FD-Solver (Ansatz)

zum Lösen eines Constraint-Systems \(F\): — DPLL für SAT:

grundsätzliches Vorgehen bei FD:

Lösungen, Lösbarkeit

FD-Constraint \(F\) über Universum \(U\), Bereichs-Abbildung \(\operatorname{dom}:V(F)\to 2^U\), Belegung \(b:V(F)\to U\), Bezeichungen:

Satz:

Algorithmen für FD-Solver

DPLL für SAT:

grundsätzliches Vorgehen bei FD:

Globale und lokale Konsistenz

bei den Schritten während der Lösungssuche:

Kantenkonsistenz (Definition)

Beispiele, Zusammenhang zw. Kantenkonsistenz und globaler Konsistenz?

Kantenkonsistenz (Herstellung)

Hyperkantenkonsistenz

Hyperkantenkonsistenz und Konflikte

durch Hyperkanten-Inferenz kann man Konflikte feststellen:

Bsp. \((x_1+x_2<x_3)\) mit \(D_1=\{1,2\}, D_2=\{1,2\}, D_3=\{0,1\}\)

Arc_Consistency_Deduction 
   { atom = x1 +x2 < x3 
   , variable = x3, restrict_to = [  ] 
   }

es wird ein failed-state erreicht (\(\operatorname{dom}(x_3)=\emptyset\))

danach ist Backtrack möglich.

(das ist die einzige Möglichkeit der Konflikt-Feststellung in autotool-Aufgabe)

Hyperkantenkonsistenz: Erweiterungen

Bsp. \((x_1+x_2<x_3)\) mit \(D_1=\{0,1\}, D_2=\{0,1\}, D_3=\{1\}\)

Bsp. \((x_1\le x_2 \wedge x_1\neq x_2)\) mit \(D_1=\{0,1,2\},D_2=\{0,1,2\}\)

FD und SAT

Constr.-Programmierung mit Gecode

Constraints in Mini/Flat-Zinc

Bitblasting

Motivation: SMT über Bitvektoren

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

http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV

Constraints für ganze Zahlen fixierter Bitbreite \(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

SAT-Kodierung von FD-Constraints

Ansatz:

Realisierungen:

one-hot-Kodierung

Treppen-Kodierung (order encoding)

Binäre Addition

\([x_0,\ldots] + [y_0,\ldots] = [z_0,\ldots]\)

Hilfsvariablen: \([c_0,\ldots]\) \(=\) Überträge

Realisierung:

Aufgaben: bestimme und vergleiche

Multiplikation

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

Bewertung von CNF-Kodierungen

bei der Kodierung einer einzelnen Funktion

Zusammenhang zur Zielfunktion ist nicht klar. Besser ist

denn darauf kommt es bei DPLL an.

Kodierungen und Propagationen

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

Kernaussagen

Kernthemen

Aussagenlogik (SAT)

Prädikatenlogik: Bereiche und -spezifische Verfahren:

Prädikatenlogik: allgemeine Verfahren:

Beispiel-Klausur (anderes Jahr, mglw. andere Gewichtung der Themen) http://www.imn.htwk-leipzig.de/~waldmann/edu/ss14/cp/klaus/

Typische Anwendungen

Einordnung, Ausblick

QBF-SAT (quantifizierte Boolesche Formeln)

Symmetrien

Symmetrien - Beispiel

Geschichte der Constraint-Progr. (I)

Geschichte der Constraint-Progr. (II)

Constraint-Programmier-Sprachen

Randbemerkung: ASP/SAT Confusion

http://www.imn.htwk-leipzig.de/~waldmann/etc/untutorial/asp/

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 Master-Projekt und -Arbeit