Abductive inference provides consistent explanations for observable e ects and has been of special interest in the context of diagnosis. The abduction problem is in general NP-hard, thus, there is a high motivation to derive solutions e ciently for practical instances. In this paper, we focus on propositional abduction in the framework of model-based diagnosis. We review four algorithms to compute explanations: one employs an ATMS to derive diagnoses and the others are con ict-directed methods based on an unsatis able reformulation of the abductive system description. In an empirical evaluation we compare the di erent approaches on practical examples. Our experiments indicate that the ATMS provides the best performance results for the majority of problems.
Abductive inference, as a form of non-monotonic reasoning, attempts to derive a set of causes which best explain an e ect. Within this paper we focus on logic-based abduction, which is formulated as nding a consistent set of hypotheses implying a given observation together with the background knowledge. A variety of approaches, such as consequence nding [Marquis, 2000] or prooftree completion [McIlraith, 1998], have been proposed as methods for mechanizing abductive reasoning and lead to the development of several systems, e.g. DART [Genesereth, 1984] or Theorist [Poole et al., 1987]. In the context of logic programming, abductive logic programming [Kakas et al., 1992] emerged aiming at providing a framework and set of techniques for performing abductive reasoning [Denecker and De Schreye, 1998; Van Nu elen, 2001]. It is well known that abduction is in general an NP-hard problem with potentially an exponential number of solutions [Bylander et al., 1991]. Thus, there is a demand to compute abductive explanations e ciently for instances of practical size and complexity.
Authors are listed in alphabetical order.
Even though abduction has been performed in the context of various tasks [Denecker and Kakas, 2002], such as planning [Poole and Kanazawa, 1994] or natural language processing [Ovchinnikova et al., 2014], its prevalent application is in diagnosis. Model-based diagnosis has been proposed as an improvement to fault localization and relies on a formal system description encompassing structural as well as behavioral knowledge of the physical artifact. Within the last decades an extensive body of research has distinguished two logical de nitions: consistency-based and abductive diagnosis. Consistency-based diagnosis relies on a formalization of the correct system response and identi es failures through inconsistency [Reiter, 1987]. In contrast, the abductive approach employs models of faulty behavior to reason from symptoms to causes and is based on a stricter criteria as it nds consistent explanations entailing the observations [Console et al., 1991]. Abductive model-based diagnosis has been applied, e.g., to environmental decision support systems [Wotawa et al., 2009].
The computation of explanations has not only been studied in the context of diagnosis, but also has received attention in the eld of constraint satisfaction problems and infeasibility analysis. Junker [2004] describes an algorithm generating preferred explanations for overconstrained systems. By employing a divide and conquer strategy, con icting constraints can be e ciently computed. These contradictions essentially constitute the causes for the unsatis ability of the system. Within the eld of infeasibility analysis, con icts refer to Minimal Unsatis able Subsets (MUSes). Recently, Li ton et al. [2015] present a direct MUSes approach which exploits the power-set lattice. Many algorithms for computing unsatis able cores, however, do not generate them directly, but rely on their hitting set dual Minimal Correction Subsets (MCSes). Li ton and Sakallah [2008] propose the CAMUS algorithm utilizing this hitting set duality to produce MUSes by rst computing all MCSes.
In this paper, we investigate approaches to computing explanations in the framework of abductive modelbased diagnosis. In particular, we examine one direct proof method by exploiting an assumption-based truth maintenance system (ATMS) to infer consistent diagnoses. The other techniques utilize the unsatis ability of a rewritten system description to derive explanations. The rst algorithm determines con icts based on a hitting set directed acyclic graph (HS-DAG), while the two remaining rely on MUSes and MCSes computation.
The remainder of this paper is structured as follows. Section 2 introduces the theoretical foundations of abductive model-based diagnosis and further provides definitions in the context of unsatis able formulas. Subsequently, we describe the selected algorithms and tools. In Section 4 we present the set-up and results of an empirical evaluation, followed by our conclusions. 2
In this section we de ne the Propositional Horn Clause Abductions Problem, which functions as the basis of our research. Subsequently, we discuss certain subsets of unsatis able formulas and show their connection to abductive diagnosis. 2.1
Abductive inference, in the context of formal logic, can be de ned as the search for a set of hypotheses which entail the observations, while being consistent in conjunction with the background theory. Model-based diagnosis builds upon a formalization of the system behavior. Thus, abductive model-based diagnosis requires a description of the system response in the presence of a fault in order to compute causes entailing symptoms.
In general logic-based abduction is an intractable problem, however, there exist certain subsets, such as de nite propositional Horn theories, where abduction is polynomial [Eiter and Gottlob, 1995; Nordh and Zanuttini, 2008]. We draw on these ndings and focus in our research on propositional logic. Note that the following de nitions are similar to the ones by Friedrich et al. [1990].
base (KB) is a tuple (A,Hyp,Th) where A denotes the set of propositional variables, Hyp A the set of hypotheses, and Th the set of Horn clause sentences over A.
The set of hypotheses contains the propositions which can either be assumed true or false and refer to possible causes. In order to form an abduction problem, in particular a Propositional Horn Clause Abduction Problem, we consider in addition to the knowledge base a set of observations for which explanations are to be computed. De nition 2 (Propositional Horn Clause Abduction Problem (PHCAP)) Given a knowledge base (A,Hyp,Th) and a set of observations Obs A then the tuple (A,Hyp,Th,Obs) forms a Propositional Horn Clause Abduction Problem (PHCAP).
Given a PHCAP (A,Hyp,Th,Obs). A set Hyp is a solution if and only if [ Th j= Obs and [ Th 6j= ?. A solution is parsimonious or minimal if and only if no set 0 is a solution.
A solution to the PHCAP constitutes an abductive diagnosis as it comprises the set of hypotheses explaining the observations.
Example 1: Consider the simpli ed example of a converter KB of an industrial wind turbine.
Hyp =
mode(F an; Corrosion); mode(F an; T M F ); mode(IGBT; HCF ) A =
mode(F an; T M F ); mode(IGBT; HCF ) 8 mode(F an; Corrosion) ! P turbine; 9 T h = >< mode(F an; T M F ) ! P turbine; >= mode(IGBT; HCF ) ! T nacelle; >: mode(IGBT; HCF ) ! P turbine ;>
Let us assume an increased temperature in the nacelle (T nacelle) and a lower than expected power output (P turbine) can be observed, i.e. Obs = fT nacelle; P turbineg. Thus, the solution to the PHCAP is 1 = fmode(IGBT; HCF )g.
To compute the abductive explanations for an observed e ect, one can check all subsets of hypotheses to determine whether they entail the observations or not. This approach, however, is computationally expensive and therefore not applicable in a practical setting. 2.2
We assume standard de nitions for propositional logic throughout this section [Chang and Lee, 1973]. If a propositional formula in CNF is unsatis able, there are subsets which are of special interest in the context of abduction. In this section we de ne said sets rst and then examine how they can be used for abductive diagnosis. The subsequent de nitions are taken from Li ton and Sakallah [2008].
A Minimal Unsatis able Subset (MUS) contains a subset of clauses which cannot be satis ed simultaneously. De nition 4 (Minimal Unsatis able Subset (MUS)) A subset U is an MUS if U is unsatis able and 8Ci 2 U; U n (fCig) is satis able.
Notice that every proper subset of an MUS is satis able. Its hitting set dual, Minimal Correction Subset (MCS), comprises clauses that correct the unsatis able formula when removed [Birnbaum and Lozinskii, 2003]. De nition 5 (Minimal Correction Subset (MCS)) A subset M is an MCS if n M is satis able and 8Ci 2 M; n (M n fCig) is unsatis able. Since removing an MCS results in a feasible formula, any MCS is the complement of some Maximal Satis able Subset (MSS), which is a generalization of a solution to the MAX-SAT problem.
De nition 6 (Maximal Satis able Subset (MSS)) A subset S is an MSS if S is satis able and 8Ci 2 n S; S [ fCig) is unsatis able.
Example 2: Consider the unsatis able formula in CNF.
C1
C2
C3
C4 = (z:a _}:|b _ c{) ^ (z:c}_| d{) ^ z(}c|){ ^ (z:}|d{) The combination of clauses C2; C3 and C4 results in being unsatis able, hence the unsatis able cores are
MUSes( ) = ffC2; C3; C4gg: Via hitting set computation we derive the following set of MCSes:
MCSes( ) = ffC2g; fC3g; fC4gg: Removing any MCS from results in the formula being satis able. Subsequently, we can compute the Maximal Satis able Subsets (MSSes) by forming the complements:
MSSes( ) = ffC1; C3; C4g; fC1; C2; C4g; fC1; C2; C3gg: As aforementioned, the MUSes correspond to the explanations of an over-constrained system [Junker, 2004]. In order to generate abductive explanations on basis of unsatis able formulae, we recast the rst condition of De nition 3 of an abductive explanation from [ T h j= Obs to T h [ [ f:Obsg j= ? by logical equivalence. f:Obsg consists of the complement of each observation in Obs, i.e. 8o 2 Obs : :o 2 f:Obsg. Thus, computing the abductive explanations is reformulated as the search for a refutation proof comprising propositions from Hyp [McIlraith, 1998]. In other words, we can restate the problem of computing diagnoses to nding the con ict sets of T h ^ Hyp ^ f:Obsg which by de nition are equivalent to the MUSes of said formula.
Naturally, MUSes contains several unsatis able subsets irrelevant for the diagnostic task. Since we are solely interested in minimal explanations, we dismiss certain subsets and parts of MUSes. We rst eliminate all propositions not corresponding to hypotheses. The resulting solution may contain supersets of diagnoses, which we subsequently remove to derive minimal explanations. We refer to MUSes corresponding to parsimonious abductive diagnoses as M U SesHyp. 3
In the following, we depict our four approaches to abductive diagnosis based on a propositional logic model. For each method, we give a brief description of the underlying notion for deriving explanations and subsequently discuss speci c tools and algorithms included in the empirical evaluation. 3.1
De Kleer's [1986a] ATMS has been recognized as a general abduction engine for propositional Horn clause sentences [Levesque, 1989]. An ATMS exploits a graph representation of the theory, where hypotheses, observations, and contradiction are vertices. The edges are determined by the implications of the underlying Horn clauses. By assigning a label to each node, the ATMS keeps track of the hypotheses from which each vertex can be inferred from. Speci cally, a label is a set of sets of hypotheses. Whenever a new rule is applied to the ATMS, the nodes' labels are updated, consistency is ensured, and valid explanations for a given e ect can be directly determined. Notice that the labels can grow exponentially in the number of assumptions [de Kleer, 1986b].
Wotawa et al. [2009] propose Algorithm abductiveExplanations, which computes abductive diagnoses for a given PHCAP by exploiting an ATMS. After passing the Horn clauses composing the theory to the ATMS, a single implication is added: o1 ^o2^: : :^on ! obs, where fo1; o2; : : : ; ong correspond to the observations and obs denotes a new proposition not yet considered in A. The label of obs comprises all hypotheses which inferred the observations, thus constitute the solutions to the PHCAP. Since the ATMS terminates due to a nite number Algorithm 1 abductiveExplanations [Wotawa et al., 2009] procedure abductiveExplanations (A; Hyp; T h; Obs) Add T h to AT M S Add Vo2Obs o ! obs to AT M S return the label of obs end procedure . obs 2= A of hypotheses, the Algorithm abductiveExplanations is guaranteed to halt as well. We utilized a Java implementation of abductiveExplanations for our empirical evaluation. 3.2
By detecting a discrepancy between the predicted and actual behavior, i.e. a con ict, Reiter [1987] derived consistency-based diagnoses via minimal hitting set computation. A con ict arises when, under the assumption all components are behaving correctly, an observation is inconsistent with the expected performance. Thus, con icts correspond to hypotheses contradicting observations. By rewriting the abductive model, as noted in Section 2.2, we can derive con icts which constitute abductive diagnoses.
Reiter's approach maintains a tree to compute all minimal hitting sets based on con icts. These con icts can be generated on demand by applying a theorem prover, which returns a refutation involving hypotheses if one exists. Starting from an initial con ict set as root node, the tree is iteratively extended in a breadth rst manner. At each node n, labeled with con ict C, an outgoing edge h(n) is generated for each c 2 C. Each edge label is checked for consistency. In case it is consistent the corresponding node determines a leaf and thus a minimal hitting set, otherwise a new con ict set is derived, such that it is disjoint to the current set of edge labels. Several pruning techniques ensure the minimality of the hitting sets and allow the use of non minimal con icts. Greiner et al. [1989] corrected some inadequacies of Reiter's algorithm and devised an approach performing on a directed acyclic graph (DAG) instead of a tree.
Algorithm hsdagAB is based on HS-DAG and a theorem prover to derive con icts and subsequently minimal abductive explanations. Given a PHCAP, we generate an implication with a conjunction of observations on the left hand side and the contradiction on the right hand side, i.e. o1 ^o2 ^: : :^on ! ?. The theory T h, the implication, and the theorem prover, represented by T P , are supplied to HS-DAG. CON F corresponds to the set of con icts obtained from the hitting set algorithm. Note that these con icts are not ensured to be minimal; thus, we remove all supersets afterwards.
procedure hsdagAB(A; Hyp; T h; Obs)
T P SeTt;hC[ONVFo2Obs;o ! ? CON F HS-DAG(TP) for all c 2 CON F do if 6 9c0 2 CON F : c0 c then
Set c end if end for return end procedure
Set . Theorem Prover . HS-DAG
For our evaluation we utilized the publicly available diagnosis engine JDiagengine1 which implements a con ict-driven search via HS-DAG [Peischl and Wotawa, 2003] exploiting a Horn clause theorem prover [Minoux, 1988]. JDiagengine as well as hsdagAB are Java implementations. 3.3
In Section 2.2 we examined the relation between MUSes and abductive diagnoses. By rewriting the model to an unsatis able formula, the abduction problem consists in computing the sets of hypotheses which are responsible for the infeasibility, i.e. M U SesHyp.
Algorithm musAB employs a MUS enumeration procedure and thereon computes the minimal abductive diagnoses, denoted M U SesHyp. We create an unsatis able CNF encoding of the problem denoted . Since T h consists of Horn clauses, we can easily convert it into a CNF representation, which we refer to as T . For each h 2 Hyp, we create a single clause assuming h to be true. Additionally, we generate a disjunction containing the negated observations, i.e. :o1 _ :o2 _ : : : _ :on.
Example 1 (cont.): Consider again our running example of the converter. Let be the unsatis able CNF representation of the abduction problem:
C1 : :mode(F an; Corrosion) _ P turbine C2 : :mode(F an; T M F ) _ P turbine C3 : :mode(IGBT; HCF ) _ P turbine C4 : :mode(IGBT; HCF ) _ T nacelle
C6 : mode(F an; T M F )
1http://www.ist.tugraz.at/modremas/index.html
procedure musAB(A; Hyp; T h; Obs)
M U Ses; Set ;
T [ Hyp [ Wo2Obs :o M U Ses MUSes( ) . MUS enumeration algorithm for all m 2 M U Ses do
M m \ Hyp end for for all u 2 M do if 6 9u0 2 M : u0 u then
end if end for return Set M U SesHyp end procedure
C8 : :T nacelle _ :P turbine Clauses C1 to C4 refer to T , C5 to C7 to the set Hyp and clause C8 contains the negation of the set of observations. We obtain the following MUSes from :
M U Ses = fC3; C4; C7; C8g ; fC1; C3; C5; C7; C8g ;
fC2; C3; C6; C7; C8g Since we are only interested in the abducibles, we remove all clauses not associated with hypotheses. Let M be the resulting set:
M = fC7g ; fC5; C7g ; fC6; C7g
Eliminating all supersets we obtain M U SesHyp = ffC7gg : Hence the abductive diagnosis is 1 = fmode(IGBT; HCF )g.
We implemented musAB in Java and employed the MUS enumeration tool MARCO2 [Li ton et al., 2015]. MARCO computes MUSes and MSSes based on an exploration of the power-set lattice. Given an unsatis able clause set, all of its supersets are unsatis able as well; thus, an MUS de nes a "low point" in an infeasible region. Similarly, an MSS characterizes a "high point" in a satis able region. In each iteration MARCO investigates an unexplored part of the lattice and traverses through the power-set until either an MUS or an MSS is found. MARCO is implemented in Python using MUSer23 and MiniSat4. Many MUS enumeration algorithms refrain from computing the unsatis able cores directly, but exploit its hitting set dual MCS, since nding satis able subsets is an NP-complete problem, whereas UNSAT resides in CoNP [Li ton and Sakallah, 2008]. Therefore, we examine an indirect approach, which rst computes the MCSes and then determines the MUSes [Koitz and Wotawa, 2015b]. In the case of diagnosis we are only interested in the hypotheses, which have been used to derive a con ict. Thus, for further computation we select MCS which only contain clauses referring to explanations. We create the 2http://sun.iwu.edu/ mli to/marco/ 3http://logos.ucd.ie/wiki/doku.php?id=muser 4http://minisat.se/ set M CSesHyp such that 8m 2 M CSesHyp : m Hyp. This has two practical consequences: it reduces the number of sets to be considered by the hitting set algorithm and the corresponding MUSes derived from M CSesHyp already constitute the abductive diagnoses.
Algorithm satAB computes the set of abductive diagnoses for a given PHCAP based on an MCS enumeration algorithm. Note that the unsatis able model is the same as in the direct MUS approach.
procedure satAB (A; Hyp; T h; Obs)
M CSes; M CSesHyp ;
T [ Hyp [ Wo2Obs :o M CSes MCSes( ) . MCS enumeration algorithm for all m 2 M CSes do if m Hyp and m [ T h is consistent then
M CSesHyp m [ M CSesHyp end if end for
Set MHS(M CSesHyp) . Minimal hitting set algorithm
return Set end procedure
Example 1 (cont.): Computing the M CSes of obtain:
M CSes =
fC3g ; fC7g ; fC8g ; fC4; C5; C6g ; fC2; C4; C5g ; fC1; C4; C6g ; fC1; C2; C4g we :
Extracting the MCSes, which only contain clauses from Hyp and are consistent with regard to the theory, results in M CSesHyp = ffC7gg. By computing the hitting set of M CSesHyp, we obtain the set of MUSes solely referring to explanations, which are in fact the set of abductive diagnoses. In our example 1 = fmode(IGBT; HCF )g.
For our evaluation we implemented satAB in Java and
utilized the MCSLS5 tool by Marques-Silva et al. [2013]
as the MCS computation procedure . MCSLS is written
in C++, employs MiniSat6, and provides the
possibility to apply several MCS enumeration algorithms. We
5http://logos.ucd.ie/web/doku.php?id=mcsls
6http://minisat.se/
decided for the CLD approach of MCSLS, which takes
advantage of disjoint unsatis able cores. Regarding the
hitting set computation, we engaged a Java
implementation of the Binary Hitting Set Tree algorithm [
In this section, we describe our empirical evaluation setup and report on the obtained results. All the numbers presented in this section were obtained from a Lenovo ThinkPad T540p Intel Core i7-4700MQ processor (2.60 GHz) with 8 GB RAM running Ubunutu 14.04 (64-bit).
We generated propositional Horn models from several Failure Mode E ect Analyses covering various technical systems by utilizing a mapping function. A detailed description of the conversion process can be found in Wotawa [2014] and Koitz and Wotawa [2015a]. Table 2 provides an overview of the models' structure as well as some characteristics of the problem instances. It is worth noting that the system descriptions vary in the number of hypotheses (Hyp), possible observables (Obs), and implications (Th). Due to theory comprising Horn clauses, a conversion into a CNF representation, suitable for the MUS-based and MCS-based computation, is straightforward.
In the experiments, we computed the abductive explanations for jObsj from one to the maximum number of e ects possible. The observations were generated randomly; however, the same set was used for all algorithms. The results reported in Table 1 have been obtained from ten trials and all algorithms faced a 200 seconds runtime limit.
To compare the algorithms, we only measured the time to compute minimal diagnoses, i.e. we disregarded the mapping, model conversion, as well as the time it required to communicate with the solvers. In case of musAB and satAB we parsed the execution time measured by the tools themselves, which was available in the output.
Note that for certain instances hsdagAB, satAB and musAB exceeded the prede ned runtime threshold, which we marked with T in the table. Thus, for the cumulative runtimes, shown in Figure 1, we utilized the maximum of 200 seconds in cases the limit was surpassed.
Whereas some of the small runtimes are arguable due to the measurement in the milliseconds range, Table 1 as well as Figure 1 reveal that abductiveExplanations (Mean = 2.41 ms, SD = 12.36 ms, Median = 0 ms) outperforms hsdagAB (Mean = 12261.77 ms, SD = 3162.5 ms, Median = 1 ms), satAB (Mean = 1741.39 ms, SD = 15633.06 ms, Median = 1 ms), and musAB (Mean = 45947.85 ms, SD = 82289.36 ms, Median = 118 ms). Unsurprisingly, the larger considered examples are more computationally demanding, especially with the model of the electrical circuit featuring a larger set of possible hypotheses and diagnoses.
In cases where the maximum cardinality of the diagnoses is limited, HS-DAG computes solutions rather efciently. However, in our examples, we enumerated all solutions, thus neither the size nor the number of hitting sets was restricted, which can result in some cases in an extensive graph.
The MCS-based approach performs rather poorly on the example of the converter. According to MarquesSilva et al. [2013] the number of SAT calls for the CLD approach depends on the size of the underlying formula, which in our case is determined by the size of the theory and the number of hypotheses, which explains the computation time for the inverter example. It is worth
MIN < 1 < 1 < 1 < 1 < 1 < 1 < 1 < 1 < 1 < 1 < 1 < 1
MIN 8 7 7 11 7 7 7 7 8 8 7 8 mentioning that in the majority of cases the hitting set computation accounted for a negligible fraction of the total runtime of satAB.
The performance of MARCO is very much dependent on the traversal of the graph towards a "low point" or "high point" in the power-set lattice, i.e. MUS or MSS, respectively. Thus, the number of clauses, which shape the power lattice, in uences the MARCO's runtime. Therefore, in particular the larger instances require more computation time.
Note that we did not focus on an e cient encoding or any kind of pre-compilation to speed up the reasoning process. Further, in the case of MUS- and MCS-based algorithms, there is no focus on the abducibles, as for the ATMS and the HS-DAG. Thus, a large number of sets is generated, which are not of interest for the diagnostic task. 5
Abductive reasoning is of special interest in the context of diagnosis. In this paper we focused on the modelbased approach utilizing a logic system description. We reviewed four di erent algorithms to compute abductive explanations for a propositional diagnosis problem. On the one hand, we investigated a direct strategy based on an ATMS, and on the other hand examined three approaches relying on con ict computation of an unsatis able model. In our tests, the con ict-based methods did not o er advantages against the ATMS. The SAT-based approaches have the drawback of not being focused on the set of abducibles, but rather enumerate all sets regardless if the clause corresponds to a hypothesis or not. Further, we could observe that in fact MCS enumeration and subsequent hitting set computation is preferable to the direct MUS approach. Surprisingly, HS-DAG did not perform well even on the smaller examples. We explain this, by the encoding of the problem, which has not been ideal for utilized theorem prover.
The work presented in this paper has been supported by the FFG project Applied Model Based Reasoning (AMOR) under grant 842407. We would further like to express our gratitude to our industrial partner, Uptime Engineering GmbH.