Find Symptom Using Unit Propagation true false false true C2: pv-t CI:rvg VR procedure propagate(c) ∥ C is a clause if all literals in C are false except l, and I is unassigned then assign true to and record c as a support for l and for each clause C mentioning not I propagate(C) end propagate 10/03/03 copyright Brian Williams, 200310/03/03 copyright Brian Williams, 2003 6 r q p C2: ¬ p ›¬ t true false true t false procedure propagate ( C) // C is a clause if all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l and for each clause C’ mentioning “not l”, propagate (C’ ) end propagate C1 : ¬r › q ›p Find Symptom Using Unit Propagation