Unit Propagation Idea: Forward checking on binary clauses (not a or B) {T,F}? T, FI Unit propagation If all literals are false, save i then assign true to l (not a( not B(A or B or C) Unit Propagation Examples C1: Not A or B Satisfied C2: Not c or a Satisfied C 3 Not B orC Satisfied C4: A Satisfied C4 CI rue B3/19/2003 copyright Brian Williams 17 Unit Propagation Idea: Forward checking on binary clauses (not A or B) {F} {T,F} ? {T} {T,F} ? Unit propagation: If all literals are false, save l then assign true to l: • (not A) (not B) (A or B or C) C 3/19/2003 copyright Brian Williams 18 Unit Propagation Examples • C1: Not A or B • C2: Not C or A • C3: Not B or C • C4: A C4 A True C1 B True C3 C True Satisfied Satisfied Satisfied Satisfied