The Route to Success - A Performance Comparison of Diagnosis Algorithms

1 Introduction

Explanations for unexpected or even faulty system behavior are a most welcome asset when faced with such behavior during system development or maintenance. The task of diagnosing a system, that is, identifying root causes for encountered errors, got a lot of attention in the AI community, so that in the last three decades many different AI-based approaches tackling this issue have been emerging.

The computational power of available control systems and PCs has been growing continuously, enabling AI-based diagnosis approaches for more and more practical purposes. This, however, leaves us with the question of which approach to adopt for a certain project. Some approaches, e.g. [Reiter, 1987; Greiner et al., 1989; de Kleer and Williams, 1987; Stern et al., 2012], exploit the fact that, given a correct system model, diagnoses are related to conflicts between actual observed system behavior and a system's model, that is conflicts in the assumptions whether the system's single components operate correctly. Others, e.g. [Fr¨ohlich and Nejdl, 1997; Feldman et al., 2010; Metodi et al., 2012; Nica and Wotawa, 2012], derive a set of consistent assumptions on the system's components' status directly, without considering conflicts. Common to all is the use of some reasoning engine (theorem prover) for deriving (or verifying) hypotheses and optionally also for computing the conflicts.

In this paper, we investigate run-time performance trends for various conflict-driven and direct setups. In our tests, we evaluated a publicly available diagnosis engine and implementations of several algorithms. The various setups perused different reasoning engines like a Horn-clause theorem prover developed specifically for diagnosis purposes, two generalpurpose satisfiability solvers, as well as a general-purpose constraint solver.

Our aimwas to identify trends in the run-times suggesting advantages for one or the other approach, and contributing to answering the question whether a general-purpose solver can be used for an efficient diagnosis in practice; or if we still need a specifically tailored engine for achieving the necessary performance.

The remainder of this paper is structured as follows. In Section 2, we introduce several definitions and discuss related work including available algorithms. In Section 3, we describe our selection of algorithms and their implementations as used for our performance tests. Our test setup and experimental results are reported in Section 4, followed by our conclusions and future work, depicted in Section 5.

2 Preliminaries and RelatedWork

[Reiter, 1987] formalizes a model-based diagnosis approach based on a system description's consistency with actually observed behavior: A system description SD defines the nominal behavior of a set of interacting components c ∈ COMP via sentences ¬AB(c) ⇒ NominalBehavior(c), where AB(c) is an assumption whether a component c's status is abnormal or not and NominalBehavior defines the system's correct behavior (Reiter uses first order logic). As Reiter includes no knowledge about faulty behavior, his approach is considered to implement a weak fault model. Given some actual observations OBS, a system is considered to be at fault iff SD ∪ OBS ∪ {¬AB(c)|c ∈ COMP} is inconsistent.

Definition 1 A diagnosis ∆ ⊆ COMP is a subset-minimal set such that SD ∪ OBS ∪ {¬AB(c)|c ∈ COMP \ ∆} is consistent.

Reiter proposed to derive diagnoses explaining the inconsistent observations via conflicts. His reasoning is based on the fact that for his definitions, the set of diagnoses is equal to the set of minimal hitting sets of the set of (not necessarily minimal) conflicts, i.e., if such a set includes at least all minimal conflicts.

Definition 2 A set C ⊆ COMP is a conflict if and only if SD ∪ OBS ∪ {¬AB(c)|c ∈ C} is inconsistent. If no proper subset of C is a conflict, C is a minimal conflict.

Reiter's complete algorithm (see also Section 3.1) maintains and prunes a tree that encodes the search pattern and intermediate results in order to achieve a structured and complete exploration of the diagnosis search space (that is exponential in the number of components). [Greiner et al., 1989] proposed an improved version, HS-DAG, using a directed acyclic graph and addressing minor but serious flaws in Reiter's formulations. [Wotawa, 2001] suggests with HST (see Section 3.1) a variant of Reiter's idea that tries to avoid building nodes that would be pruned anyway. [de Kleer and Williams, 1987] use an assumption-based truth maintenance system (ATMS) [de Kleer, 1986] to deduce the set of conflicts for an observation, where their General Diagnosis Engine (GDE) then derives via hitting set computations the desired diagnoses. Re-framing the diagnosis problem into an optimal constraint satisfaction problem, the conflict-directed A* algorithm [Williams and Ragno, 2007] generates diagnoses incrementally in best-first order and, additionally, uses conflicts to focus the search. [Stern et al., 2012] introduce the switching diagnostic engine SDE that interleaves the search for diagnoses and conflicts, exploiting the dual relation between diagnoses and conflicts via minimal hitting sets also in the reverse direction. Also interested in minimal conflicts, [Junker, 2004] introduces a preference-controlled algorithm, based on a divide-and-conquer search strategy. Starting from the idea that previous conflict detection algorithms have not exploited the basic structural properties of constraint-based recommendation problems, [Schubert et al., 2010] came up with another algorithm for an efficient identification of minimal conflicts, based on a table representation of the input and inspired by HS-DAG. While [Mozetic, 1992] aims at computing the minimal diagnoses directly via non-minimal ones, conflicts are still computed and used to prune the search space.

[Fr¨ohlich and Nejdl, 1997] proposed to directly manipulate logic models when searching for a diagnosis, without computing conflicts. Via the notion of satisfiability, one can easily encode an MBD problem. That is, introducing the corresponding variables AB(c) and connecting them to nominal behavior as above, one searches in a single query for a solution (or all, depending on the engine) up to some problem bound k limiting the diagnosis cardinality. Starting with 1, k is incremented when no solution is found (anymore). As we search for all solutions in our scope (in order to be complete), we have to add each diagnosis ∆ found as a blocking clause (in the form of ¬∆ when considering ∆ as conjunction of its elements) to the problem, in order to exclude itself and its supersets from further search. This way, the subsetminimality of derived diagnoses is ensured, and incrementally raising bound k enables us to derive all diagnoses up to some desired cardinality. Essential, however, are a reasoning model and an engine that allow us to limit k in the search.

[Feldman et al., 2010] proposed to use MAX-SAT in this respect, and implemented with MERIDIAN a corresponding approach. Via Odd-Even Mergesort (OEMS) networks [Batcher, 1968], or Cardinality Networks [As´ın et al., 2009] this requirement can be easily encoded in the Boolean domain to be directly attached to a model (obviously one could describe these networks also with constraints). An example approach in this direction is [Metodi et al., 2012], which uses constraints as intermediate format that are compiled into a SAT problem. [Nica and Wotawa, 2012] proposed with ConDiag (see Section 3.4) an algorithm capable of obtaining diagnoses directly from a constraint set, using a general-purpose constraint solver as reasoning engine.

There is yet another category of diagnosis algorithms computing diagnoses directly from the model without deriving hitting sets of conflicts. These algorithms have in common that they are based on tree-structured models. [Fattah and Dechter, 1995] and later [Stumptner and Wotawa, 2001] described algorithms that exploit tree-structured constraint systems. [Sachenbacher and Williams, 2004] generalized these algorithms. [Stumptner and Wotawa, 2003] discuss the coupling of decomposition methods for constraint satisfaction problems with tree-structured diagnosis algorithms, in order to make those compatible with non-tree-structured models.

3 Selected Diagnosis algorithms

In the following, we depict our six selected setups that contrast several conflict-driven search algorithms with approaches based on a more direct reasoning.

As we are interested in the performance one can achieve with off-the-shelf tools, we used varying corresponding publicly available reasoning engines. In the following subsections, we give brief descriptions of the algorithms and discuss for each setup the specific interfaces, reasoning engines, as well as the individual modeling concepts for the digital circuits used in our test suites (see Section 4). Occasionally we make notes regarding the performance of further internally available, comparable setups from our optimization process.

Our three conflict-based setups peruse diagnosis algorithms that compute the subset of conflicts as needed on-thefly, which is an attractive feature for practical applications. There, one often restricts the maximum cardinality in order to keep the search space (and in turn the set of required conflicts) as small as possible.

With our three direct-search based setups we compare the MAX-SAT idea with cardinality networks as outlined in Section 2. Like the complexity discussion in Section 3.3 suggests, internal tests showed cardinality networks to be ways more efficient than OEMS, so that we do not report on such a version. To the best of our knowledge, no current version of a tree-structured-model-oriented approach is publicly available so that we have no corresponding setup in our selection.

It shall be noted that, on purpose, we do not apply any pre- or post-processing steps as used in other publications for speedups, e.g. [de Kleer, 2011; Metodi et al., 2012]. In order to be fair, such pre-processing steps would have to be included in every setup, so that on one hand the effects should be comparable, and on the other one, we do not aim at identifying the efficiency of such optimizations, but the efficiency of the two general search concepts as outlined in the introduction. In practice, one certainly will explore modeloptimizations suitable for a specific project and the corresponding problem domain. Our scope is, however, the general diagnosis approach performance behind search concepts.

3.1 Conflict-Driven Algorithms using SAT

We implemented two conflict-driven setups using a SAT solver for proving deduced theories. The first, HS-DAGSAT is based on Greiner et al.'s improved version of Reiter's idea.

Reiter's algorithm maintains a tree, where each non-leaf node n is labeled with a conflict C. For each component c in this conflict there is an outgoing edge e labeled with c. Node labels C are chosen such that the set of edge labels h(n) on the path from the root to n may not intersect with the node's label. New conflict sets are retrieved by checking a new node n's set of edge labels h(n) for consistency, assuming h(n) to be a diagnosis, i.e., its components to operate abnormal (all others normal). When consistent, n is a leaf and the edgelabels h(n) represent a diagnosis. Otherwise, a new conflict set is derived as label for this node. The tree is constructed in a breadth-first manner, and several ideas are used to prune the tree and ensure the minimality of the derived solutions. [Greiner et al., 1989] presented with HS-DAG an improved version that uses a directed acyclic graph and addresses some minor but serious flaws in Reiter's original formulations.

The second setup, HSTSAT, is based on Wotawa's variant HST of Reiter's idea that tries to avoid constructing nodes that would be pruned by HS-DAG. Adopting an idea used for subset computation, HST orders the elements in COMP, and, defined by those elements encountered in the tree so far (with a special focus on the current path), the algorithm limits a node's outgoing edges to some range in COMP. Thus, it omits some edges HS-DAG would construct, but only when the corresponding label combinations would be investigated in other branches anyway (if they are of interest).

Both setups use an internal set CC of conflicts that is extended whenever a new conflict C is encountered. Thus CC acts as cache to SAT-solver calls, where we first search in CC for some C not intersecting with h(n). A cache miss followed by a satisfying SAT instance then identifies a leaf-node.

While the domain of our test models (see Section 4) is purely Boolean, we use the SMT solver Yices 1 for our experiments for two reasons. First, it can be launched in daemon mode in order to solve multiple similar problems by retracting old and adding new assertions. Second, its conflict search can be focused on our AB(c) predicates via extended assertions (assert+). Our corresponding Yices model is as follows,

∀(v, b) ∈ OBS :(define v::bool b) ∀c ∈ COMP :(define ABc::bool) (assert¬ABc → outc = fc(in 1c , . . .)) ∀c ∈ COMP \ h :(assert+ ¬ABc) ∀c ∈ h :(assert+ ABc),

1 http://yices.csl.sri.com

where h is the set of edge labels h(n), and inic , outc and fc are a component c's input-/output signals and its Boolean function implemented using Yices' built-in Boolean operators. In subsequent calls, only AB(c) predicate assignments are updated while the system description is retained. A satisfiable instance indicates a consistent assignment h, whereas for an unsatisfiable one, we identify a new conflict by deriving an unsatisfiable core in terms of AB(c) predicates.

Both HS-DAG and HST can be limited efficiently to compute only diagnoses up to a given cardinality by stopping node expansion at the corresponding DAG/tree level.

3.2 Conflict-Driven Search via Horn Clauses

Our tests included also a setup HS-DAGHC using the publicly available diagnosis engine JDiagengine 2 . This engine implements a conflict-driven search via HS-DAG as described in Section 3.1. In contrast to our setup HS-DAGSAT, it however exploits a Horn-clause reasoning engine [Minoux, 1988] instead of a SAT-solver. [Peischl and Wotawa, 2003] described the diagnosis engine and initial results in more detail. It is worth noting that their approach is similar to the one in [Nayak and Williams, 1997].

Horn clauses are disjunctions of literals where only one may be positive. In our models, for an arbitrary component c ∈ COMP, NAB c represents the corresponding ¬AB(c) predicate. in c v and out c v for v ∈ {L,H} (with H referring to high/true/"1" and L to low/false/"0") refer to c's input/output holding value v. Note that in or out represent the connections between the components' ports, and we add for each input or output s a clause s c H ∧ s c L → ⊥ stating that a signal cannot be high and low at the same time. The propositional rules added for a circuit's gate X are as follows, where we start with those for a buffer:

NAB X ∧ in X H → out X H NAB X ∧ in X L→ out X L NAB X ∧ out X H → in X H

NAB X ∧ out X L → in X L

While an inverter is defined similarly, for XOR and XNOR gates with two inputs, we define all possible combinations of input and output values, resulting in the following rules for an XOR gate X:

NAB X ∧ in 1 X H ∧ in 2 X L→ out X H NAB X ∧ in 1 X L∧ in 2 X L→ out X L NAB X ∧ in 1 X H ∧ in 2 X H → out X L NAB X ∧ in 1 X L∧ in 2 X H → out X H NAB X ∧ out X H ∧ in 2 X L→ in 1 X H NAB X ∧ out X L∧ in 2 X L→ in 1 X L NAB X ∧ out X H ∧ in 2 X H → in 1 X L NAB X ∧ out X L∧ in 2 X H → in 1 X H NAB X ∧ out X H ∧ in 1 X L→ in 2 X H NAB X ∧ out X L∧ in 1 X L→ in 2 X L NAB X ∧ out X H ∧ in 1 X H → in 2 X L NAB X ∧ out X L∧ in 1 X H → in 2 X H

AND, OR, NAND and NOR gates may comprise more than two inputs. For example, the model of an AND gate X comprising k inputs is specified as:

2 http://www.ist.tugraz.at/modremas/downloads.html

NAB X ∧ ∧i∈1,...,k in i X H → out X H ∀i ∈ 1, . . . , k : NAB X ∧ in i X L → out X L ∀i ∈ 1, . . . , k : NAB X ∧ out X H → in i X H ∀K′ ⊂ K = {1, . . . , k} such that |K′ | = k - 1 : NAB X ∧ out X L∧ ∧i∈K′ in i X H → in j X L for j ∈ K \ K′

3.3 Computing Diagnoses via SAT directly

We selected two setups for computing diagnoses in the abnormal predicates with SAT solvers directly: (1) using a MAXSAT problem and (2) by introducing cardinality constraints in a "pure" SAT search approach.

MERIDIAN [Feldman et al., 2010] constructs a MAXSAT problem by maintaining a set of clause and weight pairs. While clauses forming SD are assigned weight ∞ (i.e., excluding them from the described partial MAX-SAT problem), each assumption ¬AB(c) is added with weight 1. The MAX-SAT solver is queried for solutions until the desired maximum cardinality has been exceeded or the solver returns UNSAT. In each step, a blocking clause for the previous solution is added, excluding it and its supersets from subsequent computations.

Implementing MERIDIAN's approach for our setup Direct-MSSAT, we exploit Yices' extended assertions, which can be used to state (partial) MAX-SAT problems:

Using Yices' (max-sat) command we obtain the maximum satisfiable subset in terms of abnormal predicates. The corresponding blocking clause for a diagnosis ∆ is encoded as (assert ¬∆).

Our second direct SAT setup Direct-CNSAT, is based on cardinality constraints (networks) as proposed in, for example, [E´en and S¨orensson, 2006; Metodi et al., 2012]. By adding a limit on the number of abnormal predicates activated simultaneously, a satisfying solution of

results in a diagnosis of cardinality k at most. Incrementing k from 1 to the maximal desired cardinality while blocking discovered solutions (and their supersets) like in the MAXSAT case, we obtain a pure SAT diagnosis algorithm.

