Critical Reasoning

1 Combinatorial Explosion

Model-based diagnosis engines [de K.leer and Williams 87; de K.leer 91; Reiter 87] face a potential combinatorial explosion of:

1. the environment space,
2. the conflict space,
3. the diagnosis space.

This paper presents a new architecture, IMPLODE, which re­ quires neither a candidate generator nor checking candidates for consistency. IMPLODE uses a sensitivity analysis of as­ sumptions to assign a criticality level to assumptions. IM­ PLODE keeps track of the assumptions' criticality level, and builds up an abstract representation of the environment, con­ flict and diagnosis spaces, using a database of:

1. critical environments,
2. critical conflicts,
3. critical diagnoses.

IMPLODE avoids the combinatorial explosion of previous gen­ erations of model-based diagnostic engines. Experimental results show that the most dramatic improvement is obtained for the circuits which are the most difficult to diagnose us­ ing previous diagnosis engines. Moreover, typical sources of combinatorial explosion, such as reconvergent fanout, are a source of combinatorial implosion for IMPLODE.

2 Sensitivity Analysis

One of the earliest model-based diagnosis engines is SOPHIE [de Kleer and Brown 92]. SOPHIE utilizes a form of sensi­ tivity analysis based on partitioning the set of assumptions supporting a prediction into two sets:

1. The set of primary assumptions, P,
2. The set of secondary assumptions, S.

SOPHIE's criterion for determining whether an assumption is primary or secondary is based on a form of order of magnitude reasoning. An assumption which significantly contributes to the magnitude of the predicted value is primary otherwise it is secondary. In other words, the magnitude of the predicted value is extremely sensitive to its primary assumptions. One of SOPHIE's rules which exploits this distinction restricts the hypothesis space as follows: If two environments ( Pt, S 1) , and (P2, S2). support the same prediction, then all the com­ ponents which belong to [ P1 u P2] - [ Pt n P2] are exonerated. The intuition behind the rule is as follows. If an assumption which significantly contributes to the predicted value is vio­ lated, then the predicted value would be significantly different. Thus, assumptions not in common between the antecedent pri­ mary assumption sets are exonerated.

SOPHIE's use of sensitivity analysis for model-based diag­ nosis is based on a number of presuppositions which limit its generality:

1. Environment space: The criterion used to distinguish primary and secondary assumptions is specific to the domain of analog circuits.
2. Conflict space: The partitioning into primary and sec­ ondary assumptions is not extended to confficts - so­ PHIE does not distinguish between primary and secondary assumptions in conflicts.
3. Diagnosis space: The exoneration rule is based on the single-fault assumption.

3 Critical Environments and Abstractions

The assumption set A contains ok ( C J) for every component C J. The description of the system to diagnose and the obser­ vation set are given by (effectively) a propositional theory T over a set of literals C. We presume that T is consistent. A node n designates a literal, that is an atom or its negation.

An environment E supporting a literal n is a set of assump­ tions such that:

1. [Entailment]: T U E f= n.

2. [Consistency]: T U E is consistent.

The set of environments supporting a literal is noted £ ( n). £ ( n) is characterized by its minimal (with respect to set in­ clusion) elements, called minimal environments. However these minimal environments are computationally prohibitive to construct. As an alternative, the following definition of critical environment introduces an abstraction which can be used to characterize £ ( n) far more parsimoniously.

Definition 3.1 (Critical Environment) The critical environ­ ment for node n relative to S ~ A is:

0

Here and in the following we shall assume that there is a special assumption, called false which takes on the value false in all models, and that n 0 d;j {false}.

Example 3.1 Consider the circuit, (see Figure 3), consisting of an or-gate, Or, two rows of buffers, {B1, B2}. {B3, B4}, and an inverter, C , at the output of the or-gate. Let S be the entire set A.

Given, the observations { i 1 = 1, i2 = 1}, there are two minimal environments supporting the prediction Or = 1:

ok (Or) is the only assumption which is common to these two environments. Therefore the critical environment for Or = 1 relative to A is { ok( Or)}. 0

