chapters/optimizations.tex

   1 \section{Optimizing}
   2 \subsection*{Dummy}
   3
   4 \begin{frame}{Semnatic Branching}
   5   \begin{itemize}
   6   \item Idea: Add aditional information when considering second
   7     alternative of an or: ${\phi \vee \psi}$ becomes ${\phi \vee
   8       (¬\phi \wedge \psi)}$
   9   \item Do not reexplore branches already known to be unsat already
  10   \end{itemize}
  11 \end{frame}
  12
  13 \begin{frame}{Non-atomic Negations}
  14   TODO: ?
  15   \begin{itemize}
  16   \item Consider $\heartsuit\heartsuit\heartsuit{}p \wedge \overline{\heartsuit}\overline{\heartsuit}\overline{\heartsuit}¬p$
  17   \item Same as $\heartsuit\heartsuit\heartsuit{}p \wedge
  18     ¬\heartsuit\heartsuit\heartsuit{}p$ and thus obviously unsatisfiable
  19   \item Cool normalizes formulas to make best use of Global Caching
  20   \end{itemize}
  21 \end{frame}
  22
  23 \begin{frame}{Subset Nodes}
  24   \begin{itemize}
  25   \item Lemma: If some Node is already satisfiable, all Nodes with
  26     subsets of formulas, deferrals are also satisfiable
  27   \item Too expensive to check in general\pause
  28   \item Might be interesting for Nodes with full focus and its
  29     siblings with the same set of formulas
  30   \item Cheap but does this happen often?
  31   \end{itemize}
  32 \end{frame}
  33
  34 \begin{frame}{Normalization}
  35   TODO: ?
  36   \begin{itemize}
  37   \item Global Caching better with more same formulas
  38   \item Preprocessing in Cool currently does not consider
  39     (propositional) Comutativity, Associativity or Distributivity laws
  40   \end{itemize}
  41 \end{frame}
  42
  43
  44 \begin{frame}{Removing Edges}
  45   \begin{block}{Propagation}
  46     \begin{itemize}
  47     \item Runs in $O(edge\cdot nodes)$
  48     \item Needs to consider all satisfiable nodes
  49     \item Iterates over all edges
  50     \end{itemize}
  51   \end{block}\pause
  52   \begin{itemize}
  53   \item Idea: Remove unneeded edges
  54   \item Cores are $\exists$-quantified -- all unsatisfiable children
  55     may be removed
  56   \item States are essentially $\forall$-quantified -- all satisfiable
  57     children may be removed
  58   \end{itemize}
  59 \end{frame}
  60
  61
  62 %%% Local Variables:
  63 %%% mode: latex
  64 %%% TeX-master: "../vortrag"
  65 %%% TeX-engine: luatex
  66 %%% TeX-PDF-mode: t
  67 %%% End: