Mercurial > 13ws.ds
changeset 20:d9b98c2ba5ac
move logic to own file
| author | Markus Kaiser <markus.kaiser@in.tum.de> |
|---|---|
| date | Mon, 18 Nov 2013 15:12:27 +0100 |
| parents | 845ff8b2cbc6 |
| children | 03a0cf37ddaa |
| files | notes/tex/basics.tex notes/tex/frames.tex notes/tex/logic.tex |
| diffstat | 3 files changed, 515 insertions(+), 515 deletions(-) [+] |
line wrap: on
line diff
--- a/notes/tex/basics.tex Sat Nov 16 19:05:35 2013 +0100 +++ b/notes/tex/basics.tex Mon Nov 18 15:12:27 2013 +0100 @@ -576,518 +576,3 @@ \end{frame} } } - -\defineUnit{aussagenlogiksyntax}{% -\begin{frame}[c] - \frametitle{Syntax der Aussagenlogik} - \setbeamercovered{dynamic} - - \begin{definition}[Syntax der Aussagenlogik] - Aussagenlogische \structure{Formeln} bestehen aus Konstanten, Variablen und Operatoren. Die Menge \structure{$\mathcal{F}$} aller Formeln ist induktiv definiert. - \begin{itemize} - \item $\mathrm{false} = 0 \in \mathcal{F},\quad \mathrm{true} = 1 \in \mathcal{F}$\hfill(\alert{Konstanten}) - \item $V = \left\{ a, b, c,\ldots \right\} \subseteq \mathcal{F}$\hfill(\alert{Variablen})\\ - \medskip - \item Ist $A \in \mathcal{F}$ eine aussagenlogische Formel, dann auch - \begin{align} - \neg A &\in \mathcal{F}\tag{\alert{Negation}}\\ - \intertext{\item Sind $A, B \in \mathcal{F}$ aussagenlogische Formeln, dann auch} - (A \wedge B)&\in \mathcal{F}\tag{\alert{Konjunktion}}\\ - (A \vee B)&\in \mathcal{F}\tag{\alert{Disjunktion}}\\ - (A \rightarrow B)&\in \mathcal{F}\tag{\alert{Implikation}} - \end{align} - \end{itemize} - Alle Formeln lassen sich so konstruieren. - \end{definition} -\end{frame} - -\begin{frame} - \frametitle{Operatorenbindung} - \setbeamercovered{dynamic} - - \begin{definition}[Bindungsregeln] - Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist - \[ \neg \quad \wedge \quad \vee \quad \rightarrow \quad \leftrightarrow \] - Die Implikation ist \structure{rechtsassoziativ} - \[ 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) \] - \end{definition} - \begin{itemize} - \item Üblicherweise klammert man $\wedge$ und $\vee$ - \[ (a \wedge b) \vee c \text{\quad statt\quad} a \wedge b \vee c \] - \end{itemize} - \begin{example}[] - \begin{itemize} - \item $\neg a \wedge b$\quad steht für \quad$ \left( \left( \neg a \right) \wedge b \right)$ - \item $a \wedge b \rightarrow c \vee \neg d$\quad steht für \quad$((a \wedge b) \rightarrow (c \vee \left( \neg d \right)))$ - \end{itemize} - \end{example} -\end{frame} - -\begin{frame} - \frametitle{Syntaxbaum} - \setbeamercovered{dynamic} - - \begin{block}{Syntaxbaum} - \structure{Syntaxbäume} visualisieren in welcher Reihenfolge die Regeln zur induktiven Definition angewandt werden müssen, um eine Formel zu erzeugen. - \end{block} - \begin{example}[] - Sei $F \defeq a \wedge b \rightarrow c \vee \neg d$ dann ist der dazu passende Syntaxbaum - \centering - \begin{tikzpicture}[grow=down, level distance = 33] - \tikzstyle{every node} = [] - \tikzstyle{op} = [pretty] - \tikzstyle{var} = [pretty, rectangle] - \tikzstyle{edge from parent} = [edge] - - \tikzstyle{level 1} = [sibling distance = 80] - \tikzstyle{level 2} = [sibling distance = 40] - \node[op] {$\rightarrow$} - child { - node[op] {$\wedge$} - edge from parent - child { - node[var] {$a$} - edge from parent - } - child { - node[var] {$b$} - edge from parent - } - } - child { - node[op] {$\vee$} - edge from parent - child { - node[var] {$c$} - edge from parent - } - child { - node[op] {$\neg$} - edge from parent - child { - node[var] {$d$} - edge from parent - } - } - }; - \end{tikzpicture} - \end{example} -\end{frame} -} - -\defineUnit{aussagenlogiksemantik}{% -\begin{frame} - \frametitle{Belegung} - \setbeamercovered{dynamic} - - \begin{definition}[Belegung] - Eine passende \structure{Belegung} $\beta$ zu einer Formel $F$ ordnet jeder Variable in $V$ einen Wahrheitswert aus $\left\{ 0, 1 \right\}$ zu. Es ist - \[ \beta : V \to \left\{ 0, 1 \right\} \] - \end{definition} - \begin{itemize} - \item Belegungen formalisieren Einsetzen - \item Für $n$ Variablen existieren $2^n$ Belegungen - \end{itemize} - \begin{example}[] - Sei $F \defeq \neg \left( a \wedge b \right)$ mit $V = \left\{ a, b \right\}$ und - \begin{align} - \beta : \left\{ a, b \right\} &\to \left\{ 0, 1 \right\}\\ - a &\mapsto 1\\ - b &\mapsto 0 - \end{align} - Dann ist $\beta$ eine zu $F$ passende \structure{Belegung}. - \end{example} -\end{frame} - -\begin{frame} - \frametitle{Semantik der Aussagenlogik} - \setbeamercovered{dynamic} - - \begin{definition}[Semantik einer Formel] - Die \structure{Semantik} $[F]$ einer aussagenlogischen Formel $F$ ist eine Funktion, die jeder passenden Belegung $\beta$ einen Wahrheitswert zuordnet.\\ - Sei $\mathcal{B} = \left\{ \beta_0, \beta_1, \ldots \right\}$ die Menge aller Belegungen zu $F$. Dann ist - \[[F] : \mathcal{B} \to \left\{ 0, 1 \right\}\] - \end{definition} - \begin{itemize} - \item Die Semantik löst eingesetzte Formeln auf - \item Wird anhand der induktiven Syntax definiert - \item Es gibt \alert{syntaktisch verschiedene} Formeln gleicher \structure{Semantik} - \end{itemize} - \begin{example}[] - Sei $F \defeq \left( G \rightarrow H \right)$ mit $G, H$ Formeln. Dann ist - \[ [F](\beta) = \begin{cases} - 0 & \text{falls } [G](\beta) = 1 \text{ und } [H](\beta) = 0 \\ - 1 & \text{sonst} - \end{cases}\] - \end{example} -\end{frame} - -\begin{frame} - \frametitle{Wahrheitstabelle} - \setbeamercovered{dynamic} - - \begin{block}{Wahrheitstabelle} - 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. - \end{block} - \begin{example}[] - Sei $F \defeq a \vee b \rightarrow \neg c \wedge b$. Die zu $[F]$ gehörige Wahrheitstabelle ist - \begin{center} - \begin{tabu} to .5\textwidth {cccX|[1.2pt]Xccccc} - a & b & c & & & $a \vee b$ & $\rightarrow$ & $\neg c$ & $\wedge$ & $b$ \\ \tabucline[1.2pt]{-} - 0 & 0 & 0 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{0} & \\ - 0 & 0 & 1 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{0} & \onslide<2->{0} & \\ - 0 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\ - 0 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ - 1 & 0 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{1} & \onslide<2->{0} & \\ - 1 & 0 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ - 1 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\ - 1 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ - \end{tabu} - \end{center} - \end{example} -\end{frame} - -\begin{frame} - \frametitle{Äquivalente Formeln} - \setbeamercovered{dynamic} - - \begin{definition}[Äquivalente Formeln] - Man nennt zwei Formeln \structure{äquivalent}, wenn sie dieselbe Semantik besitzen.\\ - Seien $F, G$ Formeln mit Belegungen $\mathcal{B} = \mathcal{B}_F = \mathcal{B}_G$. $F$ und $G$ sind äquivalent wenn - \[ \forall \beta \in \mathcal{B}. [F](\beta) = [G](\beta) \] - Man schreibt \structure{$F \equiv G$} oder \structure{$F \leftrightarrow G$}. - \end{definition} - - \begin{example}[] - Für $F \defeq a \rightarrow b$ und $G \defeq \neg a \vee b$ gilt $F \equiv G$. - \begin{center} - \begin{tabu} to .4\textwidth {cc|[1.2pt]XcX||Xccc} - a & b & & $a \Rightarrow b$ & & & $\neg a$ & $\vee$ & $b$ \\ \tabucline[1.2pt]{-} - 0 & 0 & & \structure{1} & & & 1 & \structure{1} \\ - 0 & 1 & & \structure{1} & & & 1 & \structure{1} \\ - 1 & 0 & & \structure{0} & & & 0 & \structure{0} \\ - 1 & 1 & & \structure{1} & & & 0 & \structure{1} \\ - \end{tabu} - \end{center} - \end{example} -\end{frame} - -\begin{frame} - \frametitle{Eigenschaften von Formeln} - \setbeamercovered{dynamic} - - \begin{block}{Eigenschaften aussagenlogischer Formeln} - Sei $F$ eine aussagenlogische Formel mit Variablen $V$ und der Menge der passenden Belegungen $\mathcal{B}$. Man nennt F - \begin{description}[\quad unerfüllbar] - \item[erfüllbar] $\exists \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ kann wahr sein) - \item[unerfüllbar] $\forall \beta \in \mathcal{B}. [F](\beta) = 0$\hfill($F$ ist nie wahr) - \item[gültig] $\forall \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ ist immer wahr) - \end{description} - \end{block} - \begin{itemize} - \item Eine unerfüllbare Formel nennt man \structure{Widerspruch} - \item Eine gültige Formel nennt man \structure{Tautologie} - \end{itemize} - -\end{frame} -} - -\defineUnit{aussagenlogikaequivalenzen}{% -{ - \newcommand{\true}{1} - \newcommand{\false}{0} - \newcommand{\spc}{\hspace{3em}} - \newcommand{\F}{F} - \newcommand{\G}{G} - \newcommand{\K}{H} - - \begin{frame} - \frametitle{Äquivalenzregeln} - \setbeamercovered{dynamic} - - \begin{description}[Triviale Kontradiktion\quad] - \item[Identität] $\F \wedge \true \equiv \F \spc \F \vee \false \equiv \F$ - \item[Dominanz] $\F \vee \true \equiv \true \spc \F \wedge \false \equiv \false$ - \item[Idempotenz] $\F \vee \F \equiv \F \spc \F \wedge \F \equiv \F$ - \item[Doppelte Negation] $\neg \neg \F \equiv \F$ - \item[Triviale Tautologie] $\F \vee \neg \F \equiv \true$ - \item[Triviale Kontradiktion] $\F \wedge \neg \F \equiv \false$ - \bigskip - \item[Kommutativität] $\F \vee \G \equiv \G \vee \F$\\ - $\F \wedge \G \equiv \G \wedge \F$ - \item[Assoziativität] $(\F \vee \G) \vee \K \equiv \F \vee (\G \vee \K)$\\ - $(\F \wedge \G) \wedge \K \equiv \F \wedge (\G \wedge \K)$ - \item[Distributivität] $\F \vee (\G \wedge \K) \equiv (\F \vee \G) \wedge (\F \vee \K)$\\ - $\F \wedge (\G \vee \K) \equiv (\F \wedge \G) \vee (\F \wedge \K)$ - \item[De Morgan] $\neg(\F \wedge \G) \equiv \neg \F \vee \neg \G$\\ - $\neg(\F \vee \G) \equiv \neg\F \wedge \neg\G$ - \bigskip - \item[Implikation] $\F \rightarrow \G \equiv \neg \F \vee \G$ - \item[Bikonditional] $\F \leftrightarrow \G \equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F)$ - \end{description} - \end{frame} - - %\begin{frame} - %\frametitle{Äquivalenzregeln} - %\setbeamercovered{dynamic} - - %\vspace{-2em} - %\begin{align} - %\F \wedge \true &\equiv \F \spc \F \vee \false \equiv \F \tag{\structure{Identität}}\\ - %\F \vee \true &\equiv \true \spc \F \wedge \false \equiv \false \tag{\structure{Dominanz}}\\ - %\F \vee \F &\equiv \F \spc \F \wedge \F \equiv \F \tag{\structure{Idempotenz}}\\ - %\neg \neg \F &\equiv \F \tag{\structure{Doppelte Negation}}\\ - %\F \vee \neg \F &\equiv \true \tag{\structure{Triviale Tautologie}}\\ - %\F \wedge \neg \F &\equiv \false \tag{\structure{Triviale Kontradiktion}}\\ - %\bigskip - %\F \vee \G &\equiv \G \vee \F \tag{\structure{Kommutativität}}\\ - %\F \wedge \G &\equiv \G \wedge \F\\ - %(\F \vee \G) \vee \K &\equiv \F \vee (\G \vee \K) \tag{\structure{Assoziativität}}\\ - %(\F \wedge \G) \wedge \K &\equiv \F \wedge (\G \wedge \K)\\ - %\F \vee (\G \wedge \K) &\equiv (\F \vee \G) \wedge (\F \vee \K) \tag{\structure{Distributivität}}\\ - %\F \wedge (\G \vee \K) &\equiv (\F \wedge \G) \vee (\F \wedge \K)\\ - %\neg(\F \wedge \G) &\equiv \neg \F \vee \neg \G \tag{\structure{De Morgan}}\\ - %\neg(\F \vee \G) &\equiv \neg\F \wedge \neg\G\\ - %\bigskip - %\F \rightarrow \G &\equiv \neg \F \vee \G \tag{\structure{Implikation}}\\ - %\F \leftrightarrow \G &\equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \tag{\structure{Bikonditional}}\\ - %\end{align} - %\end{frame} -} -} - -\defineUnit{aussagenlogiknormalformen}{% -\begin{frame}[c] - \frametitle{Literale und Klauseln} - \setbeamercovered{dynamic} - - \begin{definition}[Literal] - Ein \structure{Literal} ist eine Variable $v \in V$ oder die Negation $\neg v$ einer Variable. - \end{definition} - - \begin{definition}[Klausel] - Eine \structure{Klausel} verknüpft mehrere Literale mit einem assoziativen Operator. - \end{definition} - - \vfill - - \begin{example}[] - Seien $a, \neg b, c$ Literale. Dann sind - \begin{itemize} - \item $a \wedge \neg b \wedge c$ - \item $a \vee \neg b \vee c$ - \end{itemize} - Klauseln. - \end{example} -\end{frame} - -{ - \newcommand{\klausel}[2]{\underbracket{(##2)}_{\text{##1-Klausel}}} - \begin{frame} - \frametitle{DNF} - \setbeamercovered{dynamic} - - \begin{definition}[Disjunktive Normalform] - Eine \structure{DNF-Klausel} ist eine Konjunktion von Literalen $L_i$.\\ - Eine Formel $F$, ist in \structure{Disjunktiver Normalform}, wenn sie eine Disjunktion von DNF-Klauseln ist. - \[ F \defeq \bigvee \bigwedge_i L_i \] - \end{definition} - \begin{itemize} - \item Ausnahme: $\textrm{false}$ ist auch in DNF - \end{itemize} - - \begin{example}[] - $F$ ist in DNF. - \[ 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} \] - \end{example} - \end{frame} - - \begin{frame} - \frametitle{KNF} - \setbeamercovered{dynamic} - - \begin{definition}[Konjunktive Normalform] - Eine \structure{KNF-Klausel} ist eine Disjunktion von Literalen $L_i$.\\ - Eine Formel $F$, ist in \structure{Konjunktiver Normalform}, wenn sie eine Konjunktion von KNF-Klauseln ist. - \[ F \defeq \bigwedge \bigvee_i L_i \] - \end{definition} - \begin{itemize} - \item Ausnahme: $\textrm{true}$ ist auch in KNF - \end{itemize} - - \begin{example}[] - $F$ ist in KNF. - \[ 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} \] - \end{example} - \end{frame} -} - -\begin{frame} - \frametitle{Konstruktion der NF} - \setbeamercovered{dynamic} - - \begin{itemize} - \item \structure{Jede} nicht-triviale Formel ist in DNF und KNF umwandelbar - \item Durch Äquivalenzumformungen berechenbar (exponentiell groß!) - \item Oder: Konstruktion mit Wahrheitstabellen - \end{itemize} - - \vfill - - \begin{block}{Normalformen aus Wahrheitstabellen} - Gegeben eine Formel $F$ und ihre Wahrheitstabelle - \begin{itemize} - \item DNF - \begin{enumerate} - \item Betrachte Zeilen mit Eintrag \structure{$1$} - \item Bilde \structure{Konjunktion} aus der \structure{Belegung} - \item Bilde \structure{Disjunktion} aller erhaltenen Klauseln - \end{enumerate} - \bigskip - \item KNF - \begin{enumerate} - \item Betrachte Zeilen mit Eintrag \alert{$0$} - \item Bilde \alert{Disjunktion} aus der \alert{Negation} der Belegung - \item Bilde \alert{Konjunktion} aller erhaltenen Klauseln - \end{enumerate} - \end{itemize} - \end{block} -\end{frame} - -{ - \newcommand{\klausel}[4]{(##2 a ##1 ##3 b ##1 ##4 c)} - \begin{frame} - \frametitle{Konstruktion der NF} - \setbeamercovered{dynamic} - - \begin{example}[] - Gegeben eine Formel $F$ mit folgender Semantik - \begin{center} - \begin{tabu} to .4\textwidth {ccc|[1.2pt]c} - a & b & c & $F$ \\ \tabucline[1.2pt]{-} - 0 & 0 & 0 & 0 \\ - 0 & 0 & 1 & 0 \\ - 0 & 1 & 0 & 0 \\ - 0 & 1 & 1 & 1 \\ - 1 & 0 & 0 & 1 \\ - 1 & 0 & 1 & 1 \\ - 1 & 1 & 0 & 1 \\ - 1 & 1 & 1 & 0 - \end{tabu} - \end{center} - $F$ dargestellt in - \begin{itemize} - \item DNF $\hfill\klausel{\wedge}{\neg}{}{} \vee (a \wedge \neg b) \vee \klausel{\wedge}{}{}{\neg}\hfill$ - \medskip - \item KNF $\hfill(a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}\hfill$ - \end{itemize} - \end{example} - \end{frame} - - \begin{frame} - \frametitle{Mengendarstellung der KNF} - \setbeamercovered{dynamic} - - \begin{block}{Mengendarstellung der KNF} - Eine Formel $F = \bigwedge \bigvee L_i$ in \structure{KNF} kann in einer \structure{Mengendarstellung} repräsentiert werden. - \begin{itemize} - \item Klauseln werden durch Mengen von Literalen dargestellt - \[\left\{ a, \neg b, c \right\} \text{ steht für } (a \vee \neg b \vee c)\] - \item KNF-Formeln sind Mengen von Klauseln - \[ \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) \] - \item $\emptyset$ steht für \textrm{true}, $\left\{ \emptyset \right\}$ für \textrm{false} - \end{itemize} - \end{block} - \begin{example}[] - Gegeben $F \defeq (a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}$ in KNF. - \[ \left\{ \left\{ a, b \right\}, \left\{ \neg a, b, \neg c \right\}, \left\{ \neg a, \neg b, \neg c \right\} \right\}\] - \end{example} - \end{frame} -} -} - -\defineUnit{DPLL}{% -\begin{frame} - \frametitle{KNF aus Syntaxbaum} - \setbeamercovered{dynamic} - - \begin{block}{Idee} - Erzeuge die KNF aus dem Syntaxbaum - \begin{enumerate} - \item<1-> Weise jedem \structure{inneren Knoten} eine Variable zu - \item<1,3-> Variablen sind \structure{abhängig} von ihren Kindern - \item<1,4-> Berechne \structure{kleine} KNFs und führe diese \structure{zusammen} - \end{enumerate} - \end{block} - \begin{columns}[T] - \begin{column}{.7\textwidth} - % FIXME: onlys around A_\vee needed for "correct" fadein - \begin{align} - (x \wedge y) \vee z - \uncover<3->{\equiv &\hphantom{{}\wedge {}}\only<3->{A_\vee}\\ - &\structure{\wedge (A_\vee \leftrightarrow A_\wedge \vee z)}\\ - &\alert{\wedge (A_\wedge \leftrightarrow x \wedge y)}\\} - \uncover<4->{\equiv &\hphantom{{}\wedge {}}\only<4->{A_\vee}\\ - &\structure{\wedge (A_\vee \vee \neg A_\wedge) \wedge (A_\vee \vee \neg z)}\\ - &\qquad\structure{\wedge (\neg A_\vee \vee A_\wedge \vee z)}\\ - &\alert{\wedge (\neg A_\wedge \vee x) \wedge (\neg A_\wedge \vee y)} \\ - &\qquad\alert{\wedge(A_\wedge \vee \neg x \vee \neg y)}} - \end{align} - \end{column} - \begin{column}{.3\textwidth} - \begin{tikzpicture}[grow=down, level distance = 33] - \tikzstyle{op} = [pretty] - \tikzstyle{var} = [pretty, rectangle] - \tikzstyle{edge from parent} = [edge] - - \tikzstyle{level 1} = [sibling distance = 50] - \tikzstyle{level 2} = [sibling distance = 30] - \node at (0, 0) {}; - \node[op] at (0, -1) {\alt<1>{$\vee$}{$A_\vee$}} - child { - node[op] {\alt<1>{$\wedge$}{$A_\wedge$}} - edge from parent - child { - node[var] {$x$} - edge from parent - } - child { - node[var] {$y$} - edge from parent - } - } - child { - node[var] {$z$} - }; - \end{tikzpicture} - \end{column} - \end{columns} -\end{frame} - -\begin{frame} - \frametitle{DPLL} - \setbeamercovered{dynamic} - - \begin{definition}[DPLL-Belegung] - Sei $F$ eine Formel in KNF und $p$ eine Variable von $F$.\\ - 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. - \end{definition} - - \begin{block}{DPLL} - Gegeben eine Formel $F$ in KNF - \begin{itemize} - \item Wenn $F = \mathrm{true}$ dann antworte \enquote{erfüllbar} - \item Wenn $F = \mathrm{false}$ dann antworte \enquote{unerfüllbar} - \item Sonst - \begin{enumerate} - \item Wähle eine Variable $p$ in $F$ - \item Prüfe ob $F[p\backslash\mathrm{true}]$ oder $F[p\backslash\mathrm{false}]$ erfüllbar - \end{enumerate} - \end{itemize} - \end{block} - \begin{itemize} - \item Schlaue Wahl der Variable beschleunigt Ausführung - \item Wähle Variablen die einzeln stehen (\structure{One-Literal-Rule}) - \end{itemize} -\end{frame} -}
--- a/notes/tex/frames.tex Sat Nov 16 19:05:35 2013 +0100 +++ b/notes/tex/frames.tex Mon Nov 18 15:12:27 2013 +0100 @@ -9,3 +9,4 @@ \input{intro.tex} \input{basics.tex} +\input{logic.tex}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/notes/tex/logic.tex Mon Nov 18 15:12:27 2013 +0100 @@ -0,0 +1,514 @@ +\defineUnit{aussagenlogiksyntax}{% +\begin{frame}[c] + \frametitle{Syntax der Aussagenlogik} + \setbeamercovered{dynamic} + + \begin{definition}[Syntax der Aussagenlogik] + Aussagenlogische \structure{Formeln} bestehen aus Konstanten, Variablen und Operatoren. Die Menge \structure{$\mathcal{F}$} aller Formeln ist induktiv definiert. + \begin{itemize} + \item $\mathrm{false} = 0 \in \mathcal{F},\quad \mathrm{true} = 1 \in \mathcal{F}$\hfill(\alert{Konstanten}) + \item $V = \left\{ a, b, c,\ldots \right\} \subseteq \mathcal{F}$\hfill(\alert{Variablen})\\ + \medskip + \item Ist $A \in \mathcal{F}$ eine aussagenlogische Formel, dann auch + \begin{align} + \neg A &\in \mathcal{F}\tag{\alert{Negation}}\\ + \intertext{\item Sind $A, B \in \mathcal{F}$ aussagenlogische Formeln, dann auch} + (A \wedge B)&\in \mathcal{F}\tag{\alert{Konjunktion}}\\ + (A \vee B)&\in \mathcal{F}\tag{\alert{Disjunktion}}\\ + (A \rightarrow B)&\in \mathcal{F}\tag{\alert{Implikation}} + \end{align} + \end{itemize} + Alle Formeln lassen sich so konstruieren. + \end{definition} +\end{frame} + +\begin{frame} + \frametitle{Operatorenbindung} + \setbeamercovered{dynamic} + + \begin{definition}[Bindungsregeln] + Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist + \[ \neg \quad \wedge \quad \vee \quad \rightarrow \quad \leftrightarrow \] + Die Implikation ist \structure{rechtsassoziativ} + \[ 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) \] + \end{definition} + \begin{itemize} + \item Üblicherweise klammert man $\wedge$ und $\vee$ + \[ (a \wedge b) \vee c \text{\quad statt\quad} a \wedge b \vee c \] + \end{itemize} + \begin{example}[] + \begin{itemize} + \item $\neg a \wedge b$\quad steht für \quad$ \left( \left( \neg a \right) \wedge b \right)$ + \item $a \wedge b \rightarrow c \vee \neg d$\quad steht für \quad$((a \wedge b) \rightarrow (c \vee \left( \neg d \right)))$ + \end{itemize} + \end{example} +\end{frame} + +\begin{frame} + \frametitle{Syntaxbaum} + \setbeamercovered{dynamic} + + \begin{block}{Syntaxbaum} + \structure{Syntaxbäume} visualisieren in welcher Reihenfolge die Regeln zur induktiven Definition angewandt werden müssen, um eine Formel zu erzeugen. + \end{block} + \begin{example}[] + Sei $F \defeq a \wedge b \rightarrow c \vee \neg d$ dann ist der dazu passende Syntaxbaum + \centering + \begin{tikzpicture}[grow=down, level distance = 33] + \tikzstyle{every node} = [] + \tikzstyle{op} = [pretty] + \tikzstyle{var} = [pretty, rectangle] + \tikzstyle{edge from parent} = [edge] + + \tikzstyle{level 1} = [sibling distance = 80] + \tikzstyle{level 2} = [sibling distance = 40] + \node[op] {$\rightarrow$} + child { + node[op] {$\wedge$} + edge from parent + child { + node[var] {$a$} + edge from parent + } + child { + node[var] {$b$} + edge from parent + } + } + child { + node[op] {$\vee$} + edge from parent + child { + node[var] {$c$} + edge from parent + } + child { + node[op] {$\neg$} + edge from parent + child { + node[var] {$d$} + edge from parent + } + } + }; + \end{tikzpicture} + \end{example} +\end{frame} +} + +\defineUnit{aussagenlogiksemantik}{% +\begin{frame} + \frametitle{Belegung} + \setbeamercovered{dynamic} + + \begin{definition}[Belegung] + Eine passende \structure{Belegung} $\beta$ zu einer Formel $F$ ordnet jeder Variable in $V$ einen Wahrheitswert aus $\left\{ 0, 1 \right\}$ zu. Es ist + \[ \beta : V \to \left\{ 0, 1 \right\} \] + \end{definition} + \begin{itemize} + \item Belegungen formalisieren Einsetzen + \item Für $n$ Variablen existieren $2^n$ Belegungen + \end{itemize} + \begin{example}[] + Sei $F \defeq \neg \left( a \wedge b \right)$ mit $V = \left\{ a, b \right\}$ und + \begin{align} + \beta : \left\{ a, b \right\} &\to \left\{ 0, 1 \right\}\\ + a &\mapsto 1\\ + b &\mapsto 0 + \end{align} + Dann ist $\beta$ eine zu $F$ passende \structure{Belegung}. + \end{example} +\end{frame} + +\begin{frame} + \frametitle{Semantik der Aussagenlogik} + \setbeamercovered{dynamic} + + \begin{definition}[Semantik einer Formel] + Die \structure{Semantik} $[F]$ einer aussagenlogischen Formel $F$ ist eine Funktion, die jeder passenden Belegung $\beta$ einen Wahrheitswert zuordnet.\\ + Sei $\mathcal{B} = \left\{ \beta_0, \beta_1, \ldots \right\}$ die Menge aller Belegungen zu $F$. Dann ist + \[[F] : \mathcal{B} \to \left\{ 0, 1 \right\}\] + \end{definition} + \begin{itemize} + \item Die Semantik löst eingesetzte Formeln auf + \item Wird anhand der induktiven Syntax definiert + \item Es gibt \alert{syntaktisch verschiedene} Formeln gleicher \structure{Semantik} + \end{itemize} + \begin{example}[] + Sei $F \defeq \left( G \rightarrow H \right)$ mit $G, H$ Formeln. Dann ist + \[ [F](\beta) = \begin{cases} + 0 & \text{falls } [G](\beta) = 1 \text{ und } [H](\beta) = 0 \\ + 1 & \text{sonst} + \end{cases}\] + \end{example} +\end{frame} + +\begin{frame} + \frametitle{Wahrheitstabelle} + \setbeamercovered{dynamic} + + \begin{block}{Wahrheitstabelle} + 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. + \end{block} + \begin{example}[] + Sei $F \defeq a \vee b \rightarrow \neg c \wedge b$. Die zu $[F]$ gehörige Wahrheitstabelle ist + \begin{center} + \begin{tabu} to .5\textwidth {cccX|[1.2pt]Xccccc} + a & b & c & & & $a \vee b$ & $\rightarrow$ & $\neg c$ & $\wedge$ & $b$ \\ \tabucline[1.2pt]{-} + 0 & 0 & 0 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{0} & \\ + 0 & 0 & 1 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{0} & \onslide<2->{0} & \\ + 0 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\ + 0 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ + 1 & 0 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{1} & \onslide<2->{0} & \\ + 1 & 0 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ + 1 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\ + 1 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ + \end{tabu} + \end{center} + \end{example} +\end{frame} + +\begin{frame} + \frametitle{Äquivalente Formeln} + \setbeamercovered{dynamic} + + \begin{definition}[Äquivalente Formeln] + Man nennt zwei Formeln \structure{äquivalent}, wenn sie dieselbe Semantik besitzen.\\ + Seien $F, G$ Formeln mit Belegungen $\mathcal{B} = \mathcal{B}_F = \mathcal{B}_G$. $F$ und $G$ sind äquivalent wenn + \[ \forall \beta \in \mathcal{B}. [F](\beta) = [G](\beta) \] + Man schreibt \structure{$F \equiv G$} oder \structure{$F \leftrightarrow G$}. + \end{definition} + + \begin{example}[] + Für $F \defeq a \rightarrow b$ und $G \defeq \neg a \vee b$ gilt $F \equiv G$. + \begin{center} + \begin{tabu} to .4\textwidth {cc|[1.2pt]XcX||Xccc} + a & b & & $a \Rightarrow b$ & & & $\neg a$ & $\vee$ & $b$ \\ \tabucline[1.2pt]{-} + 0 & 0 & & \structure{1} & & & 1 & \structure{1} \\ + 0 & 1 & & \structure{1} & & & 1 & \structure{1} \\ + 1 & 0 & & \structure{0} & & & 0 & \structure{0} \\ + 1 & 1 & & \structure{1} & & & 0 & \structure{1} \\ + \end{tabu} + \end{center} + \end{example} +\end{frame} + +\begin{frame} + \frametitle{Eigenschaften von Formeln} + \setbeamercovered{dynamic} + + \begin{block}{Eigenschaften aussagenlogischer Formeln} + Sei $F$ eine aussagenlogische Formel mit Variablen $V$ und der Menge der passenden Belegungen $\mathcal{B}$. Man nennt F + \begin{description}[\quad unerfüllbar] + \item[erfüllbar] $\exists \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ kann wahr sein) + \item[unerfüllbar] $\forall \beta \in \mathcal{B}. [F](\beta) = 0$\hfill($F$ ist nie wahr) + \item[gültig] $\forall \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ ist immer wahr) + \end{description} + \end{block} + \begin{itemize} + \item Eine unerfüllbare Formel nennt man \structure{Widerspruch} + \item Eine gültige Formel nennt man \structure{Tautologie} + \end{itemize} + +\end{frame} +} + +\defineUnit{aussagenlogikaequivalenzen}{% +{ + \newcommand{\true}{1} + \newcommand{\false}{0} + \newcommand{\spc}{\hspace{3em}} + \newcommand{\F}{F} + \newcommand{\G}{G} + \newcommand{\K}{H} + + \begin{frame} + \frametitle{Äquivalenzregeln} + \setbeamercovered{dynamic} + + \begin{description}[Triviale Kontradiktion\quad] + \item[Identität] $\F \wedge \true \equiv \F \spc \F \vee \false \equiv \F$ + \item[Dominanz] $\F \vee \true \equiv \true \spc \F \wedge \false \equiv \false$ + \item[Idempotenz] $\F \vee \F \equiv \F \spc \F \wedge \F \equiv \F$ + \item[Doppelte Negation] $\neg \neg \F \equiv \F$ + \item[Triviale Tautologie] $\F \vee \neg \F \equiv \true$ + \item[Triviale Kontradiktion] $\F \wedge \neg \F \equiv \false$ + \bigskip + \item[Kommutativität] $\F \vee \G \equiv \G \vee \F$\\ + $\F \wedge \G \equiv \G \wedge \F$ + \item[Assoziativität] $(\F \vee \G) \vee \K \equiv \F \vee (\G \vee \K)$\\ + $(\F \wedge \G) \wedge \K \equiv \F \wedge (\G \wedge \K)$ + \item[Distributivität] $\F \vee (\G \wedge \K) \equiv (\F \vee \G) \wedge (\F \vee \K)$\\ + $\F \wedge (\G \vee \K) \equiv (\F \wedge \G) \vee (\F \wedge \K)$ + \item[De Morgan] $\neg(\F \wedge \G) \equiv \neg \F \vee \neg \G$\\ + $\neg(\F \vee \G) \equiv \neg\F \wedge \neg\G$ + \bigskip + \item[Implikation] $\F \rightarrow \G \equiv \neg \F \vee \G$ + \item[Bikonditional] $\F \leftrightarrow \G \equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F)$ + \end{description} + \end{frame} + + %\begin{frame} + %\frametitle{Äquivalenzregeln} + %\setbeamercovered{dynamic} + + %\vspace{-2em} + %\begin{align} + %\F \wedge \true &\equiv \F \spc \F \vee \false \equiv \F \tag{\structure{Identität}}\\ + %\F \vee \true &\equiv \true \spc \F \wedge \false \equiv \false \tag{\structure{Dominanz}}\\ + %\F \vee \F &\equiv \F \spc \F \wedge \F \equiv \F \tag{\structure{Idempotenz}}\\ + %\neg \neg \F &\equiv \F \tag{\structure{Doppelte Negation}}\\ + %\F \vee \neg \F &\equiv \true \tag{\structure{Triviale Tautologie}}\\ + %\F \wedge \neg \F &\equiv \false \tag{\structure{Triviale Kontradiktion}}\\ + %\bigskip + %\F \vee \G &\equiv \G \vee \F \tag{\structure{Kommutativität}}\\ + %\F \wedge \G &\equiv \G \wedge \F\\ + %(\F \vee \G) \vee \K &\equiv \F \vee (\G \vee \K) \tag{\structure{Assoziativität}}\\ + %(\F \wedge \G) \wedge \K &\equiv \F \wedge (\G \wedge \K)\\ + %\F \vee (\G \wedge \K) &\equiv (\F \vee \G) \wedge (\F \vee \K) \tag{\structure{Distributivität}}\\ + %\F \wedge (\G \vee \K) &\equiv (\F \wedge \G) \vee (\F \wedge \K)\\ + %\neg(\F \wedge \G) &\equiv \neg \F \vee \neg \G \tag{\structure{De Morgan}}\\ + %\neg(\F \vee \G) &\equiv \neg\F \wedge \neg\G\\ + %\bigskip + %\F \rightarrow \G &\equiv \neg \F \vee \G \tag{\structure{Implikation}}\\ + %\F \leftrightarrow \G &\equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \tag{\structure{Bikonditional}}\\ + %\end{align} + %\end{frame} +} +} + +\defineUnit{aussagenlogiknormalformen}{% +\begin{frame}[c] + \frametitle{Literale und Klauseln} + \setbeamercovered{dynamic} + + \begin{definition}[Literal] + Ein \structure{Literal} ist eine Variable $v \in V$ oder die Negation $\neg v$ einer Variable. + \end{definition} + + \begin{definition}[Klausel] + Eine \structure{Klausel} verknüpft mehrere Literale mit einem assoziativen Operator. + \end{definition} + + \vfill + + \begin{example}[] + Seien $a, \neg b, c$ Literale. Dann sind + \begin{itemize} + \item $a \wedge \neg b \wedge c$ + \item $a \vee \neg b \vee c$ + \end{itemize} + Klauseln. + \end{example} +\end{frame} + +{ + \newcommand{\klausel}[2]{\underbracket{(##2)}_{\text{##1-Klausel}}} + \begin{frame} + \frametitle{DNF} + \setbeamercovered{dynamic} + + \begin{definition}[Disjunktive Normalform] + Eine \structure{DNF-Klausel} ist eine Konjunktion von Literalen $L_i$.\\ + Eine Formel $F$, ist in \structure{Disjunktiver Normalform}, wenn sie eine Disjunktion von DNF-Klauseln ist. + \[ F \defeq \bigvee \bigwedge_i L_i \] + \end{definition} + \begin{itemize} + \item Ausnahme: $\textrm{false}$ ist auch in DNF + \end{itemize} + + \begin{example}[] + $F$ ist in DNF. + \[ 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} \] + \end{example} + \end{frame} + + \begin{frame} + \frametitle{KNF} + \setbeamercovered{dynamic} + + \begin{definition}[Konjunktive Normalform] + Eine \structure{KNF-Klausel} ist eine Disjunktion von Literalen $L_i$.\\ + Eine Formel $F$, ist in \structure{Konjunktiver Normalform}, wenn sie eine Konjunktion von KNF-Klauseln ist. + \[ F \defeq \bigwedge \bigvee_i L_i \] + \end{definition} + \begin{itemize} + \item Ausnahme: $\textrm{true}$ ist auch in KNF + \end{itemize} + + \begin{example}[] + $F$ ist in KNF. + \[ 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} \] + \end{example} + \end{frame} +} + +\begin{frame} + \frametitle{Konstruktion der NF} + \setbeamercovered{dynamic} + + \begin{itemize} + \item \structure{Jede} nicht-triviale Formel ist in DNF und KNF umwandelbar + \item Durch Äquivalenzumformungen berechenbar (exponentiell groß!) + \item Oder: Konstruktion mit Wahrheitstabellen + \end{itemize} + + \vfill + + \begin{block}{Normalformen aus Wahrheitstabellen} + Gegeben eine Formel $F$ und ihre Wahrheitstabelle + \begin{itemize} + \item DNF + \begin{enumerate} + \item Betrachte Zeilen mit Eintrag \structure{$1$} + \item Bilde \structure{Konjunktion} aus der \structure{Belegung} + \item Bilde \structure{Disjunktion} aller erhaltenen Klauseln + \end{enumerate} + \bigskip + \item KNF + \begin{enumerate} + \item Betrachte Zeilen mit Eintrag \alert{$0$} + \item Bilde \alert{Disjunktion} aus der \alert{Negation} der Belegung + \item Bilde \alert{Konjunktion} aller erhaltenen Klauseln + \end{enumerate} + \end{itemize} + \end{block} +\end{frame} + +{ + \newcommand{\klausel}[4]{(##2 a ##1 ##3 b ##1 ##4 c)} + \begin{frame} + \frametitle{Konstruktion der NF} + \setbeamercovered{dynamic} + + \begin{example}[] + Gegeben eine Formel $F$ mit folgender Semantik + \begin{center} + \begin{tabu} to .4\textwidth {ccc|[1.2pt]c} + a & b & c & $F$ \\ \tabucline[1.2pt]{-} + 0 & 0 & 0 & 0 \\ + 0 & 0 & 1 & 0 \\ + 0 & 1 & 0 & 0 \\ + 0 & 1 & 1 & 1 \\ + 1 & 0 & 0 & 1 \\ + 1 & 0 & 1 & 1 \\ + 1 & 1 & 0 & 1 \\ + 1 & 1 & 1 & 0 + \end{tabu} + \end{center} + $F$ dargestellt in + \begin{itemize} + \item DNF $\hfill\klausel{\wedge}{\neg}{}{} \vee (a \wedge \neg b) \vee \klausel{\wedge}{}{}{\neg}\hfill$ + \medskip + \item KNF $\hfill(a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}\hfill$ + \end{itemize} + \end{example} + \end{frame} + + \begin{frame} + \frametitle{Mengendarstellung der KNF} + \setbeamercovered{dynamic} + + \begin{block}{Mengendarstellung der KNF} + Eine Formel $F = \bigwedge \bigvee L_i$ in \structure{KNF} kann in einer \structure{Mengendarstellung} repräsentiert werden. + \begin{itemize} + \item Klauseln werden durch Mengen von Literalen dargestellt + \[\left\{ a, \neg b, c \right\} \text{ steht für } (a \vee \neg b \vee c)\] + \item KNF-Formeln sind Mengen von Klauseln + \[ \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) \] + \item $\emptyset$ steht für \textrm{true}, $\left\{ \emptyset \right\}$ für \textrm{false} + \end{itemize} + \end{block} + \begin{example}[] + Gegeben $F \defeq (a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}$ in KNF. + \[ \left\{ \left\{ a, b \right\}, \left\{ \neg a, b, \neg c \right\}, \left\{ \neg a, \neg b, \neg c \right\} \right\}\] + \end{example} + \end{frame} +} +} + +\defineUnit{DPLL}{% +\begin{frame} + \frametitle{KNF aus Syntaxbaum} + \setbeamercovered{dynamic} + + \begin{block}{Idee} + Erzeuge die KNF aus dem Syntaxbaum + \begin{enumerate} + \item<1-> Weise jedem \structure{inneren Knoten} eine Variable zu + \item<1,3-> Variablen sind \structure{abhängig} von ihren Kindern + \item<1,4-> Berechne \structure{kleine} KNFs und führe diese \structure{zusammen} + \end{enumerate} + \end{block} + \begin{columns}[T] + \begin{column}{.7\textwidth} + % FIXME: onlys around A_\vee needed for "correct" fadein + \begin{align} + (x \wedge y) \vee z + \uncover<3->{\equiv &\hphantom{{}\wedge {}}\only<3->{A_\vee}\\ + &\structure{\wedge (A_\vee \leftrightarrow A_\wedge \vee z)}\\ + &\alert{\wedge (A_\wedge \leftrightarrow x \wedge y)}\\} + \uncover<4->{\equiv &\hphantom{{}\wedge {}}\only<4->{A_\vee}\\ + &\structure{\wedge (A_\vee \vee \neg A_\wedge) \wedge (A_\vee \vee \neg z)}\\ + &\qquad\structure{\wedge (\neg A_\vee \vee A_\wedge \vee z)}\\ + &\alert{\wedge (\neg A_\wedge \vee x) \wedge (\neg A_\wedge \vee y)} \\ + &\qquad\alert{\wedge(A_\wedge \vee \neg x \vee \neg y)}} + \end{align} + \end{column} + \begin{column}{.3\textwidth} + \begin{tikzpicture}[grow=down, level distance = 33] + \tikzstyle{op} = [pretty] + \tikzstyle{var} = [pretty, rectangle] + \tikzstyle{edge from parent} = [edge] + + \tikzstyle{level 1} = [sibling distance = 50] + \tikzstyle{level 2} = [sibling distance = 30] + \node at (0, 0) {}; + \node[op] at (0, -1) {\alt<1>{$\vee$}{$A_\vee$}} + child { + node[op] {\alt<1>{$\wedge$}{$A_\wedge$}} + edge from parent + child { + node[var] {$x$} + edge from parent + } + child { + node[var] {$y$} + edge from parent + } + } + child { + node[var] {$z$} + }; + \end{tikzpicture} + \end{column} + \end{columns} +\end{frame} + +\begin{frame} + \frametitle{DPLL} + \setbeamercovered{dynamic} + + \begin{definition}[DPLL-Belegung] + Sei $F$ eine Formel in KNF und $p$ eine Variable von $F$.\\ + 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. + \end{definition} + + \begin{block}{DPLL} + Gegeben eine Formel $F$ in KNF + \begin{itemize} + \item Wenn $F = \mathrm{true}$ dann antworte \enquote{erfüllbar} + \item Wenn $F = \mathrm{false}$ dann antworte \enquote{unerfüllbar} + \item Sonst + \begin{enumerate} + \item Wähle eine Variable $p$ in $F$ + \item Prüfe ob $F[p\backslash\mathrm{true}]$ oder $F[p\backslash\mathrm{false}]$ erfüllbar + \end{enumerate} + \end{itemize} + \end{block} + \begin{itemize} + \item Schlaue Wahl der Variable beschleunigt Ausführung + \item Wähle Variablen die einzeln stehen (\structure{One-Literal-Rule}) + \end{itemize} +\end{frame} +}