Reverse Unit Propagation

http://www.satcompetition.org/2014/certunsat.shtml 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∧¬C $\curvearrowright$ F∧¬C ist nicht erfüllbar $\curvearrowright$ ¬F∨C ist allgemeingültig $\curvearrowright$ F $\models$ C (aus F folgt C) $\curvearrowright$ C „ist redundant``

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