A classical way to encode cardinality constraints in the Boolean domain is the use of sorting networks, e.g., OddEven Mergesort (OEMS) networks [Batcher, 1968]. The idea is to transform the summands ABi into a unary number (i.e. "sort" all the 1s to the left) and then add the clause ¬xk+1, where {xi|1 ≤ i ≤ COMP} are the sorted bits. As it is often the case that COMP ≫ k, we use an encoding tailored to this case, coined Cardinality Networks [As´ın et al., 2009]. Compared to OEMS networks, they require only O(n log2 k) clauses instead of O(n log2 n), where n is the number of inputs (i.e., |COMP| in our case). Like [Metodi et al., 2012] we use SCryptoMinisat 3 , a SAT solver capable of returning all (or multiple) solutions to a given instance (unfortunately there is no MAX-SAT functionality). Thus unlike Direct-MSSAT, with Direct-CNSAT we obtain all the diagnoses for a specific cardinality by one query to the reasoning engine.

3 http://amit.metodi.me/research/scrypto/

3.4 Direct Constraint Solver-based Computation

Our setup Direct-MSCS is based on the ConDiag algorithm as proposed by [Nica and Wotawa, 2012]. This setup encodes a MAX-SAT problem via constraints and uses the MINION constraint solver as underlying engine for exploring theories.

Like our Direct-CNSAT setup, a single query to the solver delivers all solutions of a specified cardinality. Thus, within a loop incrementing the maximum cardinality from 1 to n, all diagnoses for some i ≤ n are derived with a single MINION call. Each solution is stored and the constraints for the corresponding blocking clause are attached to the model.

Obviously, constraints offer more flexibility regarding model-descriptions, which makes the encoding concept even more important. For instance, describing logic gates via value combination tables proved to be significantly slower than encoding them via single solver commands. For our problem domain of Boolean circuits (see Section 4), Christopher Jefferson and Peter Nightingale, two main developers behind MINION, suggested to us the encoding given in Table 1 4 .

Considering Reiter's diagnosis formulations and the various gate types, with Table 1 offering the nominal behavior for Boolean gates, we add for each gate j a constraint reifyimply(NominalBehavior , !AB[j]) with AB a vector defining each gate j's status abnormal (AB[j] = 1) or not (AB[j] = 0). While observations are encoded straightforward via eq(variable, value), the desired diagnosis cardinality is defined via sumleq(AB, i) and sumgeq(AB, i), requiring the sum of abnormal components to be equal to i.

4 Empirical Results

Like [Siddiqi, 2011] we used ten combinational circuits from the well-known ISCAS85 benchmark suite 5 for our tests, run on an Apple MacPro4,1 (early 2009) computer featuring a 2.66 GHz Intel Xeon W3520 quad-core processor, 16GiB of RAM and running an up-to-date version of OS X 10.8. The algorithms were implemented in Java 1.6 (HS-DAGHC and Direct-MSCS) and CPython 2.7 (HS-DAGSAT, HSTSAT, Direct-MSSAT and Direct-CNSAT), while for the theorem provers we used MINION 0.15, Yices 1.0.29 and SCryptoMinisat (29/01/2012) based on CryptoMiniSat 2.5.1.

4 For details on the solver specific constraints please refer to MINION's documentation http://minion.sourceforge.net/htmlhelp

5 http://www.cbl.ncsu.edu:16080/benchmarks/ISCAS85/

It is worth noting that, due to the underlying complexity, the ISCAS85 circuits provide a profound base for experiments, so that, e.g., [Wang and Provan, 2008] perused the ISCAS85 structure to develop a more general benchmark suite for diagnosis. In Table 2, we list circuit details, including the number of inputs/outputs/gates as well as their function ranging from Arithmetic Logic Units (ALUs), via interrupt controllers, adders/comparators and multipliers to single-error correction/double-error detection (SEC/DED) circuits.

Into each circuit, we randomly injected ten single-, doubleand triple-faults, aggregating test suites TS1, TS2 and TS3 respectively. We injected faults by changing a gate's Boolean function such that at least one circuit output flipped. When modifying the second and third gate, we allowed only previously unaffected outputs to flip, in order to avoid faults from masking each other. Injected faults were verified to be indeed a minimal diagnosis.

The measured run-time for deriving diagnoses up to the cardinality of the injected fault represents the total, userexperienced time, including the communication with the solvers. All algorithms faced a 200 seconds run-time limit. For HS-DAGHC we further set a limit of 100 diagnoses (whose computation always exceeded 200 seconds) as a precaution.

