X-Git-Url: https://git.siccegge.de//index.cgi?p=talk%2Fcoalgebraic-mu-calculus-cool-2.git;a=blobdiff_plain;f=chapters%2Foptimizations.tex;fp=chapters%2Foptimizations.tex;h=987763482a557232ee5fb10759b70b5793fca000;hp=0000000000000000000000000000000000000000;hb=edc63ce858f06a6b08536f876c7328820edd92a8;hpb=1d48022e102d8178ceed440a34825e110c46f4e0

diff --git a/chapters/optimizations.tex b/chapters/optimizations.tex
new file mode 100644
index 0000000..9877634
--- /dev/null
+++ b/chapters/optimizations.tex
@@ -0,0 +1,67 @@
+\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: