10/03/03 copyright Brian Williams, 2003 1 Courtesy of NASA/JPL-Caltech. http://www.jpl.nasa.gov. Conflict-directed Diagnosis Brian C. Williams 16.410-13 November 5 th 2003 Brian C. Williams, copyright 2000 10/03/03 copyright Brian Williams, 2003 2 sense P(s) WORLD observations actions AGENT Diagnostic Agent: ? Monitors & Diagnoses ? Repairs & Avoids ? Probes and Tests Plant act Symptom-directed 10/03/03 copyright Brian Williams, 2003 3 Consistency-based Diagnosis And(i): ? G(i): Out(i) = In1(i) AND In2(i) ? U(i): ? Obs: Assignment to O ? Candidate C i : Assignment of modes to X ? Diagnosis D i : A candidate such that D i ? Obs ? C(X,Y) is satisfiable. 1 1 1 1 0 Or1 Or3 And1 A B C D E F G X Y Z 0 1 Diagnosis = {A1=G, A2=U O1=G, O2=U, O3=G} ALL components have “unknown Mode” U, Whose assignment is never mentioned in C 10/03/03 copyright Brian Williams, 2003 4 Outline ? Diagnosis as Learning from symptoms and Conflicts ? Conflict learning ? Single-fault diagnosis ? Multiple-fault diagnosis 10/03/03 copyright Brian Williams, 2003 5 Or1 Or2 And1 A B C D E 1 1 1 1 F G X Y Z Symptom: F is observed 0, but should be 1 if O1, O2 and A1 are okay. Conflict: {A1=G, O1=G, O2=G} is inconsistent 0 1 1 1 :At least A1=U, O1=U, or O2=U Learning Conflicts From Symptoms 0 Or3 And3 10/03/03 copyright Brian Williams, 2003 6 r q p C 2 : ? 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 C 1 : ?r ? q ?p Find Symptom Using Unit Propagation 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 ?(F=1) ??(F=0) O1=G B=1O2=G A=1 X=1 Y=1 A1=G F=1 F=1 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 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 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 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 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 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 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” 10/03/03 copyright Brian Williams, 2003 15 Outline ? Diagnosis as Learning from Symptoms and Conflicts ? Conflict learning ? Single-fault diagnosis ? Multiple-fault diagnosis 10/03/03 copyright Brian Williams, 2003 16 Single Fault Diagnosis w Conflicts: Generate Candidates From Symptom Single_Fault_w_Conflicts(M, X, Obs) \\ Model M, Mode variables X, Observation Obs 1. Assume all components okay, All_Good = { x=G | x ? X} 2. Conflict m Test_Candidate(All_Good, M, Obs) 3. If Conflict = “consistent” return All_Good 4. Generate single fault candidates Cands m {{x=U}?Z=G | x=G ? Conflict, Z=X-{x}} 5. Test_Candidates(Cands, M, Obs) 10/03/03 copyright Brian Williams, 2003 17 Symptom: F is observed 0, but should be 1 Conflict: {O1=G, O3=G, A1=G, A2=G} is inconsistent Candidates: {O1=U, O3=U, A1=U, A2=G} Generate Candidates From Symptom Symptom 1 0 Or1 Or2 Or3 And1 And2 A B C D E F G X Y Z 1 1 1 1 0 0 1 1 0 10/03/03 copyright Brian Williams, 2003 18 Single Fault Diagnosis w Conflicts: Test Candidates Collecting Conflicts Single_Fault_Test_Candidates(C,M, Obs) \\ Candidates C, Model M, Observation Obs Solutions m {}, Conflicts m {} For each c in C If c is a superset of some conflict in Conflicts Then inconsistent candidate, ignore. Else Conflict = Test_Candidate(c, M, Obs) If Conflict = “consistent” Then add c to Solutions Else add Conflict to Conflicts return Solutions 10/03/03 copyright Brian Williams, 2003 19 Test Candidates Collecting Conflicts Or1 1 1 1 1 0 Or2 Or3 And1 And2 A B C D E F G X Y Z 0 1 1 1 ? First candidate {O1=U, …} Candidates: {{O1=U…}, {O3=U…}, {A1=U…}, {A3=U…}} Solutions: {} 10/03/03 copyright Brian Williams, 2003 20 1 1 1 1 0 Or2 Or3 And1 And2 A B C D E F G X Y Z 0 1 ? First candidate {O1=U, …} ? Suspend O1’s constraints Test Candidates Collecting Conflicts Candidates: {{O1=U…}, {O3=U…}, {A1=U…}, {A3=U…}} Solutions: {} 10/03/03 copyright Brian Williams, 2003 21 1 1 1 1 0 Or2 Or3 And1 And2 A B C D E F G X Y Z 0 1 1 1 1 ? First candidate {O1=U, …} ? Suspend O1’s constraints ? Test consistency Test Candidates Collecting Conflicts Candidates: {{O1=U…}, {O3=U…}, {A1=U…}, {A3=U…}} Solutions: {} 10/03/03 copyright Brian Williams, 2003 22 1 1 1 1 0 Or2 Or3 And1 And2 A B C D E F G X Y Z 0 1 1 1 1 ? First candidate {O1=U, …} ? Suspend O1’s constraints ? Test consistency : Consistent: Add to solutions Test Candidates Collecting Conflicts Candidates: {{O3=U…}, {A1=U…}, {A3=U…}} Solutions: {{O1=U…}} 10/03/03 copyright Brian Williams, 2003 23 1 1 1 1 0 Or1 Or2 Or3 And2 A B C D E F G X Y Z 0 1 Test Candidates Collecting Conflicts ? Second candidate {O3=U, …} ? Suspend O3’s constraints ? Test consistency And1 Candidates: {{O3=U…}, {A1=U…}, {A2=U…}} Solutions: {{O1=U…}} 10/03/03 copyright Brian Williams, 2003 24 1 1 1 1 0 Or1 And1 And2 A B C D E F G X Y Z 0 1 1 1 Test Candidates Collecting Conflicts ? Second candidate {O3=U, …} ? Suspend O3’s constraints ? Test consistency: Inconsistent 11 Testing Consistency ? Forward Prediction Candidates: {{O3=U…}, {A1=U…}, {A2=U…}} Solutions: {{O1=U…}} Or2 10/03/03 copyright Brian Williams, 2003 25 1 1 1 1 0 Or1 And1 And2 A B C D E F G X Y Z 0 1 1 1 Test Candidates Collecting Conflicts ? Second candidate {O3=U, …} ? Suspend O3’s constraints ?Test : Inconsistent 11 ? Extract Conflict: {O1=G, O2=G, A1=G} ? Use to prune candidates Candidates: {{O3=U…}, {A1=U…}, {A2=U…}} Solutions: {{O1=U…}} Conflicts: {{O1=G, O2=G, A1=G}} Or2 10/03/03 copyright Brian Williams, 2003 26 1 1 1 1 0 Or1 Or3 And1 And2 A B C D E F G X Y Z 0 1 1 1 Test Candidates Collecting Conflicts ? Third candidate {A1=U, …} ? Subsumed by conflict? : ? Suspend A1’s constraints ?Test : 1 1 Or2 Consistent Candidates: {{A1=U…}, {A2=U…}} Solutions: {{O1=U…}} Conflicts: {{O1=G, O2=G, A1=G}} No, since A1 = U, not A1=G 10/03/03 copyright Brian Williams, 2003 27 1 1 1 1 0 Or1 Or3 And1 And2 A B C D E F G X Y Z 0 1 Test Candidates Collecting Conflicts ? Fourth candidate {A2=U, …} ? Subsumed by conflict? : ? Eliminate candidate Or2 Consistent Candidates: {{A2=U…}} Solutions: {{O1=U…}, {A1=U…}} Conflicts: {{O1=G, O2=G, A1=G}} Yes, since O1=G,O2=G and A1=G 10/03/03 copyright Brian Williams, 2003 28 1 1 1 1 0 Or1 Or3 And1 And2 A B C D E F G X Y Z 0 1 Test Candidates Collecting Conflicts ? Return Solutions :O1 or A1 broken Or2 Candidates: {} Solutions: {{O1=U…}, {A1=U…} Conflicts: {{O1=G, O2=G, A1=G}} 10/03/03 copyright Brian Williams, 2003 29 Single Fault Diagnoses = {A1=U, M1=U} Single Fault Diagnoses are the Intersection of All Conflicts A1=U or M1=U or M2=U removes conflict 1. A1=U or A2=U or M1=U or M3=U removes conflict 2 {A1=G, M1=U, M2=U} conflict 1. {A1=U, A2=U, M1=U, M3=U} conflict 2 10/03/03 copyright Brian Williams, 2003 30 Outline ? Model-based diagnosis ? Accounting for failures ? Explaining failures ? Handling unknown failures ? Learning from symptoms and conflict ? Conflict learning ? Single-fault diagnosis ? Multiple-fault diagnosis 10/03/03 copyright Brian Williams, 2003 31 Multiple Faults Occur Image taken from NASA’s web site: http://www.nasa.gov. ? Quintuple fault occurs (three shorts, tank-line and pressure jacket burst, panel flies off). ? Power limitations too severe to perform new mission.. ? Novel reconfiguration identified, exploiting LEM batteries for power. ? Swaggert & Lovell work on Apollo 13 emergency rig lithium hydroxide unit. APOLLO 13 10/03/03 copyright Brian Williams, 2003 32 ? Candidate: Assignment to all component modes. 3 2 2 3 3 M1 M2 M3 A1 A2 A B C D E F G X Y Z 10 Adder(i): ? G(i): Out(i) = In1(i)+In2(i) ? U(i): 12 Diagnosis identifies consistent modes Candidate = {A1=G, A2=G, M1=G, M2=G, M3=G} 10/03/03 copyright Brian Williams, 2003 33 Diagnosis identifies All sets of consistent modes Adder(i): ? G(i): Out(i) = In1(i)+In2(i) ? U(i): ? Diagnosis D: Candidate consistent with model Phi and observables OBS. ? As more constraints are relaxed, candidates are more easily satisfied. ?Typically an exponential number of candidates. 3 2 2 3 3 M1 M3 A1 A B C D E F G X Y Z 10 12 Diagnosis = {A1=G, A2=U, M1=G, M2=U, M3=G} 10/03/03 copyright Brian Williams, 2003 34 ? ? “Smallest” sets of modes that remove all symptoms 3 2 2 3 3 M1 M3 A1 A B C D E F G X Y Z 10 12 ? Kernel Diagnosis = {A2=U, M2=U} Representing Diagnoses Compactly: Kernel Diagnoses Every candidate that is a subset of a kernel diagnosis is a diagnosis. 10/03/03 copyright Brian Williams, 2003 35 Kernel Diagnoses = Generate Kernels From Conflicts A1=U or M1=U or M2=U removes conflict 1. A1=U or A2=U or M1=U or M3=U removes conflict 2 “Smallest” sets of modes that remove all conflicts {A1=G, M1=U, M2=U} conflict 1. {A1=U, A2=U, M1=U, M3=U} conflict 2 10/03/03 copyright Brian Williams, 2003 36 Kernel Diagnoses = {A1=U} “Smallest” sets of modes that remove all conflicts A1=U or M1=U or M2=U removes conflict 1. A1=U or A2=U or M1=U or M3=U removes conflict 2 Generate Kernels From Conflicts 10/03/03 copyright Brian Williams, 2003 37 Kernel Diagnoses = {M1=U} {A1=U} “Smallest” sets of modes that remove all conflicts A1=U or M1=U or M2=U removes conflict 1. A1=U or A2=U or M1=U or M3=U removes conflict 2 Generate Kernels From Conflicts 10/03/03 copyright Brian Williams, 2003 38 Kernel Diagnoses = {A2=U, M2=U} {M1=U} {A1=U} “Smallest” sets of modes that remove all conflicts A1=U or M1=U or M2=U removes conflict 1. A1=U or A2=U or M1=U or M3=U removes conflict 2 Generate Kernels From Conflicts 10/03/03 copyright Brian Williams, 2003 39 Kernel Diagnoses = {M2=U, M3=U} {A2=U, M2=U} {M1=U} {A1=U} “Smallest” sets of modes that remove all conflicts A1=U or M1=U or M2=U removes conflict 1. A1=U or A2=U or M1=U or M3=U removes conflict 2 Generate Kernels From Conflicts 10/03/03 copyright Brian Williams, 2003 40 Diagnosis by Divide and Conquer Given model Phi and observations OBS ? 1. Find all symptoms ? 2. Diagnose each symptom separately (each generates a conflict :candidates) ? 3. Merge diagnoses (set covering :kernel diagnoses) General Diagnostic Engine [de Kleer & Williams, 87] 10/03/03 copyright Brian Williams, 2003 41 When you have eliminated the impossible, whatever remains, however improbable, must be the truth. - Sherlock Holmes. The Sign of the Four. Exploring the Improbable 10/03/03 copyright Brian Williams, 2003 42 A2=U M1=U M3=UA1=U A1=U, A2=U, M1=U, M3=U A1=U M1=U M2=U A1=U M1=U M1=U ? A2=U M2=U ? M3=U Conflict-Directed A*: Generating The Best Kernel A1=U, M1=U , M2=U Conflicts ? Minimal set covering is an instance of breadth first search. ? To find the best kernel, expand tree in best first order. Insight: ? Kernels found by minimal set covering 10/03/03 copyright Brian Williams, 2003 43 A1=U, A2=U, M1=U, M3=U A1=U M1=U M2=U M1=U Conflict-Directed A*: Generating The Best Kernel A1=U, M1=U , M2=U Conflicts ? Minimal set covering is an instance of breadth first search. ? To find the best kernel, expand tree in best first order. Insight: ? Kernels found by minimal set covering 10/03/03 copyright Brian Williams, 2003 44 Summary: Model-based Diagnosis ? A failure is a discrepancy between the model and observations of an artifact. ? Diagnosis is symptom directed ? Symptoms identify conflicting components as initial candidates. ? Test novel failures by suspending constraints and testing consistency. ? Newly discovered conflicts further prune candidates. 10/03/03 copyright Brian Williams, 2003Brian C. Williams, copyright 2000 451 Appendix: Modeling with Propositional Logic ? Syntax ? Semantics ? Clausal Form 10/03/03 copyright Brian Williams, 2003 46 How Do Model Complex Systems? Helium tank Fuel tankOxidizer tank Main Engines Flow 1 = zero Pressure 1 = nominal Pressure 2 = nominal Acceleration = zero 10/03/03 copyright Brian Williams, 2003 47 Outline ? Motivation ? Propositional Logic ? Syntax ? Semantics ? Propositional Satisfiability ? Systematic methods ? Characteristics of systematic search ? Through local search (optional) ? Summary ? Appendix: Reduction to Clausal Form 10/03/03 copyright Brian Williams, 2003 48 Propositional Logic: Syntax ? Proposition ? Statement that is true or false ? (valve v1) ? (= voltage high) ? Propositional sentence (S) ? S ::= proposition | ? (NOT S) | ? (OR S1 ... Sn) | ? (AND S1 ... Sn) ? Defined Constructs ? (implies S1 S2) => ((not S1) OR S2) ? (IFF S1 S2) => (AND (IMPLIES S1 S2)(IMPLIES S2 S1)) ? . . . 10/03/03 copyright Brian Williams, 2003 49 Engine Example: propositional logic sentence (mode(E1) = ok implies (thrust(E1) = on if and only if flow(V1) = on and flow(V2) = on)) and (mode(E1) = ok or mode(E1) = unknown) and not (mode(E1) = ok and mode(E1) = unknown) E1 V1 V2 10/03/03 copyright Brian Williams, 2003 50 Propositional Logic: Semantics An interpretation assigns true/false to every proposition symbol P i ? A = True, B = False, C = False TrueFalseFalse FalseFalseFalse FalseTrueFalse TrueTrueFalse FalseFalseTrue TrueFalseTrue FalseTrueTrue TrueTrueTrue CBA 10/03/03 copyright Brian Williams, 2003 51 Propositional Logic: Semantics The truth of sentence S is defined as a composition of boolean operators applied to the interpretation (S, S 1 and S 2 are sentences): ? Not S is True iff S is False ? S 1 and S 2 is True iff S 1 is True and S 2 is True ? S 1 or S 2 is True iff S 1 is True or S 2 is True FalseFalseFalse TrueFalseFalse FalseTrueFalse TrueTrueTrue S2S1S1 and S2 FalseFalseFalse TrueFalseTrue FalseTrueTrue TrueTrueTrue S2S1S1 or S2 10/03/03 copyright Brian Williams, 2003 52 Example: Determining the truth of a sentence (mode(E1) = ok implies [(thrust(E1) = on if and only if (flow(V1) = on and flow(V2) = on)) and (mode(E1) = ok or mode(E1) = unknown) and not (mode(E1) = ok and mode(E1) = unknown)]) Interpretation: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 53 Example: Determining the truth of a sentence (True implies [(thrust(E1) = on if and only if (flow(V1) = on and flow(V2) = on)) and (True or mode(E1) = unknown) and not (True and mode(E1) = unknown)]) Interpretation: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 54 Example: Determining the truth of a sentence (True implies [(False if and only if (True and False)) and (True or False) and not (True and False)]) Interpretation: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 55 Example: Determining the truth of a sentence (True implies [(False if and only if (True and False)) and (True or False) and not (True and False)]) Interpretation: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 56 Example: Determining the truth of a sentence (True implies [(False if and only if (True and False)) and (True or False) and not False]) Interpretation: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 57 Example: Determining the truth of a sentence (True implies [(False if and only if (True and False)) and (True or False) and True]) Model: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 58 Example: Determining the truth of a sentence (True implies [(False if and only if False) and True and True]) Model: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 59 Example: Determining the truth of a sentence (True implies [(False if and only if False) and True and True]) Model: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 60 Example: Determining the truth of a sentence (True implies [(False implies False ) and (False implies False )) and True and True]) Model: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 61 Example: Determining the truth of a sentence (True implies [(not False or False ) and (not False or False )) and True and True]) Model: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 62 Example: Determining the truth of a sentence (True implies [(True or False ) and (True or False )) and True and True]) Model: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 63 Example: Determining the truth of a sentence (True implies [(True and True) and True and True]) Model: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 64 Example: Determining the truth of a sentence (True implies [True and True and True]) Model: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 65 Example: Determining the truth of a sentence (True implies True) Model: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 66 Example: Determining the truth of a sentence (not True or True) Model: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 67 Example: Determining the truth of a sentence (False or True) Interpretation: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False 10/03/03 copyright Brian Williams, 2003 68 Example: Determining the truth of a sentence True! Interpretation: mode(E1) = ok is True thrust(E1) = on is False flow(V1) = on is True flow(V2) = on is False mode(E1) = unknown is False ?An interpretation that satisfies sentence S is called a Model of S 10/03/03 copyright Brian Williams, 2003 69 Propositional Clauses: A Simpler Form ? Literal: proposition or its negation ? B, Not A ? Clause: disjunction of literals ? (not A or B or E) ? Conjunctive Normal Form ? Phi = (A or B or C) and (not A or B or E) and (not B or C or D) ? Viewed as a set of clauses 10/03/03 copyright Brian Williams, 2003 70 Engine Example: Mapping to a Clausal Form (mode(E1) = ok implies (thrust(E1) = on iff flow(V1) = on and flow(V2) = on)) and (mode(E1) = ok or mode(E1) = unknown) and not (mode(E1) = ok and mode(E1) = unknown) not (mode(E1) = ok) or not (thrust(E1) = on) or flow(V1) = on; not (mode(E1) = ok) or not (thrust(E1) = on) or flow(V2) = on; not (mode(E1) = ok) or not (flow(V1) = on) or not (flow(V2) = on) or thrust(E1) = on; mode(E1) = ok or mode(E1) = unknown; not (mode(E1) = ok) or not (mode(E1) = unknown); 10/03/03 copyright Brian Williams, 2003 71 Reducing Propositional Formula to Clauses (CNF) ? Eliminate IFF and Implies ? E1 iff E2 => (E1 implies E2) and (E2 implies E1) ? E1 implies E2 => not E1 or E2 10/03/03 copyright Brian Williams, 2003 72 Engine Example: Eliminate IFF (mode(E1) = ok implies (thrust(E1) = on iff (flow(V1) = on and flow(V2) = on))) and (mode(E1) = ok or mode(E1) = unknown) and not (mode(E1) = ok and mode(E1) = unknown) 10/03/03 copyright Brian Williams, 2003 73 Engine Example: Eliminate IFF (mode(E1) = ok implies (thrust(E1) = on iff (flow(V1) = on and flow(V2) = on))) and (mode(E1) = ok or mode(E1) = unknown) and not (mode(E1) = ok and mode(E1) = unknown) (mode(E1) = ok implies ((thrust(E1) = on implies (flow(V1) = on and flow(V2) = on)) and ((flow(V1) = on and flow(V2) = on) implies thrust(E1) = on))) and (mode(E1) = ok or mode(E1) = unknown) and not (mode(E1) = ok and mode(E1) = unknown) 10/03/03 copyright Brian Williams, 2003 74 Engine Example: Eliminate Implies (mode(E1) = ok implies ((thrust(E1) = on implies (flow(V1) = on and flow(V2) = on)) and ((flow(V1) = on and flow(V2) = on) implies thrust(E1) = on))) and (mode(E1) = ok or mode(E1) = unknown) and not (mode(E1) = ok and mode(E1) = unknown) 10/03/03 copyright Brian Williams, 2003 75 Engine Example: Eliminate Implies (mode(E1) = ok implies ((thrust(E1) = on implies (flow(V1) = on and flow(V2) = on)) and ((flow(V1) = on and flow(V2) = on) implies thrust(E1) = on))) and (mode(E1) = ok or mode(E1) = unknown) and not (mode(E1) = ok and mode(E1) = unknown) (not (mode(E1) = ok) or ((not (thrust(E1) = on) or (flow(V1) = on and flow(V2) = on)) and (not (flow(V1) = on and flow(V2) = on)) or thrust(E1) = on))) and (mode(E1) = ok or mode(E1) = unknown) and not (mode(E1) = ok and mode(E1) = unknown) 10/03/03 copyright Brian Williams, 2003 76 Reducing Propositional Formula to Clauses (CNF) ? Move negations in to propositions (De Morgan) ? Not (E1 and E2) => (not E1) or (not E2) ? Not (E1 or E2) => (not E1) and (not E2) ? Not (not E1) => E1 10/03/03 copyright Brian Williams, 2003 77 Engine Example: Move Negations In (not (mode(E1) = ok) or ((not (thrust(E1) = on) or (flow(V1) = on and flow(V2) = on)) and (not (flow(V1) = on and flow(V2) = on)) or thrust(E1) = on))) and (mode(E1) = ok or mode(E1) = unknown) and not (mode(E1) = ok and mode(E1) = unknown) 10/03/03 copyright Brian Williams, 2003 78 Engine Example: Move Negations In (not (mode(E1) = ok) or ((not (thrust(E1) = on) or (flow(V1) = on and flow(V2) = on)) and (not (flow(V1) = on and flow(V2) = on)) or thrust(E1) = on))) and (mode(E1) = ok or mode(E1) = unknown) and not (mode(E1) = ok and mode(E1) = unknown) (not (mode(E1) = ok) or ((not (thrust(E1) = on) or (flow(V1) = on and flow(V2) = on)) and (not (flow(V1) = on) or not (flow(V2) = on)) or thrust(E1) = on) ) and (mode(E1) = ok or mode(E1) = unknown) and (not (mode(E1) = ok) or not (mode(E1) = unknown))) 10/03/03 copyright Brian Williams, 2003 79 Reducing Propositional Formula to Clauses (CNF) ? Move conjunction out (Distribution) ? E1 or (E2 and E3) =>(E1 or E2) and (E1 or E3) 10/03/03 copyright Brian Williams, 2003 80 Engine Example: Move Conjunctions Out (not (mode(E1) = ok) or ((not (thrust(E1) = on) or (flow(V1) = on and flow(V2) = on)) and (not (flow(V1) = on) or not (flow(V2) = on) or thrust(E1) = on))) and (mode(E1) = ok or mode(E1) = unknown) and (not (mode(E1) = ok) or not (mode(E1) = unknown)) 10/03/03 copyright Brian Williams, 2003 81 Engine Example: Move Conjunctions Out (not (mode(E1) = ok) or ((not (thrust(E1) = on) or (flow(V1) = on and flow(V2) = on)) and (not (flow(V1) = on) or not (flow(V2) = on) or thrust(E1) = on))) and (mode(E1) = ok or mode(E1) = unknown) and (not (mode(E1) = ok) or not (mode(E1) = unknown)) (not (mode(E1) = ok) or (((not (thrust(E1) = on) or flow(V1) = on) and (not (thrust(E1) = on) or flow(V2) = on)) and (not (flow(V1) = on) or not (flow(V2) = on) or thrust(E1) = on))) and (mode(E1) = ok or mode(E1) = unknown) and (not (mode(E1) = ok) or not (mode(E1) = unknown)) 10/03/03 copyright Brian Williams, 2003 82 Engine Example: Move Conjunctions Out (not (mode(E1) = ok) or (((not (thrust(E1) = on) or flow(V1) = on) and (not (thrust(E1) = on) or flow(V2) = on)) and (not (flow(V1) = on) or not (flow(V2) = on) or thrust(E1) = on))) and (mode(E1) = ok or mode(E1) = unknown) and (not (mode(E1) = ok) or not (mode(E1) = unknown)) 10/03/03 copyright Brian Williams, 2003 83 Engine Example: Move Conjunctions Out (not (mode(E1) = ok) or (((not (thrust(E1) = on) or flow(V1) = on) and (not (thrust(E1) = on) or flow(V2) = on)) and (not (flow(V1) = on) or not (flow(V2) = on) or thrust(E1) = on))) and (mode(E1) = ok or mode(E1) = unknown) and (not (mode(E1) = ok) or not (mode(E1) = unknown)) (not (mode(E1) = ok) or not (thrust(E1) = on) or flow(V1) = on) and (not (mode(E1) = ok) or not (thrust(E1) = on) or flow(V2) = on)) and (not (mode(E1) = ok) or not (flow(V1) = on) or not (flow(V2) = on) or thrust(E1) = on) and (mode(E1) = ok or mode(E1) = unknown) and (not (mode(E1) = ok) or not (mode(E1) = unknown))