Mercurial > 13ws.ds

comparison notes/tex/basics.tex @ 17:099613ee2f37

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fourth slides and sheet
author Markus Kaiser <markus.kaiser@in.tum.de>
date Tue, 12 Nov 2013 00:34:55 +0100
parents b83150706135
children 8408cf61d46b
comparison
equal deleted inserted replaced
16:b83150706135 17:099613ee2f37
789 \item Eine gültige Formel nennt man \structure{Tautologie} 789 \item Eine gültige Formel nennt man \structure{Tautologie}
790 \end{itemize} 790 \end{itemize}
791 791
792 \end{frame} 792 \end{frame}
793 } 793 }
794
795 \defineUnit{aussagenlogikaequivalenzen}{%
796 {
797 \newcommand{\true}{1}
798 \newcommand{\false}{0}
799 \newcommand{\spc}{\hspace{3em}}
800 \newcommand{\F}{F}
801 \newcommand{\G}{G}
802 \newcommand{\K}{H}
803
804 \begin{frame}
805 \frametitle{Äquivalenzregeln}
806 \setbeamercovered{dynamic}
807
808 \begin{description}[Triviale Kontradiktion\quad]
809 \item[Identität] $\F \wedge \true \equiv \F \spc \F \vee \false \equiv \F$
810 \item[Dominanz] $\F \vee \true \equiv \true \spc \F \wedge \false \equiv \F$
811 \item[Idempotenz] $\F \vee \F \equiv \F \spc \F \wedge \F \equiv \F$
812 \item[Doppelte Negation] $\neg \neg \F \equiv \F$
813 \item[Triviale Tautologie] $\F \vee \neg \F \equiv \true$
814 \item[Triviale Kontradiktion] $\F \wedge \neg \F \equiv \false$
815 \bigskip
816 \item[Kommutativität] $\F \vee \G \equiv \G \vee \F$\\
817 $\F \wedge \G \equiv \G \wedge \F$
818 \item[Assoziativität] $(\F \vee \G) \vee \K \equiv \F \vee (\G \vee \K)$\\
819 $(\F \wedge \G) \wedge \K \equiv \F \wedge (\G \wedge \K)$
820 \item[Distributivität] $\F \vee (\G \wedge \K) \equiv (\F \vee \G) \wedge (\F \vee \K)$\\
821 $\F \wedge (\G \vee \K) \equiv (\F \wedge \G) \vee (\F \wedge \K)$
822 \item[De Morgan] $\neg(\F \wedge \G) \equiv \neg \F \vee \neg \G$\\
823 $\neg(\F \vee \G) \equiv \neg\F \wedge \neg\G$
824 \bigskip
825 \item[Implikation] $\F \rightarrow \G \equiv \neg \F \vee \G$
826 \item[Bikonditional] $\F \leftrightarrow \G \equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F)$
827 \end{description}
828 \end{frame}
829
830 %\begin{frame}
831 %\frametitle{Äquivalenzregeln}
832 %\setbeamercovered{dynamic}
833
834 %\vspace{-2em}
835 %\begin{align}
836 %\F \wedge \true &\equiv \F \spc \F \vee \false \equiv \F \tag{\structure{Identität}}\\
837 %\F \vee \true &\equiv \true \spc \F \wedge \false \equiv \F \tag{\structure{Dominanz}}\\
838 %\F \vee \F &\equiv \F \spc \F \wedge \F \equiv \F \tag{\structure{Idempotenz}}\\
839 %\neg \neg \F &\equiv \F \tag{\structure{Doppelte Negation}}\\
840 %\F \vee \neg \F &\equiv \true \tag{\structure{Triviale Tautologie}}\\
841 %\F \wedge \neg \F &\equiv \false \tag{\structure{Triviale Kontradiktion}}\\
842 %\bigskip
843 %\F \vee \G &\equiv \G \vee \F \tag{\structure{Kommutativität}}\\
844 %\F \wedge \G &\equiv \G \wedge \F\\
845 %(\F \vee \G) \vee \K &\equiv \F \vee (\G \vee \K) \tag{\structure{Assoziativität}}\\
846 %(\F \wedge \G) \wedge \K &\equiv \F \wedge (\G \wedge \K)\\
847 %\F \vee (\G \wedge \K) &\equiv (\F \vee \G) \wedge (\F \vee \K) \tag{\structure{Distributivität}}\\
848 %\F \wedge (\G \vee \K) &\equiv (\F \wedge \G) \vee (\F \wedge \K)\\
849 %\neg(\F \wedge \G) &\equiv \neg \F \vee \neg \G \tag{\structure{De Morgan}}\\
850 %\neg(\F \vee \G) &\equiv \neg\F \wedge \neg\G\\
851 %\bigskip
852 %\F \rightarrow \G &\equiv \neg \F \vee \G \tag{\structure{Implikation}}\\
853 %\F \leftrightarrow \G &\equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \tag{\structure{Bikonditional}}\\
854 %\end{align}
855 %\end{frame}
856 }
857 }
858
859 \defineUnit{aussagenlogiknormalformen}{%
860 \begin{frame}[c]
861 \frametitle{Literale und Klauseln}
862 \setbeamercovered{dynamic}
863
864 \begin{definition}[Literal]
865 Ein \structure{Literal} ist eine Variable $v \in V$ oder die Negation $\neg v$ einer Variable.
866 \end{definition}
867
868 \begin{definition}[Klausel]
869 Eine \structure{Klausel} verknüpft mehrere Literale mit einem assoziativen Operator.
870 \end{definition}
871
872 \vfill
873
874 \begin{example}[]
875 Seien $a, \neg b, c$ Literale. Dann sind
876 \begin{itemize}
877 \item $a \wedge \neg b \wedge c$
878 \item $a \vee \neg b \vee c$
879 \end{itemize}
880 Klauseln.
881 \end{example}
882 \end{frame}
883
884 {
885 \newcommand{\klausel}[2]{\underbracket{(##2)}_{\text{##1-Klausel}}}
886 \begin{frame}
887 \frametitle{DNF}
888 \setbeamercovered{dynamic}
889
890 \begin{definition}[Disjunktive Normalform]
891 Eine \structure{DNF-Klausel} ist eine Konjunktion von Literalen $L_i$.\\
892 Eine Formel $F$, ist in \structure{Disjunktiver Normalform}, wenn sie eine Disjunktion von DNF-Klauseln ist.
893 \[ F \defeq \bigvee \bigwedge_i L_i \]
894 \end{definition}
895 \begin{itemize}
896 \item Ausnahme: $\textrm{false}$ ist auch in DNF
897 \end{itemize}
898
899 \begin{example}[]
900 $F$ ist in DNF.
901 \[ 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} \]
902 \end{example}
903 \end{frame}
904
905 \begin{frame}
906 \frametitle{KNF}
907 \setbeamercovered{dynamic}
908
909 \begin{definition}[Konjunktive Normalform]
910 Eine \structure{KNF-Klausel} ist eine Disjunktion von Literalen $L_i$.\\
911 Eine Formel $F$, ist in \structure{Konjunktiver Normalform}, wenn sie eine Konjunktion von KNF-Klauseln ist.
912 \[ F \defeq \bigwedge \bigvee_i L_i \]
913 \end{definition}
914 \begin{itemize}
915 \item Ausnahme: $\textrm{true}$ ist auch in KNF
916 \end{itemize}
917
918 \begin{example}[]
919 $F$ ist in KNF.
920 \[ 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} \]
921 \end{example}
922 \end{frame}
923 }
924
925 \begin{frame}
926 \frametitle{Konstruktion der NF}
927 \setbeamercovered{dynamic}
928
929 \begin{itemize}
930 \item \structure{Jede} nicht-triviale Formel ist in DNF und KNF umwandelbar
931 \item Durch Äquivalenzumformungen berechenbar (exponentiell groß!)
932 \item Oder: Konstruktion mit Wahrheitstabellen
933 \end{itemize}
934
935 \vfill
936
937 \begin{block}{Normalformen aus Wahrheitstabellen}
938 Gegeben eine Formel $F$ und ihre Wahrheitstabelle
939 \begin{itemize}
940 \item DNF
941 \begin{enumerate}
942 \item Betrachte Zeilen mit Eintrag \structure{$1$}
943 \item Bilde \structure{Konjunktion} aus der \structure{Belegung}
944 \item Bilde \structure{Disjunktion} aller erhaltenen Klauseln
945 \end{enumerate}
946 \bigskip
947 \item KNF
948 \begin{enumerate}
949 \item Betrachte Zeilen mit Eintrag \alert{$0$}
950 \item Bilde \alert{Disjunktion} aus der \alert{Negation} der Belegung
951 \item Bilde \alert{Konjunktion} aller erhaltenen Klauseln
952 \end{enumerate}
953 \end{itemize}
954 \end{block}
955 \end{frame}
956
957 {
958 \newcommand{\klausel}[4]{(##2 a ##1 ##3 b ##1 ##4 c)}
959 \begin{frame}
960 \frametitle{Konstruktion der NF}
961 \setbeamercovered{dynamic}
962
963 \begin{example}[]
964 Gegeben eine Formel $F$ mit folgender Semantik
965 \begin{center}
966 \begin{tabu} to .4\textwidth {ccc|[1.2pt]c}
967 a & b & c & $F$ \\ \tabucline[1.2pt]{-}
968 0 & 0 & 0 & 0 \\
969 0 & 0 & 1 & 0 \\
970 0 & 1 & 0 & 0 \\
971 0 & 1 & 1 & 1 \\
972 1 & 0 & 0 & 1 \\
973 1 & 0 & 1 & 1 \\
974 1 & 1 & 0 & 1 \\
975 1 & 1 & 1 & 0
976 \end{tabu}
977 \end{center}
978 $F$ dargestellt in
979 \begin{itemize}
980 \item DNF $\hfill\klausel{\wedge}{\neg}{}{} \vee (a \wedge \neg b) \vee \klausel{\wedge}{}{}{\neg}\hfill$
981 \medskip
982 \item KNF $\hfill(a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}\hfill$
983 \end{itemize}
984 \end{example}
985 \end{frame}
986
987 \begin{frame}
988 \frametitle{Mengendarstellung der KNF}
989 \setbeamercovered{dynamic}
990
991 \begin{block}{Mengendarstellung der KNF}
992 Eine Formel $F = \bigwedge \bigvee L_i$ in \structure{KNF} kann in einer \structure{Mengendarstellung} repräsentiert werden.
993 \begin{itemize}
994 \item Klauseln werden durch Mengen von Literalen dargestellt
995 \[\left\{ a, \neg b, c \right\} \text{ steht für } (a \vee \neg b \vee c)\]
996 \item KNF-Formeln sind Mengen von Klauseln
997 \[ \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) \]
998 \item $\emptyset$ steht für \textrm{true}, $\left\{ \emptyset \right\}$ für \textrm{false}
999 \end{itemize}
1000 \end{block}
1001 \begin{example}[]
1002 Gegeben $F \defeq (a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}$ in KNF.
1003 \[ \left\{ \left\{ a, b \right\}, \left\{ \neg a, b, \neg c \right\}, \left\{ \neg a, \neg b, \neg c \right\} \right\}\]
1004 \end{example}
1005 \end{frame}
1006 }
1007 }
1008
1009 \defineUnit{DPLL}{%
1010 \begin{frame}
1011 \frametitle{KNF aus Syntaxbaum}
1012 \setbeamercovered{dynamic}
1013
1014 \begin{block}{Idee}
1015 Erzeuge die KNF aus dem Syntaxbaum
1016 \begin{enumerate}
1017 \item<1-> Weise jedem \structure{inneren Knoten} eine Variable zu
1018 \item<1,3-> Variablen sind \structure{abhängig} von ihren Kindern
1019 \item<1,4-> Berechne \structure{kleine} KNFs und führe diese \structure{zusammen}
1020 \end{enumerate}
1021 \end{block}
1022 \begin{columns}[T]
1023 \begin{column}{.7\textwidth}
1024 % FIXME: onlys around A_\vee needed for "correct" fadein
1025 \begin{align}
1026 (x \wedge y) \vee z
1027 \uncover<3->{\equiv &\hphantom{{}\wedge {}}\only<3->{A_\vee}\\
1028 &\structure{\wedge (A_\vee \leftrightarrow A_\wedge \vee z)}\\
1029 &\alert{\wedge (A_\wedge \leftrightarrow x \wedge y)}\\}
1030 \uncover<4->{\equiv &\hphantom{{}\wedge {}}\only<4->{A_\vee}\\
1031 &\structure{\wedge (A_\vee \vee \neg A_\wedge) \wedge (A_\vee \vee \neg z)}\\
1032 &\qquad\structure{\wedge (\neg A_\vee \vee A_\wedge \vee z)}\\
1033 &\alert{\wedge (\neg A_\wedge \vee x) \wedge (\neg A_\wedge \vee y)} \\
1034 &\qquad\alert{\wedge(A_\wedge \vee \neg x \vee \neg y)}}
1035 \end{align}
1036 \end{column}
1037 \begin{column}{.3\textwidth}
1038 \begin{tikzpicture}[grow=down, level distance = 33]
1039 \tikzstyle{op} = [pretty]
1040 \tikzstyle{var} = [pretty, rectangle]
1041 \tikzstyle{edge from parent} = [edge]
1042
1043 \tikzstyle{level 1} = [sibling distance = 50]
1044 \tikzstyle{level 2} = [sibling distance = 30]
1045 \node at (0, 0) {};
1046 \node[op] at (0, -1) {\alt<1>{$\vee$}{$A_\vee$}}
1047 child {
1048 node[op] {\alt<1>{$\wedge$}{$A_\wedge$}}
1049 edge from parent
1050 child {
1051 node[var] {$x$}
1052 edge from parent
1053 }
1054 child {
1055 node[var] {$y$}
1056 edge from parent
1057 }
1058 }
1059 child {
1060 node[var] {$z$}
1061 };
1062 \end{tikzpicture}
1063 \end{column}
1064 \end{columns}
1065 \end{frame}
1066
1067 \begin{frame}
1068 \frametitle{DPLL}
1069 \setbeamercovered{dynamic}
1070
1071 \begin{definition}[DPLL-Belegung]
1072 Sei $F$ eine Formel in KNF und $p$ eine Variable von $F$.\\
1073 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.
1074 \end{definition}
1075
1076 \begin{block}{DPLL}
1077 Gegeben eine Formel $F$ in KNF
1078 \begin{itemize}
1079 \item Wenn $F = \mathrm{true}$ dann antworte \enquote{erfüllbar}
1080 \item Wenn $F = \mathrm{false}$ dann antworte \enquote{unerfüllbar}
1081 \item Sonst
1082 \begin{enumerate}
1083 \item Wähle eine Variable $p$ in $F$
1084 \item Prüfe ob $F[p\backslash\mathrm{true}]$ oder $F[p\backslash\mathrm{false}]$ erfüllbar
1085 \end{enumerate}
1086 \end{itemize}
1087 \end{block}
1088 \begin{itemize}
1089 \item Schlaue Wahl der Variable beschleunigt Ausführung
1090 \item Wähle Variablen die einzeln stehen (\structure{One-Literal-Rule})
1091 \end{itemize}
1092 \end{frame}
1093 }