Constraint-Programmierung
Vorlesung
Sommersemester 2009, 2012

<all>

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

mögl. Projektthemen:

Literatur

Erfüllbarkeit aussagenlogischer Formeln (SAT)

Aussagenlogik: Syntax aussagenlogische Formel:

Aussagenlogik: Semantik

Der Folgerungsbegriff

eine Formel \(F\) folgt aus einer Formelmenge \(M\):

Beispiele/Übung (beweise!)

Normalformen (DNF, CNF)

Definitionen:

Disjunktion als Implikation: diese Formeln sind äquivalent:

Modellierung durch SAT

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

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

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

also auch \(|G| = \text{Poly}(|F|)\)

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

nach Tseitin-Algorithmus.

Beispiele zur SAT-Modellierung

Vorgehen bei Modellierung:

SAT: Anwendungen

SAT-Kodierungen

Weil SAT NP-vollständig ist (Ü: Definition) kann man jedes Problem aus NP nach SAT übersetzen,

d.h. in Polynomialzeit eine Formel konstruieren, die genau dann erfüllbar ist, wenn das Problem eine Lösung hat — und man kann aus der erfüllenden Belegung eine Lösung rekonstruieren.

Beispiele:

SAT-Kodierung: Independent Set Def: Graph \(G=(V,E)\), Menge

\(M\subseteq V\) heißt unabhängig, falls \(\forall x,y\in M: xy\notin E\).

Entscheidungsproblem:

Optimierungsproblem:

Ist das Optimierungsproblem schwieriger (aufwendiger) als das Entscheidungsproblem? (Hier: nein.)

SAT-Kodierung: Anzahl-Constraints

\({\operatorname{count}_{\ge{k}}}(p_1,\ldots,p_n) =\) wenigstens \(k\) der \(n\) Variablen sind wahr.

(Übung: definiere \({\operatorname{count}_{={k}}}, {\operatorname{count}_{\le{k}}}\))

Anwendung: größte unabh. Menge von Springern?

SAT-Kodierung: Vertex Cover

SAT-Kodierung: Hamiltonkreis

SAT-Kodierung: Färbung von Graphen

Suche nach symmetrischen Lösungen

falls ein Problem zu groß für den Solver ist:

Def (allgemein): \(f\) ist Symmetrie von \(M\), falls \(f(M)\sim M\).

Beispiel: rotationssymmetrische Aufstellungen von Figuren auf Schachbrett (Vertex Cover, Hamiltonkreis).

Neue Schranke für Van der Waerdens Funktion

\(W(r,k) = \) die größte Zahl \(n\), für die es eine \(r\)-Färbung von \([1,2,\dots,n]\) gibt ohne einfarbige arithmetische Folge.

Satz (überhaupt nicht trivial): alle diese Zahlen sind endlich.

Einige Schranken erst vor kurzer Zeit verbessert, durch SAT-Kodierung, siehe Heule, M. J. H: Improving the Odds: New Lower Bounds for Van der Waerden Numbers. March 4, 2008. http://www.st.ewi.tudelft.nl/sat/slides/waerden.pdf

Software zur SAT-Kodierung

Überblick

Softwarepaket satchmo (SAT encoding monad) https://github.com/jwaldmann/satchmo

vergleichbar: http://rise4fun.com/Z3Py
(Übung: Unterschiede?)

Technische Grundlagen

Automatische Hilfsvariablen

im Quelltext: Haskell-Namen (x), für Solver: Nummern (1)

import Satchmo.Boolean 
import Satchmo.Solve
test :: IO ( Maybe Bool )
test = solve $ do 
    x <- boolean -- Allokation einer Variablen
    assert [ not x ]
    return $ decode x

Realisierung:

Realisierung logischer Funktionen

and :: [ Boolean ] -> SAT Boolean
and xs = do
  y <- boolean -- Hilfsvariable lt. Tseitin
  forM xs $ \ x -> do
      assert [ not y, x ]
  assert $ y : map not xs
  return y

Übung:

Dekodierung mit Typklassen

(vereinfachte Darstellung)

type Decoder a = Reader (Map Literal Bool) a
class Decode c a where 
    decode :: c -> Decoder a
instance Decode Boolean Bool where 
    decode x = ... -- benutzt Minisat-API
instance (Decode c a) => Decode [c] [a] where
    decode xs = forM xs decode

Relationen

relation :: ( Ix a, Ix b )
  => ((a,b),(a,b)) -> SAT ( Relation a b )
instance (Ix a, Ix b) => 
  Decode ( Relation a b ) ( Array (a,b) Bool ) 
product :: ..=> Relation a b -> Relation b c 
  -> SAT ( Relation a c )
implies :: ..=> Relation a b -> Relation a b
  -> SAT Boolean

Anwendungen:

transitive r = do
    r2 <- product r r ; implies r2 r

Übung: eine schwach zusammenhängende Relation;
eine s.z. Halbordnung, die keine totale Ordnung ist.

SAT-Solver in Paketmanagern

gesucht: konfliktfreier Install-Plan

Pentomino

Es gibt 12 Pentominos: zusammenhängende Figuren aus je 5 Einheitsquadraten.

(Henry Ernest Dudeny, 1907; Solomon W. Golomb, 197*)

(und viele ähnliche Fragen dieser Art.)

Lösung durch SAT-Modellierung.

Variablen? Constraints?

Schwierige Fälle für die SAT-Kodierung

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)

Zustand \(=\) partielle Belegung

DPLL: Heuristiken, Modifikationen

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

Beweise für Nichterfüllbarkeit

Solver rechnet lange, evtl. Hardwarefehler usw.

Resolution

Resolution und Unerfüllbarkeit

Satz: \(F\) in CNF nicht erfüllbar \(\iff\) es gibt eine Resolutions-Ableitung der leeren Klausel.

Beweis:

dabei Induktionsschritt:

Resolution, Bemerkungen

DPLL: Lernen von Konfliktklauseln

bei jedem Konflikt:

conflict-driven backtracking:

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

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

Binäre Entscheidungsgraphen (ROBDDs)

Motivation

gesucht ist eine Datenstruktur, die eine aussagenlogische Formel kanonisch repräsentiert und für die aussagenlog. Operationen effizient ausführbar sind.

Ansätze:

Lösung: bessere Darstellung für \({\operatorname{Mod}}(F)\)

Literatur: Kroening, Strichman: Decision Procedures, 2.4.

Darstellung von Modellmengen

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

und dann binärer Entscheidungsbaum:

Für jede Formel \(F\) existiert Baum \(B\) mit \([B] = {\operatorname{Mod}}(F)\).

Entscheidungsbäume mit Sharing

ausgehend von eben definiertem Baum: konstruiere DAG (gerichteten kreisfreien Graphen):

reduziertes geordnetes binäres Entscheidungsdiagramm (ROBDD)

Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677-691, 1986

Eigenschaften von ROBDDs

Operationen mit ROBDDs

binäre boolesche Operation \(f\):

der Trick ist: dynamische Optimierung (d. h. von unten nach oben ausrechnen und Ergebnisse merken).

ergibt Laufzeit für \(f(s,t)\) von \(O(|s|\cdot|t|)\).

\(\Rightarrow\) worst-case-Laufzeit für Konstruktion eines ROBDD zu einer Formel: exponentiell

OBDD-Anwendung: Modelle zählen

typische Anwendung von OBDD …

\[\begin{aligned} |{\operatorname{Mod}}(0)|=0, |{\operatorname{Mod}}(1)|=1, \\ |{\operatorname{Mod}}(v,l,r)|=|{\operatorname{Mod}}(l)|+|{\operatorname{Mod}}(r)|\end{aligned}\]

diese Zahlen bottom-up dranschreiben: Linearzeit

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

ROBBD-Implementierungen

