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, 2003
10/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
Find Symptom Using Unit Propagation 0=C A=1 (F=1)y-(F=0) (O1=G)v-(A=1)vX-1+X=1 F=1 F A=G→+A1=0X-1)Y-Y=1)VF=1 (02=G)-(B=1)Y=1+y=1 02=G B=1 10/03/03 copyright Brian Williams, 2003 7
10/03/03 copyright Brian Williams, 2003 7 Find Symptom Using Unit Propagation (O1=G) (A=1) X=1 (A1=G) (X=1) (Y=1) F=1 (O2=G) (B=1) Y=1 O1=G (F=1) (F=0) O2=G B=1 A=1 X=1 Y=1 A1=G F=1 F=1
Find Symptom Using Unit Propagation A=1 true 0=C A=1 (F=1)y-(F=0) (O1=G)v-(A=1)vX-1+X=1 true F=1 F=1 AIG+(Al=G)V(X-1)V=(Y=I)VF=1 F=l (02=G)-(B=1)Y=1+y=1 true 02=G B=1 10/03/03 copyright Brian Williams, 2003
10/03/03 copyright Brian Williams, 2003 8 Find Symptom Using Unit Propagation (O1=G) (A=1) X=1 (A1=G) (X=1) (Y=1) F=1 (O2=G) (B=1) Y=1 (F=1) (F=0) B=1 O1=G B=1 true O2=G A=1 A=1 true X=1 Y=1 A1=G F=1 F=1 F=1 true
Find Symptom Using Unit Propagation O1=G A= A true true 01=GA= (F=1)y-(F=0) 01=G-(A=1)VX=1+X= true F=1 F=1 Al=G M=→Al=Gy(Xy-(x)PF true (02=G)-(B=1)Y=1+y=1 true true 02=GB= 02=G 10/03/03 copyright Brian Williams, 2003
10/03/03 copyright Brian Williams, 2003 9 Find Symptom Using Unit Propagation (O1=G) (A=1) X=1 (A1=G) (X=1) (Y=1) F=1 (O2=G) (B=1) Y=1 (F=1) (F=0) O1=G B=1 O1=G true B=1 true O2=G O2=G true A=1 A=1 true X=1 Y=1 A1=G A1=G true F=1 F=1 F=1 true
Find Symptom Using Unit Propagation O1=G A= A true true 01=GA= (F=1)y-(F=0) true 01=G)-(A=1)VX=1+X=1 true F=1 F=1 M=→Al=Gy(X=y(x)VPF true true (02=G)V-(B=1)Y=1+y=1 true true 02=GB= O2=G 10/03/03 copyright Brian Williams, 2003 10
10/03/03 copyright Brian Williams, 2003 10 Find Symptom Using Unit Propagation (O1=G) (A=1) X=1 (A1=G) (X=1) (Y=1) F=1 (O2=G) (B=1) Y=1 (F=1) (F=0) O1=G B=1 O1=G true B=1 true O2=G O2=G true A=1 A=1 true X=1 true Y=1 true A1=G A1=G true F=1 F=1 F=1 true