Mercurial > 13ws.ds

comparison notes/tex/logic.tex @ 20:d9b98c2ba5ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
move logic to own file
author Markus Kaiser <markus.kaiser@in.tum.de>
date Mon, 18 Nov 2013 15:12:27 +0100
parents
children dc6b569c57c8
comparison
equal deleted inserted replaced
19:845ff8b2cbc6 20:d9b98c2ba5ac
1 \defineUnit{aussagenlogiksyntax}{%
2 \begin{frame}[c]
3 \frametitle{Syntax der Aussagenlogik}
4 \setbeamercovered{dynamic}
5
6 \begin{definition}[Syntax der Aussagenlogik]
7 Aussagenlogische \structure{Formeln} bestehen aus Konstanten, Variablen und Operatoren. Die Menge \structure{$\mathcal{F}$} aller Formeln ist induktiv definiert.
8 \begin{itemize}
9 \item $\mathrm{false} = 0 \in \mathcal{F},\quad \mathrm{true} = 1 \in \mathcal{F}$\hfill(\alert{Konstanten})
10 \item $V = \left\{ a, b, c,\ldots \right\} \subseteq \mathcal{F}$\hfill(\alert{Variablen})\\
11 \medskip
12 \item Ist $A \in \mathcal{F}$ eine aussagenlogische Formel, dann auch
13 \begin{align}
14 \neg A &\in \mathcal{F}\tag{\alert{Negation}}\\
15 \intertext{\item Sind $A, B \in \mathcal{F}$ aussagenlogische Formeln, dann auch}
16 (A \wedge B)&\in \mathcal{F}\tag{\alert{Konjunktion}}\\
17 (A \vee B)&\in \mathcal{F}\tag{\alert{Disjunktion}}\\
18 (A \rightarrow B)&\in \mathcal{F}\tag{\alert{Implikation}}
19 \end{align}
20 \end{itemize}
21 Alle Formeln lassen sich so konstruieren.
22 \end{definition}
23 \end{frame}
24
25 \begin{frame}
26 \frametitle{Operatorenbindung}
27 \setbeamercovered{dynamic}
28
29 \begin{definition}[Bindungsregeln]
30 Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist
31 \[ \neg \quad \wedge \quad \vee \quad \rightarrow \quad \leftrightarrow \]
32 Die Implikation ist \structure{rechtsassoziativ}
33 \[ a \rightarrow b \rightarrow c \rightarrow d\text{\quad steht für\quad} \left( a \rightarrow \left( b \rightarrow \left( c \rightarrow d \right) \right) \right) \]
34 \end{definition}
35 \begin{itemize}
36 \item Üblicherweise klammert man $\wedge$ und $\vee$
37 \[ (a \wedge b) \vee c \text{\quad statt\quad} a \wedge b \vee c \]
38 \end{itemize}
39 \begin{example}[]
40 \begin{itemize}
41 \item $\neg a \wedge b$\quad steht für \quad$ \left( \left( \neg a \right) \wedge b \right)$
42 \item $a \wedge b \rightarrow c \vee \neg d$\quad steht für \quad$((a \wedge b) \rightarrow (c \vee \left( \neg d \right)))$
43 \end{itemize}
44 \end{example}
45 \end{frame}
46
47 \begin{frame}
48 \frametitle{Syntaxbaum}
49 \setbeamercovered{dynamic}
50
51 \begin{block}{Syntaxbaum}
52 \structure{Syntaxbäume} visualisieren in welcher Reihenfolge die Regeln zur induktiven Definition angewandt werden müssen, um eine Formel zu erzeugen.
53 \end{block}
54 \begin{example}[]
55 Sei $F \defeq a \wedge b \rightarrow c \vee \neg d$ dann ist der dazu passende Syntaxbaum
56 \centering
57 \begin{tikzpicture}[grow=down, level distance = 33]
58 \tikzstyle{every node} = []
59 \tikzstyle{op} = [pretty]
60 \tikzstyle{var} = [pretty, rectangle]
61 \tikzstyle{edge from parent} = [edge]
62
63 \tikzstyle{level 1} = [sibling distance = 80]
64 \tikzstyle{level 2} = [sibling distance = 40]
65 \node[op] {$\rightarrow$}
66 child {
67 node[op] {$\wedge$}
68 edge from parent
69 child {
70 node[var] {$a$}
71 edge from parent
72 }
73 child {
74 node[var] {$b$}
75 edge from parent
76 }
77 }
78 child {
79 node[op] {$\vee$}
80 edge from parent
81 child {
82 node[var] {$c$}
83 edge from parent
84 }
85 child {
86 node[op] {$\neg$}
87 edge from parent
88 child {
89 node[var] {$d$}
90 edge from parent
91 }
92 }
93 };
94 \end{tikzpicture}
95 \end{example}
96 \end{frame}
97 }
98
99 \defineUnit{aussagenlogiksemantik}{%
100 \begin{frame}
101 \frametitle{Belegung}
102 \setbeamercovered{dynamic}
103
104 \begin{definition}[Belegung]
105 Eine passende \structure{Belegung} $\beta$ zu einer Formel $F$ ordnet jeder Variable in $V$ einen Wahrheitswert aus $\left\{ 0, 1 \right\}$ zu. Es ist
106 \[ \beta : V \to \left\{ 0, 1 \right\} \]
107 \end{definition}
108 \begin{itemize}
109 \item Belegungen formalisieren Einsetzen
110 \item Für $n$ Variablen existieren $2^n$ Belegungen
111 \end{itemize}
112 \begin{example}[]
113 Sei $F \defeq \neg \left( a \wedge b \right)$ mit $V = \left\{ a, b \right\}$ und
114 \begin{align}
115 \beta : \left\{ a, b \right\} &\to \left\{ 0, 1 \right\}\\
116 a &\mapsto 1\\
117 b &\mapsto 0
118 \end{align}
119 Dann ist $\beta$ eine zu $F$ passende \structure{Belegung}.
120 \end{example}
121 \end{frame}
122
123 \begin{frame}
124 \frametitle{Semantik der Aussagenlogik}
125 \setbeamercovered{dynamic}
126
127 \begin{definition}[Semantik einer Formel]
128 Die \structure{Semantik} $[F]$ einer aussagenlogischen Formel $F$ ist eine Funktion, die jeder passenden Belegung $\beta$ einen Wahrheitswert zuordnet.\\
129 Sei $\mathcal{B} = \left\{ \beta_0, \beta_1, \ldots \right\}$ die Menge aller Belegungen zu $F$. Dann ist
130 \[[F] : \mathcal{B} \to \left\{ 0, 1 \right\}\]
131 \end{definition}
132 \begin{itemize}
133 \item Die Semantik löst eingesetzte Formeln auf
134 \item Wird anhand der induktiven Syntax definiert
135 \item Es gibt \alert{syntaktisch verschiedene} Formeln gleicher \structure{Semantik}
136 \end{itemize}
137 \begin{example}[]
138 Sei $F \defeq \left( G \rightarrow H \right)$ mit $G, H$ Formeln. Dann ist
139 \[ [F](\beta) = \begin{cases}
140 0 & \text{falls } [G](\beta) = 1 \text{ und } [H](\beta) = 0 \\
141 1 & \text{sonst}
142 \end{cases}\]
143 \end{example}
144 \end{frame}
145
146 \begin{frame}
147 \frametitle{Wahrheitstabelle}
148 \setbeamercovered{dynamic}
149
150 \begin{block}{Wahrheitstabelle}
151 Die Semantik einer Formel kann mit Hilfe einer \structure{Wahrheitstabelle} visualisiert werden. Die Tabelle gibt den Wahrheitswert der Formel für jede mögliche Belegung an.
152 \end{block}
153 \begin{example}[]
154 Sei $F \defeq a \vee b \rightarrow \neg c \wedge b$. Die zu $[F]$ gehörige Wahrheitstabelle ist
155 \begin{center}
156 \begin{tabu} to .5\textwidth {cccX|[1.2pt]Xccccc}
157 a & b & c & & & $a \vee b$ & $\rightarrow$ & $\neg c$ & $\wedge$ & $b$ \\ \tabucline[1.2pt]{-}
158 0 & 0 & 0 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{0} & \\
159 0 & 0 & 1 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{0} & \onslide<2->{0} & \\
160 0 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\
161 0 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\
162 1 & 0 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{1} & \onslide<2->{0} & \\
163 1 & 0 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\
164 1 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\
165 1 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\
166 \end{tabu}
167 \end{center}
168 \end{example}
169 \end{frame}
170
171 \begin{frame}
172 \frametitle{Äquivalente Formeln}
173 \setbeamercovered{dynamic}
174
175 \begin{definition}[Äquivalente Formeln]
176 Man nennt zwei Formeln \structure{äquivalent}, wenn sie dieselbe Semantik besitzen.\\
177 Seien $F, G$ Formeln mit Belegungen $\mathcal{B} = \mathcal{B}_F = \mathcal{B}_G$. $F$ und $G$ sind äquivalent wenn
178 \[ \forall \beta \in \mathcal{B}. [F](\beta) = [G](\beta) \]
179 Man schreibt \structure{$F \equiv G$} oder \structure{$F \leftrightarrow G$}.
180 \end{definition}
181
182 \begin{example}[]
183 Für $F \defeq a \rightarrow b$ und $G \defeq \neg a \vee b$ gilt $F \equiv G$.
184 \begin{center}
185 \begin{tabu} to .4\textwidth {cc|[1.2pt]XcX||Xccc}
186 a & b & & $a \Rightarrow b$ & & & $\neg a$ & $\vee$ & $b$ \\ \tabucline[1.2pt]{-}
187 0 & 0 & & \structure{1} & & & 1 & \structure{1} \\
188 0 & 1 & & \structure{1} & & & 1 & \structure{1} \\
189 1 & 0 & & \structure{0} & & & 0 & \structure{0} \\
190 1 & 1 & & \structure{1} & & & 0 & \structure{1} \\
191 \end{tabu}
192 \end{center}
193 \end{example}
194 \end{frame}
195
196 \begin{frame}
197 \frametitle{Eigenschaften von Formeln}
198 \setbeamercovered{dynamic}
199
200 \begin{block}{Eigenschaften aussagenlogischer Formeln}
201 Sei $F$ eine aussagenlogische Formel mit Variablen $V$ und der Menge der passenden Belegungen $\mathcal{B}$. Man nennt F
202 \begin{description}[\quad unerfüllbar]
203 \item[erfüllbar] $\exists \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ kann wahr sein)
204 \item[unerfüllbar] $\forall \beta \in \mathcal{B}. [F](\beta) = 0$\hfill($F$ ist nie wahr)
205 \item[gültig] $\forall \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ ist immer wahr)
206 \end{description}
207 \end{block}
208 \begin{itemize}
209 \item Eine unerfüllbare Formel nennt man \structure{Widerspruch}
210 \item Eine gültige Formel nennt man \structure{Tautologie}
211 \end{itemize}
212
213 \end{frame}
214 }
215
216 \defineUnit{aussagenlogikaequivalenzen}{%
217 {
218 \newcommand{\true}{1}
219 \newcommand{\false}{0}
220 \newcommand{\spc}{\hspace{3em}}
221 \newcommand{\F}{F}
222 \newcommand{\G}{G}
223 \newcommand{\K}{H}
224
225 \begin{frame}
226 \frametitle{Äquivalenzregeln}
227 \setbeamercovered{dynamic}
228
229 \begin{description}[Triviale Kontradiktion\quad]
230 \item[Identität] $\F \wedge \true \equiv \F \spc \F \vee \false \equiv \F$
231 \item[Dominanz] $\F \vee \true \equiv \true \spc \F \wedge \false \equiv \false$
232 \item[Idempotenz] $\F \vee \F \equiv \F \spc \F \wedge \F \equiv \F$
233 \item[Doppelte Negation] $\neg \neg \F \equiv \F$
234 \item[Triviale Tautologie] $\F \vee \neg \F \equiv \true$
235 \item[Triviale Kontradiktion] $\F \wedge \neg \F \equiv \false$
236 \bigskip
237 \item[Kommutativität] $\F \vee \G \equiv \G \vee \F$\\
238 $\F \wedge \G \equiv \G \wedge \F$
239 \item[Assoziativität] $(\F \vee \G) \vee \K \equiv \F \vee (\G \vee \K)$\\
240 $(\F \wedge \G) \wedge \K \equiv \F \wedge (\G \wedge \K)$
241 \item[Distributivität] $\F \vee (\G \wedge \K) \equiv (\F \vee \G) \wedge (\F \vee \K)$\\
242 $\F \wedge (\G \vee \K) \equiv (\F \wedge \G) \vee (\F \wedge \K)$
243 \item[De Morgan] $\neg(\F \wedge \G) \equiv \neg \F \vee \neg \G$\\
244 $\neg(\F \vee \G) \equiv \neg\F \wedge \neg\G$
245 \bigskip
246 \item[Implikation] $\F \rightarrow \G \equiv \neg \F \vee \G$
247 \item[Bikonditional] $\F \leftrightarrow \G \equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F)$
248 \end{description}
249 \end{frame}
250
251 %\begin{frame}
252 %\frametitle{Äquivalenzregeln}
253 %\setbeamercovered{dynamic}
254
255 %\vspace{-2em}
256 %\begin{align}
257 %\F \wedge \true &\equiv \F \spc \F \vee \false \equiv \F \tag{\structure{Identität}}\\
258 %\F \vee \true &\equiv \true \spc \F \wedge \false \equiv \false \tag{\structure{Dominanz}}\\
259 %\F \vee \F &\equiv \F \spc \F \wedge \F \equiv \F \tag{\structure{Idempotenz}}\\
260 %\neg \neg \F &\equiv \F \tag{\structure{Doppelte Negation}}\\
261 %\F \vee \neg \F &\equiv \true \tag{\structure{Triviale Tautologie}}\\
262 %\F \wedge \neg \F &\equiv \false \tag{\structure{Triviale Kontradiktion}}\\
263 %\bigskip
264 %\F \vee \G &\equiv \G \vee \F \tag{\structure{Kommutativität}}\\
265 %\F \wedge \G &\equiv \G \wedge \F\\
266 %(\F \vee \G) \vee \K &\equiv \F \vee (\G \vee \K) \tag{\structure{Assoziativität}}\\
267 %(\F \wedge \G) \wedge \K &\equiv \F \wedge (\G \wedge \K)\\
268 %\F \vee (\G \wedge \K) &\equiv (\F \vee \G) \wedge (\F \vee \K) \tag{\structure{Distributivität}}\\
269 %\F \wedge (\G \vee \K) &\equiv (\F \wedge \G) \vee (\F \wedge \K)\\
270 %\neg(\F \wedge \G) &\equiv \neg \F \vee \neg \G \tag{\structure{De Morgan}}\\
271 %\neg(\F \vee \G) &\equiv \neg\F \wedge \neg\G\\
272 %\bigskip
273 %\F \rightarrow \G &\equiv \neg \F \vee \G \tag{\structure{Implikation}}\\
274 %\F \leftrightarrow \G &\equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \tag{\structure{Bikonditional}}\\
275 %\end{align}
276 %\end{frame}
277 }
278 }
279
280 \defineUnit{aussagenlogiknormalformen}{%
281 \begin{frame}[c]
282 \frametitle{Literale und Klauseln}
283 \setbeamercovered{dynamic}
284
285 \begin{definition}[Literal]
286 Ein \structure{Literal} ist eine Variable $v \in V$ oder die Negation $\neg v$ einer Variable.
287 \end{definition}
288
289 \begin{definition}[Klausel]
290 Eine \structure{Klausel} verknüpft mehrere Literale mit einem assoziativen Operator.
291 \end{definition}
292
293 \vfill
294
295 \begin{example}[]
296 Seien $a, \neg b, c$ Literale. Dann sind
297 \begin{itemize}
298 \item $a \wedge \neg b \wedge c$
299 \item $a \vee \neg b \vee c$
300 \end{itemize}
301 Klauseln.
302 \end{example}
303 \end{frame}
304
305 {
306 \newcommand{\klausel}[2]{\underbracket{(##2)}_{\text{##1-Klausel}}}
307 \begin{frame}
308 \frametitle{DNF}
309 \setbeamercovered{dynamic}
310
311 \begin{definition}[Disjunktive Normalform]
312 Eine \structure{DNF-Klausel} ist eine Konjunktion von Literalen $L_i$.\\
313 Eine Formel $F$, ist in \structure{Disjunktiver Normalform}, wenn sie eine Disjunktion von DNF-Klauseln ist.
314 \[ F \defeq \bigvee \bigwedge_i L_i \]
315 \end{definition}
316 \begin{itemize}
317 \item Ausnahme: $\textrm{false}$ ist auch in DNF
318 \end{itemize}
319
320 \begin{example}[]
321 $F$ ist in DNF.
322 \[ F \defeq \klausel{DNF}{a \structure{\wedge} b \structure{\wedge} \neg c} \alert{\vee} \klausel{DNF}{\neg b \structure{\wedge} c} \alert{\vee} \klausel{DNF}{\neg a \structure{\wedge} b \structure{\wedge} \neg c} \]
323 \end{example}
324 \end{frame}
325
326 \begin{frame}
327 \frametitle{KNF}
328 \setbeamercovered{dynamic}
329
330 \begin{definition}[Konjunktive Normalform]
331 Eine \structure{KNF-Klausel} ist eine Disjunktion von Literalen $L_i$.\\
332 Eine Formel $F$, ist in \structure{Konjunktiver Normalform}, wenn sie eine Konjunktion von KNF-Klauseln ist.
333 \[ F \defeq \bigwedge \bigvee_i L_i \]
334 \end{definition}
335 \begin{itemize}
336 \item Ausnahme: $\textrm{true}$ ist auch in KNF
337 \end{itemize}
338
339 \begin{example}[]
340 $F$ ist in KNF.
341 \[ F \defeq \klausel{KNF}{\neg a \alert{\vee} b} \structure{\wedge} \klausel{KNF}{\neg b \alert{\vee} c} \structure{\wedge} \klausel{KNF}{a \alert{\vee} b \alert{\vee} \neg c} \]
342 \end{example}
343 \end{frame}
344 }
345
346 \begin{frame}
347 \frametitle{Konstruktion der NF}
348 \setbeamercovered{dynamic}
349
350 \begin{itemize}
351 \item \structure{Jede} nicht-triviale Formel ist in DNF und KNF umwandelbar
352 \item Durch Äquivalenzumformungen berechenbar (exponentiell groß!)
353 \item Oder: Konstruktion mit Wahrheitstabellen
354 \end{itemize}
355
356 \vfill
357
358 \begin{block}{Normalformen aus Wahrheitstabellen}
359 Gegeben eine Formel $F$ und ihre Wahrheitstabelle
360 \begin{itemize}
361 \item DNF
362 \begin{enumerate}
363 \item Betrachte Zeilen mit Eintrag \structure{$1$}
364 \item Bilde \structure{Konjunktion} aus der \structure{Belegung}
365 \item Bilde \structure{Disjunktion} aller erhaltenen Klauseln
366 \end{enumerate}
367 \bigskip
368 \item KNF
369 \begin{enumerate}
370 \item Betrachte Zeilen mit Eintrag \alert{$0$}
371 \item Bilde \alert{Disjunktion} aus der \alert{Negation} der Belegung
372 \item Bilde \alert{Konjunktion} aller erhaltenen Klauseln
373 \end{enumerate}
374 \end{itemize}
375 \end{block}
376 \end{frame}
377
378 {
379 \newcommand{\klausel}[4]{(##2 a ##1 ##3 b ##1 ##4 c)}
380 \begin{frame}
381 \frametitle{Konstruktion der NF}
382 \setbeamercovered{dynamic}
383
384 \begin{example}[]
385 Gegeben eine Formel $F$ mit folgender Semantik
386 \begin{center}
387 \begin{tabu} to .4\textwidth {ccc|[1.2pt]c}
388 a & b & c & $F$ \\ \tabucline[1.2pt]{-}
389 0 & 0 & 0 & 0 \\
390 0 & 0 & 1 & 0 \\
391 0 & 1 & 0 & 0 \\
392 0 & 1 & 1 & 1 \\
393 1 & 0 & 0 & 1 \\
394 1 & 0 & 1 & 1 \\
395 1 & 1 & 0 & 1 \\
396 1 & 1 & 1 & 0
397 \end{tabu}
398 \end{center}
399 $F$ dargestellt in
400 \begin{itemize}
401 \item DNF $\hfill\klausel{\wedge}{\neg}{}{} \vee (a \wedge \neg b) \vee \klausel{\wedge}{}{}{\neg}\hfill$
402 \medskip
403 \item KNF $\hfill(a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}\hfill$
404 \end{itemize}
405 \end{example}
406 \end{frame}
407
408 \begin{frame}
409 \frametitle{Mengendarstellung der KNF}
410 \setbeamercovered{dynamic}
411
412 \begin{block}{Mengendarstellung der KNF}
413 Eine Formel $F = \bigwedge \bigvee L_i$ in \structure{KNF} kann in einer \structure{Mengendarstellung} repräsentiert werden.
414 \begin{itemize}
415 \item Klauseln werden durch Mengen von Literalen dargestellt
416 \[\left\{ a, \neg b, c \right\} \text{ steht für } (a \vee \neg b \vee c)\]
417 \item KNF-Formeln sind Mengen von Klauseln
418 \[ \left\{ \left\{ \neg a \right\}, \left\{ a, \neg b, c \right\} \right\} \text{ steht für } \neg a \wedge (a \vee \neg b \vee c) \]
419 \item $\emptyset$ steht für \textrm{true}, $\left\{ \emptyset \right\}$ für \textrm{false}
420 \end{itemize}
421 \end{block}
422 \begin{example}[]
423 Gegeben $F \defeq (a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}$ in KNF.
424 \[ \left\{ \left\{ a, b \right\}, \left\{ \neg a, b, \neg c \right\}, \left\{ \neg a, \neg b, \neg c \right\} \right\}\]
425 \end{example}
426 \end{frame}
427 }
428 }
429
430 \defineUnit{DPLL}{%
431 \begin{frame}
432 \frametitle{KNF aus Syntaxbaum}
433 \setbeamercovered{dynamic}
434
435 \begin{block}{Idee}
436 Erzeuge die KNF aus dem Syntaxbaum
437 \begin{enumerate}
438 \item<1-> Weise jedem \structure{inneren Knoten} eine Variable zu
439 \item<1,3-> Variablen sind \structure{abhängig} von ihren Kindern
440 \item<1,4-> Berechne \structure{kleine} KNFs und führe diese \structure{zusammen}
441 \end{enumerate}
442 \end{block}
443 \begin{columns}[T]
444 \begin{column}{.7\textwidth}
445 % FIXME: onlys around A_\vee needed for "correct" fadein
446 \begin{align}
447 (x \wedge y) \vee z
448 \uncover<3->{\equiv &\hphantom{{}\wedge {}}\only<3->{A_\vee}\\
449 &\structure{\wedge (A_\vee \leftrightarrow A_\wedge \vee z)}\\
450 &\alert{\wedge (A_\wedge \leftrightarrow x \wedge y)}\\}
451 \uncover<4->{\equiv &\hphantom{{}\wedge {}}\only<4->{A_\vee}\\
452 &\structure{\wedge (A_\vee \vee \neg A_\wedge) \wedge (A_\vee \vee \neg z)}\\
453 &\qquad\structure{\wedge (\neg A_\vee \vee A_\wedge \vee z)}\\
454 &\alert{\wedge (\neg A_\wedge \vee x) \wedge (\neg A_\wedge \vee y)} \\
455 &\qquad\alert{\wedge(A_\wedge \vee \neg x \vee \neg y)}}
456 \end{align}
457 \end{column}
458 \begin{column}{.3\textwidth}
459 \begin{tikzpicture}[grow=down, level distance = 33]
460 \tikzstyle{op} = [pretty]
461 \tikzstyle{var} = [pretty, rectangle]
462 \tikzstyle{edge from parent} = [edge]
463
464 \tikzstyle{level 1} = [sibling distance = 50]
465 \tikzstyle{level 2} = [sibling distance = 30]
466 \node at (0, 0) {};
467 \node[op] at (0, -1) {\alt<1>{$\vee$}{$A_\vee$}}
468 child {
469 node[op] {\alt<1>{$\wedge$}{$A_\wedge$}}
470 edge from parent
471 child {
472 node[var] {$x$}
473 edge from parent
474 }
475 child {
476 node[var] {$y$}
477 edge from parent
478 }
479 }
480 child {
481 node[var] {$z$}
482 };
483 \end{tikzpicture}
484 \end{column}
485 \end{columns}
486 \end{frame}
487
488 \begin{frame}
489 \frametitle{DPLL}
490 \setbeamercovered{dynamic}
491
492 \begin{definition}[DPLL-Belegung]
493 Sei $F$ eine Formel in KNF und $p$ eine Variable von $F$.\\
494 Dann bezeichnet \structure{$F[p\backslash\mathrm{true}]$} die Formel, die entsteht, wenn jedes Vorkommnis von $p$ in F durch $\mathrm{true}$ ersetzt und vereinfacht wird.
495 \end{definition}
496
497 \begin{block}{DPLL}
498 Gegeben eine Formel $F$ in KNF
499 \begin{itemize}
500 \item Wenn $F = \mathrm{true}$ dann antworte \enquote{erfüllbar}
501 \item Wenn $F = \mathrm{false}$ dann antworte \enquote{unerfüllbar}
502 \item Sonst
503 \begin{enumerate}
504 \item Wähle eine Variable $p$ in $F$
505 \item Prüfe ob $F[p\backslash\mathrm{true}]$ oder $F[p\backslash\mathrm{false}]$ erfüllbar
506 \end{enumerate}
507 \end{itemize}
508 \end{block}
509 \begin{itemize}
510 \item Schlaue Wahl der Variable beschleunigt Ausführung
511 \item Wähle Variablen die einzeln stehen (\structure{One-Literal-Rule})
512 \end{itemize}
513 \end{frame}
514 }