Binary file ds13-04.pdf has changed

--- a/notes/tex/basics.tex	Tue Nov 12 00:34:37 2013 +0100
+++ b/notes/tex/basics.tex	Tue Nov 12 00:34:55 2013 +0100
@@ -791,3 +791,303 @@
 
 \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 \F$
+            \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 \F \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}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/notes/tex/ue04_notes.tex	Tue Nov 12 00:34:55 2013 +0100
@@ -0,0 +1,13 @@
+\input{preamble.tex}
+\input{frames.tex}
+
+\title{Übung 4: Aussagenlogik II}
+\subtitle{Diskrete Strukturen im Wintersemester 2013/2014}
+\author{\href{mailto:markus.kaiser@in.tum.de}{Markus Kaiser}}
+
+\begin{document}
+\showUnit{titel}
+\showUnit{aussagenlogikaequivalenzen}
+\showUnit{aussagenlogiknormalformen}
+\showUnit{DPLL}
+\end{document}

Binary file notes/ue04_notes.pdf has changed