Notice that the critical environment for a literal n relative to S is always included in the minimal environments for n in S. If a node has a single minimal environment E in S, then E is also the critical environment for n relative to S.

The abstraction process leading to the generation of critical environments ensures the following local consistency property for the critical environment any given node:

Proposition 1 T U S ( n) is consistent if T is consistent and S ( n) is consistent.

Proof 1 S ( n) is an intersection of environments which by definition already possess this consistency property (if it is consistent, i.e., does not contain false). 0

Thus critical environments inherit the consistency property of environments. However, in general it is not true that critical environments inherit the entailment property of environments, i.e. in general it is not true that T U S ( n) f= n. In general, the critical environments only possess the entailment property if the background theory T is augmented adequately. But augmenting T may lead to inconsistencies. The following sections introduce the concept of critical conflicts and critical diagnoses to determine how to augment T so that the critical environments become environments of the augmented theory, and show how to exploit the augmented theory for diagnosis purposes.

4 Critical Conflicts

A conflict C is a set of assumptions such that C u T is in­ consistent. A minimal conflict has no other as a subset. As the number of conflicts also explodes we exploit similar intu­ itions to those underlying critical environments to introduce the notion of critical conflicts.

Definition 4.1 (Critical Conflicts) The critical conflict for S ~A is:

0

Example 4.1 (Continued) If C = 1 the minimal conflicts are:

Thus:

0

Since the minimal conflicts characterize all conflicts (via subset), we can always use the minimal conflicts to stand for all the conflicts in our definitions and examples. This example shows that a critical conflict relative to S subsumes all the conflicts in S.

Critical conflicts offer an abstract representation of the con­ flict space. Critical conflicts are also the keystone for iden­ tifying whether or not a critical abstraction which abstracts simultaneously the environments for multiple nodes preserves the consistency of the background theory T. More precisely, a critical abstraction is defined as follows:

Definition 4.2 (Critical Abstraction) The critical abstrac­ tion of a theory T relative to S ~ A is the theory:

0

Note that the process of abstraction adds only Hom clauses to the original theory; in particular the abstraction of a Hom theory is a Hom theory.

Proposition 2 (Consistency of Critical Theories) S(T) is consistent iff S( l_) -1- 0.

Proof2 Assume that S(l.) = 0. Since S(_i) --+ l_ belongs to S(T), S(T) is inconsistent.

Assume that S(_i) -1- 0; choose A E S(_i). Since A belongs to all the conflicts in S it follows that: T' d;j T U (S\ {A} )U{A} is consistent. To prove that S(T) is consistent, it suffices to prove that

for each node n. This follows trivially if A E S ( n). If not, there is an environment E ~ ( 5 \ {A}) for n. But then T I= ( 5 \ {A}) ---> n, so that T' I= n. D

In many cases A( .l) will be non-empty -all the conflicts will have a non-empty intersection. For instance, this will happen if the system obeys a single-fault assumption. In this case {A} is a minimal diagnosis for every A E A( .l ).

However, it could be that A( .l) = 0. In such a case there must be at least two mutually disjoint conflicts, C 1 and C2 in A. Thus, we can partition A into two subsets 5t (containing C 1) and 52 (containing C2). We may then exploit the intuition that often designed systems are constructed in such a way that they are nearly decomposable. So we may choose to transform the initial search for diagnoses into two separate diagnosis problem: we consider the assumptions in 51 separately from those in 52, constructing separately the critical environments and conflicts for these two sets. Once that is done, we desire to glue together information about the diagnosis of the system gleaned from these two disjoint analyses.

In general, however, St (T) U S2(T) is not guaranteed con­ sistent even if separately both S 1 ( T ) and S2 ( T) are consistent. (Examples are easy to construct.) We now give certain rather general conditions under which the consistency of conjunc­ tions of critical abstractions is guaranteed.

Definition 4.3 (Critical Cover) A critical cover relative to a subset 5 of A is a set {51 , . .. , 5 k } of subsets of 5 such that:

Critical consistency: S; ( .l) is non-empty, for all i.

Covering: Every conflict C ~ 5 is subsumed by S;(.l), for some i.

Disjointness: S; ( .l) is disjoint from 5i, for every distinct i andj.

D

In such a case, the set { S 1 ( .l), . . . , S k ( .l)} is called a covering set of critical conflicts. Note that the disjointnes~ condition implies that S; ( .l) is distinct from Si ( .l) -hence any cover contains at most I 5 I critical conflicts.

Proposition 3 (Consistency or critical covers.) If S is a critical cover relative to A then

is consistent.

Proof 3 The proof is very similar to that of Theorem 2. Since each S; ( .l) is non-empty, choose an A; E S; ( .l ). Consider the augmented theory

By Disjointness, T' is equivalent to

First, we claim that T' is consistent. Suppose it is not. Then it must be the case that

However, if the 5; are not trivial (that is, contain at least one conflict), then for each i, there must be a conflict of the form A;, 6; --->where 6; ~ 5; \{A;}. Hyper-resolving the k such clauses against the clause in ( 11) yields the A conflict of T:

However, this conflict is not subsumed by any S; ( .l) (which must contain A;), in violation of our Coverage assumption. The contradiction establishes that T' is consistent.

Now we show that for every literal n and i:

This obviously follows if A; E S; ( n). Otherwise, there is some environment for n contained in 5; \ {A;}; that is T I= E---> n, where E ~ 5; \{A;}. It follows then that T' I= n, and we are done. D

Critical covers do not always exist as the following example shows.

Example 4.2 The simplest example is given by the cyclic theory:

Take S = A = {a, b, c }. The only subset of 5 for which there is a non-trivial intersection of conflicts is the set 5 - however, in this case the interseCtion is 0. D

When critical covers do not exist, we are obliged to seek for maximal subsets of A which do have a cover. Explor­ ing the space of weaker definitions of critical cover (that will guarantee the existence of critical covers in more cases) is beyond the scope of the paper. We expect to see significant tradeoffs between the weakness and computability of the def­ initions; indeed we would not be surprised if it is impossible to simultaneously achieve a definition of critical cover that guarantees that only minimal diagnoses are generated (see Theorem 6 below), that always exists for consistent theories, and that can be used to compute critical diagnoses efficiently and incrementally.

5 Critical Diagnoses

This section exploits the concept of criticality to obtain a concise representation of the diagnosis space. For a given ~ of literals 5, the set {I I l E 5} is noted S. We shall treatS as identical to 5. A diagnosis is a set S for some 5 ~ A such that T u S is consistent.

Definition 5.1 (Critical diqnosis) A critical diagnosis ofT relative to a 5 ~ A is a set .1 n S such that:

1. .1 is a diagnosis of S(T).
2. There is no other diagnosis .1' of S(T) such that .1' n S is a strict subset of .1 n S.

D

In the following, by a critical diagnosis of T, we shall mean a critical diagnosis of T relative to A.

Example 5.1 (Continued) Since

A( .l) = { ok( Or), ok( C)}, the critical diagnoses relative to A are the two potential single faults: { ok( Or)} and { ok( C)}.

D

Say that a diagnosis .1 hits a conflict C if there exists an A E .1 such that A E C.

Proposition 4 If S(T) is consistent, and there is at least one conflict C ~ S ofT, then the set of critical diagnosis ofT relative to S is

Proof 4 Assume S contains at least one conflict of T. Any diagnosis of S ( T) must hit S ( l.); indeed any element of S ( l.) is adequate. A critical diagnosis can contain at most one such element. 0

Note that if S does not contain any conflict ofT, then S ( l.) = {false}, yielding the vacuous critical diagnosis 0.

ElUUDple 5.2 (Continued) SinceA(l.) = { ok(Or ), ok( C)} Therefore the critical diagnoses relative to A are the two potential single faults: { ok (Or)} and { ok (C)}. 0