For Figure 1, we ordered all samples from TS1 to TS3 according to their run-time, and report the amount of samples solved for growing cumulative time. The amount of completed samples per test suite and setup is given in Table 3. In Table 4 we present from top to bottom the run-times for computing single-fault diagnoses for TS1, up to double-fault ones for TS2 and diagnoses up to a size of three for TS3. For clarity, we put the best values per category and circuit in bold face. Note that we did not include any results from samples that timed out in our tables and figures. While this leads to missing entries in Table 4, we report the minimal and median values whenever available.

Specifically in the context that we did not exploit modeloptimization concepts like cones of influence, considering Table 4 suggests that any algorithm offers attractive performance when focusing on single-fault diagnoses for these circuits. HS-DAGHC and Direct-MSCS match each other for the crown, where like all other approaches, the latter has the disadvantage of relying on an external reasoning engine. While HS-DAGHC outperformed the others for very small singlefault samples, as evident also in Figure 1, it couldn't complete quite many samples (even some of TS1, see also Table 3), so that Direct-MSCS becomes even more interesting.

The other two conflict driven setups, HS-DAGSAT and HSTSAT, performed similarly for all test suites (see Table 4) with a slight advantage for the first (see Figure 1), which could also solve slightly more samples (see Table 3). It is beaten, however, specifically in the completion rate, by the best performing direct SAT setup Direct-MSCS.

Between the two direct SAT setups Direct-CNSAT and Direct-MSSAT, the first is superior (best seen in Figure 1 and Table 3). Due to internal tests with a Direct-CNSAT version computing a single solution per query, we can state that a large (but varying) part of the advantage comes from the fewer amount of theorem prover calls related to the internal loop in SCryptoMinisat used by Direct-CNSAT. Future tests will delve into the encountered run-time differences.

Regarding a comparison of Direct-MSCS using a constraint solver and the best direct SAT setup Direct-CNSAT, we see some advantages for the first for TS1, which changes with higher maximum cardinalities for TS2 and TS3. Presumably due to better performance for larger samples, Direct-CNSAT completes more samples within the given time limit (see Figure 1 and Table 3). While this might suggest better scalability for the SAT-based setup, we do assume this to be very domain-dependent. That is, for more complex modeling domains, this might actually be different.

Considering our tests with Direct-CNSAT being the topperformer, at least for some domains, conflict-driven search as used in many classic approaches seems not to offer significant advantages against direct setups anymore.

5 Conclusions &FutureWork

In this paper, we reviewed two generic search strategies adopted in diagnosis approaches, i.e. conflict-driven search and the direct computation of diagnoses. Several setups implementing one or the other strategy perusing varying solvers were used to identify corresponding performance trends.

In our tests, conflict-driven search did not offer significant advantages against setups that derive diagnoses directly, i.e. brute force search focused via blocking clauses/constraints. Surprisingly, the direct setups even set the pace (excluding HS-DAGHC that had advantages for small samples due to its internal reasoning engine). Avoiding the maintenance of a tree/DAG for encoding the search by attaching blocking clauses/constraints (excluding solutions and their supersets from further consideration) to the model, seems to be a competitive strategy with the performance of today's generalpurpose reasoning engines. This is complemented by minimal implementation efforts as well as enhanced robustness due to the simplistic algorithm/code.

The answer to our question whether general-purpose solvers can be used for an efficient diagnosis thus seems to be an affirmative one, considering our tests. For many projects one might consider direct setups against specifically tailored conflict-driven engines. While their general performance is attractive, in our optimization process we also saw that the interface plays a significant role (e.g. whether one can exploit an internal loop for constructing multiple solutions).

An interesting question in the scope of direct setups is the choice of the underlying engine. While our top-performing SAT setup offered, on average, slight performance advantages against our constraint-solver setup, we would like to note two things. First, the other SAT setup was often outperformed by the constraint-solver setup, and second, we expect a comparison to be domain-dependent. That is, for model domains more complex than the Boolean one of our circuits, future research will have to identify corresponding trends. Also the evolvement of SAT and constraint solvers as best observed in corresponding competitions will influence this choice. Future work will also aim at trends for strong fault mode diagnosis with behavioral modes [de Kleer and Williams, 1989].

Acknowledgments

Parts of this work have been supported by the Austrian Science Fund (FWF): P22959-N23 ("MoDiaForTed") and by the FFG: BRIDGE project 824913 ("SIMOA").