Unit Propagation Examples C1: Not Aor B Satisfied C2: Not CorASatisfied C3 Not b orc Satisfied C4:A C4 rue True True C1 A B C4: Not B Satisfied False False CI B Unit Propagation true fal C2:pV”t CI:TVaVp p 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 19 Unit Propagation Examples • C1: Not A or B • C2: Not C or A • C3: Not B or C • C4: A • C4’: Not B C4 C1 C3 C1 C2 C4’ A True B True C True A False B False C False C4 A True Satisfied Satisfied Satisfied Satisfied 3/19/2003 copyright Brian Williams 20 C1 : ¬r › q › p C2: ¬ p ›¬ t r true q false p t 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 Unit Propagation