Unit Propagation true false pvt procedure propagate (c) C is a clause B if all literals in C are false except 1, and I is unassigned then assign true to / and record C as a support for I and for each clause C' mentioning“notP”, propagate(c) end propagate Unit Propagation true fal true C2: pv-t CI: r va vp procedure propagate( c) ∥ C is a clause if all literals in C are false except I, and I is unassigned then assign true to l and record c as a support for I and or each clause C' mentioning"not I propagate(c) end propagate3/19/2003 copyright Brian Williams 21 C1 : ¬r › q › p C2: ¬ p ¬ t r true q false p t 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 Unit Propagation 3/19/2003 copyright Brian Williams 22 C1 : ¬r › q › p r q p C2: ¬ p ¬ t true false true t 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’ “not l”, propagate(C’) end propagate Unit Propagation procedure procedure mentioning › // › //