import qualified Prelude ; import OBDD
import qualified Data.Set as S

let t = or [ unit "x" Prelude.True
           , unit "y" Prelude.False ]
number_of_models (S.fromList ["x", "y"]) t

http://hackage.haskell.org/package/obdd-0.2

Prädikatenlogik

Plan

(für den Rest der Vorlesung)

Syntax der Prädikatenlogik

Semantik der Prädikatenlogik

die Modell-Relation \((S,b) \models F\)

Erfüllbarkeit, Allgemeingültigkeit (Def, Bsp)

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

Termgleichungen

Einführung

Anwendungen: Verarbeitung symbolischer Ausdrücke

Unifikation—Begriffe

Unifikation—Definition

Unifikationsproblem

allgemeinst \(=\) minimal bzgl. der Prä-Ordnung

\(\sigma_1 \le \sigma_2 \iff \exists \tau : \sigma_1 \circ \tau = \sigma_2\)

Satz: jedes Unifikationsproblem ist entweder gar nicht oder bis auf Umbenennung eindeutig lösbar

Unifikation—Algorithmus

\({\operatorname{mgu}}(s, t)\) nach Fallunterscheidung

Bemerkungen:

Übung zur Prädikaten-Logik

(vgl. Uwe Schöning: Logik für Informatiker, Spektrum)

Übung zu Termgleichungen

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.

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

LP ist in P (Ellipsoid-Verfahren), aber IP ist NP-vollständig:

deswegen gibt es keinen effizienten Algorithmus (falls P \(\neq\) NP)

SAT als IP

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

Lösungsidee:

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

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 = es gibt = eine 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:

[node distance=5cm,auto,>=stealth,thick] (s) # s; (p) [right of=s] # p; (q) [right of=p] q; (t) [right of=q] # t; (s) edge [bend right] node [below] 4 (p); (p) edge [bend right] node [below] # 2 (q); (q) edge [bend right] node [below] # 1 (t); (s) edge [bend left] node # 0 (p); (p) edge [bend left] node 0 (q); (q) edge [bend left] node # 0 (t);

besser:

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,,x_i) x_{i+1},,x_k: P( x_1,,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–f2)2 – (e3(e+2)(a+1)2+1–o2)2 – ((a2–1)y2+1–x2)2 – (16r2y4(a2–1)+1–u2)^2 – (((a+u2(u2–a))^2 –1)(n+4dy)^2 + 1 – (x+cu)2)2 – (n+l+v–y)^2 – ((a2–1)l2+1–m2)2 – (ai+k+1–l–i)^2 – (p+l(a–n–1)+b(2an+2a–n2–2n–2)–m)2 – (q+y(a–p–1)+s(2ap+2a–p2–2p–2)–x)2 – (z+pl(a–p)+t(2ap–p2–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

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 b = b a $ gehört zur \({\operatorname{Th}}(\text{\)$ mit Multipl.})\(, aber nicht zu \){}()$.

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) (f(f(g(x))) 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.

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.

Testklausur KW23

SAT, CNF, Kodierung

ROBDD

Definieren Sie (jeweils Wort und Bedeutung): B, R, O.

Für die boolesche Funktion \(G\):

\[{\operatorname{bin}}(x_1,x_0) \ge {\operatorname{bin}}(y_1,y_0)\]

(Größenvergleiche von Binärzahlen,
\(x_0\) und \(y_0\) sind jeweils LSB)

Lineare Ungleichungen

Für das Ungleichungssystem:

$ x_1 + x_2 x_3 x_2 x_1 +7 x_1+ 10 x_3 + x_2$,

Differenz-Logik

Die Erfüllbarkeit einer Konjunktion von Differenz-Constraints kann reduziert werden auf eine Eigenschaft eines Graphen.

(jeweils allgemein und am Beispiel

\(x_1 \le x_2+3 \wedge x_2\le x_3+4 \wedge x_3\le x_1-7 \wedge x_4 + 5\le x_2\))

In welchen Anwendungsproblemen treten solche Constraints auf? (Was ist dabei die Bedeutung der Variablen, was die Bedeutung der Zahlen?)

EC/UF

EC: Equality-Constraints

UF: EC mit uninterpretierten Funktionen

Presburger-Arithmetik (PA)

Wir definieren eine Folge \(F_0, F_1,\ldots\) von Formeln durch

\(F_0(x,z)=(x+1=z), F_{k+1}(x,z) = \exists y: F_k(x,y)\wedge F_k(y,z)\).

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 $ x: 0x< i 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 $ i_1, , i_k: (I 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?

Nelson-Oppen (I)

(Wdhlg) Formel/Ausdruck

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.

SMT, DPLL(T)

SMT

SMT \(=\) Satisfiability modulo Theory

Literatur: Kroening/Strichman, Kap. 12

DPLL(T)

Ansatz: für jedes Atom \(F = P(t_1,\ldots,t_k)\)
eine neue boolesche Unbekannte \(p_F \leftrightarrow F\), dann:

Ideen zur Realisierung/Verbesserung:

DPLL(T), Beispiel

T \(=\) LRA (linear real arithmetic)

durch Tseitin-Transformation als CNF darstellen (zusätzliche boolesche Variablen)

DPLL(T) benutzt

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

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

DPLL(T) Übung

DPLL/CDCL

CDCL: Spezifikation

conflict driven clause learning

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

Bitblasting

Idee

Constraints für ganze Zahlen

die Zahlen werden gesprengt (blast \(=\) Explosion)

und man rechnet mit ihren Bits (CNF-SAT)

(nach Festlegung der Bitbreite der Zahlen)

\(x = [x_0,x_1,\ldots,x_{w-1}]\)

Notation hier: LSB ist links

Binäre Addition

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

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

Realisierung:

dafür CNF ohne Hilfsvariablen!

Subtraktion

Vergleiche

Größer: \(x = [x_0,\ldots] > [y_0,\ldots] = y\), falls

Gleich: \(x = [x_0,\ldots] = [y_0,\ldots] = y\), falls

Damit \(x>y\) mit linear vielen Variablen und Klauseln möglich. Welches sind die besten Faktoren?

Multiplikation

\([x_0,\ldots] \cdot [y_0,\ldots]\),

SAT-Formeln für binäre Multiplikation sind sehr schwer: Resultatbit \(k\) hängt von allen Eingabebits \(0,\dots,k\) ab.

Bitshift

\(x\ll y = z\) …um einen unbekannten Betrag \(y\)!

(Hausaufgabe.)

Unärkodierung

CNF-Kompression (Motivation) vereinfachte Annahme:

SAT-Solver ist schneller, wenn

führt zu der Aufgabe:

Anwendungen:

Aber: mehr Klauseln \(\Rightarrow\) mehr Propagationen

CNF-Kompression (Implementierung)

zu gegebener Formel \(F\) bestimme Menge der Prim-Implikanten \(P=\{P_1,\ldots\}\),

das sind minimale Klauseln \(P_i\) mit \(F\rightarrow P_i\)

(minimal bezüglich Inklusion von Literalen)

dann bestimme eine kleinste Teilmenge \(M \subseteq P\) mit \(\bigwedge M \rightarrow F\).

das ist eine ganzzahlige lineare Optimierungsaufgabe (Übung: welche?), kann durch entsprechende Constraint-Solver gelöst werden (glpsol, scip, clp)

Diskussion: http://groups.google.com/group/minisat/msg/012bb4712c7e90a7

Anwendung: https://github.com/jwaldmann/satchmo/blob/master/Satchmo/Binary/Op/Common.hs#L118

Zusammenfassung, Ausblick

Kernaussagen

Kernthemen

Aussagenlogik (SAT)

Prädikatenlogik: Bereiche und -spezifische Verfahren:

Prädikatenlogik: allgemeine Verfahren:

Themen zum Weiterarbeiten