--- /dev/null
+\section{Optimizing}
+\subsection*{Dummy}
+
+\begin{frame}{Semnatic Branching}
+ \begin{itemize}
+ \item Idea: Add aditional information when considering second
+ alternative of an or: ${\phi \vee \psi}$ becomes ${\phi \vee
+ (¬\phi \wedge \psi)}$
+ \item Do not reexplore branches already known to be unsat already
+ \end{itemize}
+\end{frame}
+
+\begin{frame}{Non-atomic Negations}
+ TODO: ?
+ \begin{itemize}
+ \item Consider $\heartsuit\heartsuit\heartsuit{}p \wedge \overline{\heartsuit}\overline{\heartsuit}\overline{\heartsuit}¬p$
+ \item Same as $\heartsuit\heartsuit\heartsuit{}p \wedge
+ ¬\heartsuit\heartsuit\heartsuit{}p$ and thus obviously unsatisfiable
+ \item Cool normalizes formulas to make best use of Global Caching
+ \end{itemize}
+\end{frame}
+
+\begin{frame}{Subset Nodes}
+ \begin{itemize}
+ \item Lemma: If some Node is already satisfiable, all Nodes with
+ subsets of formulas, deferrals are also satisfiable
+ \item Too expensive to check in general\pause
+ \item Might be interesting for Nodes with full focus and its
+ siblings with the same set of formulas
+ \item Cheap but does this happen often?
+ \end{itemize}
+\end{frame}
+
+\begin{frame}{Normalization}
+ TODO: ?
+ \begin{itemize}
+ \item Global Caching better with more same formulas
+ \item Preprocessing in Cool currently does not consider
+ (propositional) Comutativity, Associativity or Distributivity laws
+ \end{itemize}
+\end{frame}
+
+
+\begin{frame}{Removing Edges}
+ \begin{block}{Propagation}
+ \begin{itemize}
+ \item Runs in $O(edge\cdot nodes)$
+ \item Needs to consider all satisfiable nodes
+ \item Iterates over all edges
+ \end{itemize}
+ \end{block}\pause
+ \begin{itemize}
+ \item Idea: Remove unneeded edges
+ \item Cores are $\exists$-quantified -- all unsatisfiable children
+ may be removed
+ \item States are essentially $\forall$-quantified -- all satisfiable
+ children may be removed
+ \end{itemize}
+\end{frame}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../vortrag"
+%%% TeX-engine: luatex
+%%% TeX-PDF-mode: t
+%%% End: