Find Symptom Using Unit Propagation O1=G A= A true true 01=GA= (F=1)-(F=0 true 01=G)-(A=1)VX=1+X=1 true true F=1 F=1 M=→Al=Gy(X=y(x)VF 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/03/03 copyright Brian Williams, 2003 11 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 true F=1 F=1 true
Extract Conflict by Tracing Support Ol=G ￥tre true 01=GA= (F=1)-(F=0 true 01=G)-(A=1)VX=1+X=1 true true F=1 F=1 Al=G A/=G→+1(A1-0)X=1)Y=1)VF=1Fr true true (02=G)-(B=1)yY=1+y=1 true true 02=GB= 0=0)B 10/03/03 copyright Brian Williams, 2003 12
10/03/03 copyright Brian Williams, 2003 12 Extract Conflict by Tracing Support (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 true F=1 F=1 true
Extract Conflict by Tracing Support procedure Confli ict(C) /C is an inconsistent clause for each literal l in C union Support-Conflict (, support() end Conflict procedure Support-Conflict(, s) If unit-clause? (C) If mode-assignment? (teral (C) Then literal(C)1 Else Else for each literal 1 in C, other than l Union Support-Conflict(1, support (1)) end Support-Conflict 10/03/03 copyright Brian Williams, 2003 13
10/03/03 copyright Brian Williams, 2003 13 procedure Conflict ( C) // C is an inconsistent clause for each literal I in C union Support-Conflict(l, support(l) ) end Conflict procedure Support-Conflict(l,S) If unit-clause?(C) If mode-assignment?(literal (C)) Then { literal(C) } Else { } Else for each literal I1 in C, other than l Union Support-Conflict(l1, support(l1)) end Support-Conflict Extract Conflict by Tracing Support
Candidate Test with Conflict Extraction procedure Test Candidate(C, M,obs) 1. Assert candidate assignment c 2. Propagate obs through model m using unit propagation 3. If inconsistent clause return Conflict(c) 4. Else search for satisfying solution using DPLL fE inconsistent return c as a conflict se return consistent 10/03/03 copyright Brian Williams, 2003
10/03/03 copyright Brian Williams, 2003 14 Candidate Test with Conflict Extraction procedure Test_Candidate(c,M,obs) 1. Assert candidate assignment c 2. Propagate obs through model M using unit propagation. 3. If inconsistent clause return Conflict(c) 4. Else search for satisfying solution using DPLL • If inconsistent return c as a conflict. • Else return “consistent
Out line Diagnosis as Learning from Symptoms and Conflicts Conflict learning Single-fault diagnosis Multiple-fault diagnosis 10/03/03 copyright Brian Williams, 2003 15
10/03/03 copyright Brian Williams, 2003 15 Outline Diagnosis as Learning from Symptoms and Conflicts Conflict learning Single-fault diagnosis Multiple-fault diagnosis