\begin{slide}{Reverse Unit Propagation}


\begin{small}
\url{http://www.satcompetition.org/2014/certunsat.shtml}
\end{small}
\emph{RUP proofs are a sequence of clauses that are redundant 
with respect to the input formula. To check that a clause C is redundant, 
all literals C are assigned to false followed by unit propagation. 
In order to verify redundancy, unit propagation should result in a conflict.}

$\curvearrowright$ Konflikt für $F\wedge \neg C$ 
$\curvearrowright$ $F\wedge\neg C$ ist nicht erfüllbar 
$\curvearrowright$ $\neg F\vee C$ ist allgemeingültig
$\curvearrowright$ $F\models C$ (aus $F$ folgt $C$)
$\curvearrowright$ $C$ \glqq ist redundant\grqq



\begin{small}
siehe auch 
E.Goldberg, Y.Novikov. 
\emph{Verification of proofs of 
unsatisfiability for CNF formulas.} 
Design, Automation and Test in Europe. 
2003, March 3-7,pp.886-891
\url{http://eigold.tripod.com/papers/proof_verif.pdf}
\end{small}

\end{slide}
