\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: 