Proposition 5 Every critical diagnosis ofT relative to any S ~ A is a subset of a minimal diagnosis ofT.

Proof 5 No proper subset of a critical diagnosis relative to S can hit all the conflicts of S. 0

Theorem 6 (Diagnostic Hypercube) Let { S 1, ... , Sk} be a critical cover of A for T. If .1; is a critical diagnosis for S;, then .1 = .1t u . . . u .1k is a minimal diagnosis for T.

Proof 6 Since .1 hits every conflict in A, it is a diagnosis. Suppose it is not minimal. Then there is an A E .1 such that .1' = .1 \ {A} is a diagnosis. Note that there is exactly one i :::; k such that A E S; ( l. ). (To avoid trivialities, assume that A is distinct from false.) However, .1' cannot hit any of the conflicts contained in S;, since .1' is disjoint from S;. Hence .1' cannot be a diagnosis. 0

Thus finding a critical decomposition of A, if any, allows a linear encoding ·of an exponential number of minimal diag­ noses.

ElUUDple 5.3 (Continued) Since A forms a critical partition, T contains two single faults as minimal diagnoses: { ok (Or)} and { ok( C)}. 0

Proposition 7 If A forms a critical partition then A( l.) con­ tains all the single faults.

Searching for critical conflicts enables an architecture for model-based diagnosis which ensures the consistency of the candidates while bypassing the interpretation construction and context switching of conventional diagnostic algorithms.

5.1 Critical Probes

For the purpose of this paper we assume that probing is the only kind of action available to differentiate among different diagnoses. We ignore component failure rates and cost of probes. The conventional (GDE-like) approach to finding the probe which differentiates best among all the diagnoses is to determine the environments for the different nodes.

Our strategy here is to focus on critical diagnoses and find a probe which differentiates best among the critical diagnoses. To identify this probe we would like to consider the nodes' critical environments. To justify ignoring the supersets of critical environments we show that once the diagnosis space is restricted to the set of critical diagnoses the critical envi­ ronments possess the following entailment property:

Proposition 8 (Critical Entailment) Let St, ... , Sk be a critical partition of A, and P be the product space of crit­ ical diagnoses, and n be a literal of C.

Example5.4 (Continued) Since A(Or = 1) = {ok(Or)} and A(Or = 0) = {ok(C)}, probing the output of the Or performs a half split on the space of critical diagnoses. Thus, if initially all the components are equally likely to fail and the cost of different probes are the same, this output of Or is the probe which differentiates best among the critical diagnoses. Notice also that, in this case, the output of Or is also the best probe to differentiate among all consistent diagnoses. 0

As new observations are gathered, the evolution of critical environments, critical conflicts and critical diagnoses may be non monotonic if the new observation eliminates all the critical diagnoses.

Example 5.5 (Continued) The two critical diagnoses predict that B2 should be 1. If the output of B2 is observed to be 0, then all the critical diagnoses are eliminated and there is a non monotonic evolution of the critical diagnoses. If B2 = 1, then there are two disjoint minimal conflicts: {ok(Bt), ok(B2)} and {ok(B3), ok(B4), ok(Or), ok(C)}. These two disjoint minimal conflicts become the covering set of critical conflicts. The new set of critical diagnoses is given by the product space:

This non monotonicity highlights the fact that critical rea­ soning is a particular form of non monotonic reasoning. Ex­ ploring the link between critical reasoning and other forms of non monotonic reasoning is beyond the scope of this paper.

6 IMPWDE Algorithm

Given a Hom propositional theory which has a covering set of critical conflicts, IMPLODE identifies the critical conflicts and computes critical environments, and concisely encodes the set of critical diagnoses.

IMPLODE is an incremental algorithm. Counterintuitively, it does not operate by maintaining a single global data structure of the current best approximation of a critical cover which is then incrementally updated. Much in the spirit of an ATMS, each environment also carries with it, locally, the smallest set of assumptions (discovered so far in the process) which makes the environment a critical one.

