chapters/optimizations.tex

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