Matchings
Def: Ist G=(V,E) ein Graph, dann nennt man eine Teilmenge M⊆E ein Matching, wenn jeder Knoten aus V zu höchstens einer Kante aus M inzident ist.
Ein Matching maximaler Größe wird Maximum-Matching genannt. Die Größe eines Maximummatchings ist m (G)
Achtung: Nicht jedes Inklusions-maximale Matching ist ein Maximum-Matching
Beispiel:
(Graph: Quadrat mit jeweils 1 Weiteren Kante zu je einem Punkt außerhalb des Quadrats von jeder Ecke aus, 2 Gegenüberleigende Seiten des Quadrats sind Rot gefärbt(M), die Knten nach außen sind Gelb(M'))
M ist inklusions-maximal
M' ist Maximum-Matching
Def: Sei M ein Matching in G=(V,E).
Ein Knoten v€V ist M-Saturiert, wenn v inzident zu einem e€M ist.
Ein Weg in G ist M-augmentierend, wenn er m M-unsatorierten Knoten beginnt und endet und auf dem Weg Kanten aus M und aus E\M alternierend auftreten.
Grüner Weg im Graph: anfangend von einem der Außenpunkte über 3 Seiten im Quadrat und an einem anderen Außenpunkt endend:
M-augmentierender Weg
Beobachtung: Ist M ein Matching mit einem M-Augmentierenden Weg dann ist |M|≠m(G) und man kann M durch einen Knotenaustausch um eine Kante Vergrößern:
Auf dem Weg werden alle Kanten aus M gestrichen und alle Kanten aus E\M aufgenommen.
Perfektes Matching: |M|=|E|\2
Heiratssatz: Ist G=(AuB,E) ein bipartiter Graph. Es gibt ein Matching das alle Knoten aus A saturiert
Dann ist m(G)=|A| genau dann, wenn für jede Teilmenge
X⊆A die Ungleichung |N(X)|≥|X| gilt.
N(X): Nachbarschaft von X
Beweis: => einfach
(Punkte von A, Punkte von B, jeder Punkt von A ist mit genau einem Punkt von B verbunden) Betrachte M⊆E und |M|=m(G)=|A|
X⊆A
N(X)⊇{b€B| b inzident zu e€M und e inzident zu einem a€X}
<=: Angenommen ∀X⊆A |N(X)|≥|X| und m(G)<A
Sei M Matching mit |M|=m(G)
1)∃ a_1€A, so dass a_1 M-unsaturiert ist.
X={a_1} => |N(X)|≥1
wähle ein b_1€N(X)
2 Fälle:
1)b_1 ist M-unsaturiert -> M-Augmentierender Weg => Widerspruch
2)b_1 ist M-saturiert -> setze a_2 als Knoten aus A mit {b_1,a_2}€M
2) X={a_1,a_2}
|N(X)|≥2
Wähle b_2€N(X), b_2≠b_1
2 Fälle...usw
Da G endlich, muss irgendwann Fall 1 eintreten =>Widerspruch
a1 ----------- b1 Fett =Kanten aus E\M
∖ ⋰ nicht fett = Kanten aus M
⋅
⋰ ∖
a2 b2
⋰
⋰
a3 ----------- b3
∖ ⋰
⋅
⋰ ∖
a4 b4
Satz: Ist M ein Matching in G=(V,E) mit |M| < m(G), dann gibt es einen M-augmentierenden Weg
Beweis: Sei M' ein Maximum-Matching und H=(V,F) wobei F=(M\M')u(M'\M)=(MuM')\(MnM')
(Graph)
Was weiß man über H?
Mehr Kanten aus M' als Kanten aus M
Zusammenhangskomponenten sind alternierende Kreise gerader Länge oder es sind alternierende Wege oder isolierte Knoten.
in alternierenden Kreisen und isolierte Knoten: gleich viele Kanten aus M und M'
=> es gibt eine Komponente mit mehr Knoten aus M' als M=>M-augmentierender Weg
Algorithmus zur Suche von M-augmentierenden Wegen in bipartiten Graphen
G=(AuB,EE) M⊆E Matching
ungerichtet
1) Betrachte gerichtete Version von G
Kanten aus M: A->B
Kanten aus E\M: B->A
Führe zusätzliche Knoten s, t (Source, Target)ein
Führe für alle M-unsaturierten v€A Kanten v->T ein
für alle M-unsaturierten u€B Kante s->u
Führe DFS aus mit Startknoten s
Wenn DFS t erreicht, dann enthält der Rückweg(π-Zeiger) einen M-augmentierenden Weg (erste und letzte Kante ignorieren)
31.01.2013
Resulotionskalkül und Prädikatenlogik
Begriffe und Bezeichnungen
Var_n ={x_1,...,x_n}
Var={x_1,x_2,...}
Belegung Ω_n={ω:Var_n -> |B}
Ω={ω:Var -> |B}
F_n=Formeln der Aussagenlogik über Var_n
F=⋃[n=1 bis ∞]F_n= Formeln der Aussagenlogik über Var
Interpretation ɸ_n(ω,F) |ω:Ω_n; F:F_n
Def: F€F_n, X⊆F
F wird erfüllt von ω€Ω_n, wenn ɸ(ω,F)=1
in diesem Fall wird F erfüllbar genannt und ω wird ein Modell für F genannt
Schreibweise ω |=F
ω ist Modell für X, wenn ω|= F für alle F€X
F ist allgemeingültig (Tautologie) wenn ω |=F für alle ω€Ω_n, Schreibweise: _ |=F
F ist Kontradiktion, wenn F nicht erfüllbar ist
|= F->F Selbstimplikation
|= F ->(G->F) Prämissenbelastung
|= (F->(G->H))->(G->(F->H)) Prämissenvertauschung
|= (F->G)->((G->H)->(F->H)) gewöhnlicher Kettenschluss
|= (F->(G->H))->((F->G)->(F->H)) Fregescher Kettenschluss
Def: F ist aussagenlogische Folgerung aus der Formellänge X, wenn für alle w mit ω |= X gilt, dass auch ω |= F.
Schreibweise: X |=F, wenn X= {F_1,...,F_n} auch F_1, F_2,...,F_n |=F
Resolutionskalkül
Kalkül= Kollektion von Umformungsregeln
Ziel: Erfüllbarkeit von Formeln in KNT entscheiden
Eingabe sind Formeln der Form
(l_11 v...v l_1k_1)^(l2,1v...v l_2,k_2)^...^(l_n,1 v... v l_n,k_n)
wobei l_i,j Litearale sind, also die x_i oder !x_i=x_i haben
l={x_1 falls l=x_i; x_1 falls l=x_1
Verwenden die Klausel-Schreibweise
Die Menge der Literale in einem Disjunktionsfeld ist eine Klausel K und die KNF ist eine Menge von Klauseln
Beispiel:
F=(x_1 v !x_2 v x5)^(x3 v ! x4) ^(x2 v x3 v !x5)
K_F={{x1,!x2,x5},{x3,!x4},{x2,x3,!x5}}
Def: Sind K_1 und K_2 zwei Klauseln und l ein Literal, so dass l€K_1 und !l€K_2, dann nennt man die Klausel R=(K_1\{l})u(K_2\{!l}) einen Resolventen aus K_1 und K_2
Notation:
K_1 K_2
\ /
R
Beispiel: K_1={x1,x2,!x3,x4} K_2={!x1,x3,x4,!x5}
R1={x2, x3, !x3, x4, !x5}
R2={x1, !x1, x2, x4, !x5}
Nur 1 Literal streichen!
Resolutionslemma:
Sei F eine Formel in KNF mit Klauselbeschreibung K=K_F
Ist R ein Resolven von zwei Klauseln K_1,K_2€K, dann ist F genau dann erfüllbar, wenn die Formel mit der Klauselmenge Ku{R} erfüllbar ist
Beweis:
Sei F' Formel von K u {R}
Wenn F' erfüllbar ist, dann gibt es eine Belegung ω€Ω, so dass jede Klausel K€Ku{R} erfüllt wird
Daraus folgt ω|=F (ω ist erfüllende Belegung für F)
Angenommen ω ist erfüllende Belegung für F
und R=(K_1\{l})u(K_2\{!l}) wobei l€K_1 und !l€K_2
zu zeigen: ω erfüllt R
Fall 1: ω(l)=1 => ω(!l)=0
wenn ω |= K_2, denn muss es ein l'€K_2 mit ω(l')=1 -> l'€R => ω |=R
Fall 2: ω(l)=0, weil ω |= K_1 muss es ein l'€K_1, so dass ω(l')=1 => l'€R => ω |=R
Die leere Klausel wird mit [] bezeichnet
Sie kann als Resolvent nur dann entstehen, wenn K_1={l} und K_2={!l}
Wenn man [] ableiten kann, dann war die entsprechende Formel nicht erfüllbar.
Def: Für eine Klauselmenge K definiert man
Res(K)=K u {R | R ist Resolvent aus K_1, K_2 € K}
Res°(K)=K
Res^(n-1)(K)=Res(Res^(n)(K))
Res^(*)(K)=⋃[n=0 bis∞] Res ^(n)(K)
Resolutionssatz: Eien KNF-Formel F ist genau dann nicht erfüllbar, wenn [] € R^(*)(K_F)
=> wird Vollständigkeit des Kalküls genannt
<= wird Korrektheit des Kalküls genannt (folgt unmittelbar aus Resolutionslemma)
Algorithmus: Eingabe K=K_F
repeat
J=K
K=Res(J)
until ([]€K) or (J==K)
if []€K then return " F ist unerfüllbar"
else return "F ist erfüllbar"
Beispiel:
1{!x1,x2} 2{x1,x2,x3} 3{!x2} 4{x2,!x3}
R12={x2,x3}
R13={!x1}
R23={x1,x3}
R24={x1,x2}
R34={!x3}
.....
=>[]
05.01.2013
Formel F in KNF
↓
K_F
K_1,K_2€K_F und l€K_1, !l€K_2
R=(K_1\{l})u(K_2\{!l})
Resolvent aus K_1 und K_2
R=[]: leere Klausel; nicht erfüllbar
Resolutionssatz: Ein KNF F ist genau dann unerfüllbar, wenn man []aus Res*(K_F)
Beweis:
[]€Res*(K_F)=> Ableitung von [] nur aus K_1={x_k} und K_2={!x_k} möglich, aber dann ist F nicht erfüllbar
F nicht erfüllbar => [] € Res*(K_F)
Beweis mit vollständiger Induktion nach n, wobei F€F_n, d.h. F hat nur Variable aus {x_1,....,x_n}
IA: n=1, wenn F nicht erfüllbar, dann muss F die Klauseln {x_1} und {!x_1} enthalten => []€Res(K_F)
IS: n -> n+1
IV: Für jede nicht erfüllbare Formel (Klauselmenge) F€ F_n ist []€Res(K_F)
Sei F€ F_(n+1)
Betrachte K_F=K_0 u K_1 u K_2
wobei K_0={K€K_F|x_(n+1)∉K}
K_1={K€K_F|!x_(n+1)∉K}
K_2={K€K_F|x_(n+1) ^!x_(n+1) €K} Innerer Wert 1
Beispiel: n+1=4 (n=3)
K_F={{x1,x2},{x1,!x3},{x1,x3,x4},{!x4},{!x1,x4}}
K_0={{x1,x2},{x1,!x3},{!x4}}
K_1={{x1,x2},{x1,!x3},{x1,x3,x4},{!x1,x4}}
K_0'={K\{!x_(n+1}|K€K_0}
K_1'={K\{x_(n+1}|K€K_1}
Im Beispiel: K_0'={{x1,x2},{x1,!x3},[]}
K_1'={{x1,x2},{,!x3},{x1,x3},{!x1}}
Behauptung: K_0' und K_1' repräsentieren unerfüllbare Formeln aus F_n
Begründung:Wäre K_0' erfüllbar, dann könnt man die erfüllbare Belegung ω:Var_n->|B wird mit ω(x_(n+1))=1 mit erfüllender Belegung von F erweitert. ->Widerspruch
Wäre K_1' erfüllbar, dann........ mit ω(x_(n+1))=0 zu erfüllender Bedingung von F erweitern. -> Widerspruch
Nach IV kann man aus K_0' und K_1' jeweils [] ableiten.
Im Beispiel: []€K_0'
und {x1,x3},{!x1} -> {x3}
{x1,!x3},{!x1} -> {!x3}
{x3},{!x3} -> []
Übertrage Ableitung von [] in K_0' und K_1' auf K_0, K_1
Im Beispiel in K_0: [] ->{!x4}
in K_1: {x1,!x3} {x1,x3,x4} {!x1,x4}
{x1,x3,x4},{!x1,x4} -> {x3,x4}
{x1,!x3},{!x1,x4} -> {!x3,x4}
{x3,x4},{!x3,x4} -> {x4}
Dabei wird in K_0 aus [] entweder [] oder {!x_(n+1)}; in K_1 aus [] entweder [] oder {x_(n+1)}; Das ist alles in Res*(K_F)
->[]€Res*(K_F)
Das ist die Behauptung!
Wichtig für Anwendungen!
1) Wenn F unerfüllbar, dann reicht Ableitung von [] als Beweis aus, Berechnung von Res*(K_F) nicht notwendig
ABER wenn F erfüllbar, dann muss man Res*(K_F) vollständig bestimmen (und []∉ feststellen)
2)Niemals 2 Lierale gleichzeitig streichen
BSP: {x1,!x3},{!x1,x3} ->[]
{x1,!x3},{!x1,x3} ->{x3,!x3}
{x1,!x3},{!x1,x3} ->{X1,!x1}
3) Anwendung zum Tautologietest für Formeln in DNF
Gegeben F in DNF
Bilde !F und verwende deMorgen -> G≡!F in KNF
Resolution für G
[]€Res*(K_G)=>G nicht erfüllbar =>F ist Tautologie
[]∉Res*(K_G)=>G erfüllbar =>F ist keine Tautologie
Beispiel: F=(x1 ^ !x2) v (!x1 ^ x3) v x2 v (!2 ^ !x3)
F Tautologie?
1) !F≡!(x1 ^ !x2) v !(!x1 ^ x3) v !x2 v !(!x2 ^ !x3)
≡ (!x1 v x2) ^ (x1 v !x3) ^ !x2 ^ (x2 v x3) KNF
2) 1{!x1,x3} 2{x1,!x3} 3{!x2} 4{x2,x3}
1,3 -> 5 {!x1}
2,4 -> 6{x3}
2,6 -> 7 {x1}
5,7 ->[]
3) !F ist unerfüllbar => F ist Tautologie
Horn-Formeln
Def: EIne KNF-Formel F wird Hornformel genannt, wenn in jeder Klausel von F höchstens ein positives Literal vorkommt ( positives Literal = Variable, negatives Literal= negierte Variable)
Beispiel: (x1 v !x2 v !x4) ^ (x1 v !x3) ^ (!x1 v x2) ^ (!x2 v !x3) ^ x4
drei typische Vertreter:
1)isoliertes positives Literal
2)ohne positives Literal
3)gemischt (mit pos. und neg. Literalen)
kann man als Implikation schreiben
3) !x1 v x2 v !x4≡ (!x1 v !x4) v x2
≡ !(x1 ^ x4) v x2 ≡ (x1 ^ x4) -> x2
2) !x1 v !x3 v !x4 v 0 ≡ (x1 ^ x2 ^ x4) -> 0
1) 0 v x3 ≡ !1 v x3 ≡ 1-> x3
Wann ist eine Horn-Formel F erfüllbar?
Beobachtungen:
1) Wenn jede Klausel ein negatives Literal enthält
(Typ 2 und 3) => F erfüllbar
(setze alles auf 0)
2) Wenn jede Klausel ein positives Literal enthält => erfüllbar
3) Wenn Klausel von Typ 1, z.B. {x_k} enthalten ist, dann muss jede erfüllende Belegung x_k auf 1 setzen
Algorithmus Idee:(Markierungsalgorithmus)
Wenn einzelne positive Literale eine Kausel bilden, markiere diese Variable (1 setzen)
-> markierte Variablen in negierter Form werden in den Klauseln gestrichen
-> markierte Variablen in positiver Form werden mit ihren Klauseln gestrichen
-> Abbruch wenn [] entsteht => unerfüllbar
oder keine weiteren isolierten positiven Variablen => erfüllbar
(alle Markierten auf 1, der Rest auf 0)
07.02.2013
Markierungsalgorithmus für Hornformeln
gegeben: Hornformel F in KKlauselschreibweise K_F
while ([]∉K or K enthält Klausel der Form {x_i})
markiere x_i (x_i =1)
for all K€K
if (x_i € K) K=K\{K}
if (!x_i € K) K=K\{!x_i}
if []€K return "unerfüllbar"
else return "erfüllbar" (Erfüllende Belegung: setze alle markierten Variablen x_i auf 1, alle anderen auf 0)
Beispiel:
(x1 ^ x3 -> x4) ^ (x2-> x3) ^ ( 1 -> x1) ^ (x1 ^ x4 -> 0) ^ (1-> x2) ^ (x2 ^ x3 -> x4)
als Hornformel in Klauselschreibweise
{{!x1,!x3,x4}, {!x2,x3}, {x1}, {!x1,!x4}, {x2}, {!x2,!x3,x4}}
Markierungsalgorithmus
1) x1=1
{{!x1,!x3,x4}, {!x2,x3}, {x1}, {!x1,!x4}, {x2}, {!x2,!x3,x4}}
2) x2=1
{{!x1,!x3,x4}, {!x2,x3}, {x1}, {!x1,!x4}, {x2}, {!x2,!x3,x4}}
3) x3=1
{{x4}, {!x4},{x4}
4) x4=1
[]
=> unerfüllbar
Der Markierungsalgorithmus verwendet nur eine speziellen Art von Resolution
{x_j} {!x_j, !x_i,!xk,x_l}
{!x_j, !x_k,x_l}
Def: Ein Resolvent R=(K1\{l}) v (K2\{!l}) ist ein Einheitsresolvent, wenn |K1|=1 oder |K2|=1
Analoge Einführung von
1-Res(K)
1-Res^n (K)
1-Res*(K)
Satz: Ist F eine Hornformel, dann ist F genau dann unerfüllbar, wenn []€1-Res*(K)
Algebraische Strukturen und Prädikatenlogik
Sonderzeichen: √, ∤, |, ≥, ≤, ∑, ⊕, ≠, , ○, ⚡, Σ, π, ✓, ∞, ρ
≡, ∈, ∉, ∀, ∃, ∅, ⋂, ⋃, ∪, ⊂, ⊃, ⊆, ⊇, ⋀, ⋁, ¬, ≈
⇒, ⇔, ⟼, ↤, ☇, →, ↔, ↓, /,\
Ā, Ē, Ū, Ō, Ω, ɸ, ω, τ, ℕ, ℤ, α, β, γ, δ, ε, ⌈,⌉, ⌊,⌋