We expand the notation of Section 2 to include the node or assertion which it supports. The triple (M, P, S) denotes a clause whose literals are M UP u S. P is the set of primary assumptions, S is the set of secondary assumptions, and M is the remaining set of literals. ( 0, P, S) represents a conflict.

Each (M, P, S) represents a critical environment (or con­ flict). Pis the critical environment of M relative toP uS. P and S are always kept disjoint: S is the set of assumptions that are needed to be combined with P which makes P a critical environment. More formally:

During execution IMPLODE is only representing approxima­ tions of critical environments and critical conflicts. At the conclusion of the algorithm (if it terminates successfully) the current set of critical conflicts form a critical cover.

IMPLODE takes as input the set of clauses T and produces new clauses using the following rules: IMPLOSION:

RESOLUTION: If m E M unless P1 U P2 = 0 and M = { m }.

EXPLOSION:

IMPLODE, incrementally applies these rules, to a restricted set of clauses, the active clauses. Active clauses are deter­ mined by the following rules. When IMPLODE receives a new clause, this clause is initially marked as active. A clause can become inactive by either being critically subsumed or by be­ ing suppressed. A clause (M1, P1, 51) is critically subsumed if there is another active clause (M2, P2, 52) such that M2UP2 is a strict subset of M1 U P1 or just of 51 alone. When IM­ PLODE finds multiple critical environments for a node, it sys­ tematically chooses only one of those critical environments to propagate via the resolution rule - the other critical en­ vironments are suppressed (inactivated). An inactive clause whose reason for inactivation itself is inactivated or removed is reactivated.

IMPLODE prioritizes rule applications by always running higher priority rules if they are applicable:

1. Reactivate clauses whose reason for inactivation has dis­ appeared.
2. Inactivate any clauses which are now critically subsumed.
3. Apply EXPLOSION.
4. Apply IMPLOSION.
5. For any literal with more than one critical environment, suppress all but one by marking it inactive because of the chosen critical environment.
6. Apply RESOLUTION.

Note that in this algorithm the number of critical environ­ ments for a node can never explode. Even in examples (such as levels of alternating and/or gates) which cause exponential behavior for GDE-like algorithms for single faults IMPLODE performs well.

7 IMPLODE Example

T, the initial set of clauses contains the models for all the components and connections. For example, the buffer B 1 is modeled by the two clauses:

The connection i 1 is modeled by the single clause:

The two observations are:

Repeated applications of the resolution rule produces the fol­ lowing clauses:

The Implosion rule produces:

This clause immediately inactivates the two clauses marked t. Resolution produces:

Now suppose we observed:

Resolution immediately produces the critical conflict:

This critical conflict permanently inactivates the clause t. The resolution rule also produces:

Now suppose we observe:

Resolution produces the critical conflict:

This clause inactivates the clauses marked · and this now causes the clauses marked t to be reactivated except the first such clause is immediately inactivated again by the new crit­ ical conflict. The single activated clause resolves to produce the critical conflict:

8 Experimental Results

We have adapted our [de Klcer 91] model-based diagnosis algorithm to implement IMPLODE. IMPLODE is sufficiently different, that an overall reimplementation would produce far more significant performance improvements. But we report preliminary results in the following table. This table provides the results on only a few instances of each circuit. All in­ stances are examples which had been earlier determined to be the most difficult for the unoptimiz.ed focused algorithm [de Kleer 91 1 and therefore the timings are far worse than average for those circuits. Each run is of a single test vector and one symptomatic output. All of the circuits are from the test suite provided in [Brglez eta/. 85]. The timings are obtained on a SymbolicsXL1200,andincludethesetuptimeforrunningthe experiment (which is now the dominant cost). The table has two columns. The first contains the timing for the algorithm of [de Klcer 91] entitled "AAAI91 ", the second one contains IMPLODE's timing.

IMPLODE shows the greatest improvement on the circuits with significant redundancy and reconvergent fanout- some­ thing extremely difficult for previous algorithms. For exam­ ple, circuit c6288 is a 16 by 16 bit parallel multiplier and manifests a great deal of reconvergent fanout.