\section{Optimizing}
\subsection*{Dummy}
-\begin{frame}{Semnatic Branching}
+\begin{frame}{Semantic 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
+ \item Idea: Add additional information when considering second
+ alternative of a disjunction: ${\phi \vee \psi}$ becomes ${\phi
+ \vee (¬\phi \wedge \psi)}$
+ \item Do not re-explore branches already known to be unsatisfiable 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
\end{itemize}
\end{frame}
-
\begin{frame}{Removing Edges}
\begin{block}{Propagation}
\begin{itemize}
- \item Runs in $O(edge\cdot nodes)$
+ \item Runs in $\mathcal{O}(\mathit{|edge|}\cdot\mathit{|nodes|})$
\item Needs to consider all satisfiable nodes
\item Iterates over all edges
\end{itemize}