In classical hitting set algorithms for ModelBased Diagnosis (MBD) that use on-demand conflict generation, a single conflict is computed whenever needed during tree construction. Since such a strategy leads to a full “restart” of the conflict-generation algorithm on each call, we propose a divide-and-conquer algorithm called MERGEXPLAIN which efficiently searches for multiple conflicts during a single call. The design of the algorithm aims at scenarios in which the goal is to find a few leading diagnoses and the algorithm can - due to its non-intrusive design - be used in combination with various underlying reasoners (theorem provers). An empirical evaluation on different sets of benchmark problems shows that our proposed algorithm can lead to significant reductions of the required diagnosis times when compared to a “one-conflict-ata-time” strategy.
In Model-Based Diagnosis (MBD), the concept of conflicts describes parts of a system which – given a set of observations – cannot all work correctly. Besides MBD, the calculation of minimal conflicts is a central task in a number of other AI approaches [1]. Reiter [2] showed that the minimal hitting sets of conflicts correspond to diagnoses, where a diagnosis is a possible explanation why a system’s observed behavior differs from its expected behavior. He used this property for the computation of diagnoses in the breadthfirst hitting set tree (HS-tree) diagnosis algorithm.
Over time, the principle of this MBD approach was used for a number of different diagnosis problems such as electronic circuits, hardware descriptions in VHDL, program specifications, ontologies, and knowledge-based systems[3; 4; 5; 6; 7]. A reason for the broad utilization of hitting set approaches is that its principle does not depend on the underlying knowledge representation and reasoning technique, because only a general Theorem Prover (TP) – a component that returns conflicts – is needed.
The implementation of a TP can be done in different ways. First, the conflict detection can be implemented as a reasoning task, e.g., by modifying a consistency checking algorithm [8; 9]. Second, “non-intrusive” conflict detection techniques can be used with a variety of reasoning approaches, since they require only a very limited reasoning functionality like consistency or entailment checking without knowing the internals of the reasoning algorithm. Such methods can benefit from the newest improvements in reasoning algorithms, such as incremental solving, heuristics, learning strategies, etc., without any modifications.
A non-intrusive conflict detection algorithm which has
shown to be very efficient in different application
scenarios is Junker’s QUICKXPLAIN [
In many classical hitting set based approaches, conflicts
are computed individually with QXP during HS-tree
construction when they are required, as in many domains not
all conflicts are known in advance [
In this paper, we propose MERGEXPLAIN (MXP for short), a divide-and-conquer algorithm which searches for multiple conflicts during a single decomposition run. Our method is built upon QXP and is therefore also nonintrusive. The basic idea behind MXP is that (a) the early identification of multiple conflicts can speed up the overall diagnosis process, e.g., due to better conflict “reuses” [2], and that (b) we can identify additional conflicts faster when we decompose the original components into smaller subsets with the divide-and-conquer strategy of MXP.
The paper is organized as follows. After a problem characterization in Section 2, we present the details of MXP in Section 3 and discuss the properties of the algorithm. Section 4 presents the results of an extensive empirical evaluation using various diagnosis benchmark problems. Previous work is finally discussed in Section 5. 2 2.1
We use the definitions of[2] to characterize a system, diagnoses, and conflicts.
Definition 1 (System). A system is a pair (SD, COMPS) where SD is a system description (a set of logical sentences) and COMPS represents the system’s components (a finite set of constants). A diagnosis problem arises when a set of logical sentences OBS, called observations, is inconsistent with the normal behavior of the system (SD, COMPS). The correct behavior is represented in SD with an “abnormal” predicate AB/1. That is, for any component ci ∈ COMPS the literal ¬AB(ci) represents the assumption that the component ci behaves correctly.
Definition 2 (Diagnosis). Given a diagnosis problem (SD, COMPS, OBS), a diagnosis is a minimal set Δ ⊆ COMPS such that SD ∪ OBS ∪ {AB(c)|c ∈ Δ} ∪ {¬AB(c)|c ∈ COMPS\Δ} is consistent.
A diagnosis therefore corresponds to a minimal subset of the system components which, if assumed to be faulty (and thus behave abnormally) explain the system’s behavior, i.e., are consistent with the observations.
Two general classes of MBD algorithms exist. One relies on direct problem encodings and the aim is often to find one diagnosis quickly, see [12; 13; 14]. The other class relies on the computation of conflicts and their hitting sets (see next section). Such diagnosis algorithms are often used when the goal is to findmultiple or all minimal diagnoses. In the context of our work, techniques of the second class can immediately profit when the conflict generation process is done more efficiently. 2.2
Finding all minimal diagnoses corresponds to finding all minimal hitting sets (HS) of all existing conflicts [2]. Definition 3 (Conflict) . A conflict CS for (SD, COMPS, OBS) is a set {c1, . . . , ck} ⊆ COMPS such that SD ∪ OBS ∪{¬AB(ci) | ci ∈ CS } is inconsistent.
Assuming that all components of a conflict work correctly therefore contradicts the observations. A conflict CS is minimal, if no proper subset of CS is also a conflict.
To find the set ofall minimal diagnoses for a given
problem, [2] proposed a breadth-first HS-tree algorithm with tree
pruning and conflict reuse. A correction to this algorithm
was proposed by Greiner et al. which uses a directed acyclic
graph (DAG) instead of the tree to correctly deal with
nonminimal conflicts [
QXP was developed in the context of inconsistent constraint
satisfaction problems (CSPs) and the computation of
explanations. E.g., in case of an overconstrained CSP, the
problem consists in determining a minimal set of constraints
which causes the CSP to become unsolvable for the given
inputs. A simplified version of QXP [
Input: B: background theory, C: the set of possibly faulty constraints
Output: A minimal conflict CS ⊆ C
1 if isConsistent(B ∪ C) then return ‘no conflict’;
2 else if C = ∅ then return ∅;
3 return GETCONFLICT(B, B, C)
function GETCONFLICT (B, D, C)
if D 6= ∅ ∧ ¬ isConsistent(B) then return ∅;
if |C| = 1 then return C;
Split C into disjoint, non-empty sets C1 and C2
D2 ← GETCONFLICT (B ∪ C1, C1, C2)
D1 ← GETCONFLICT (B ∪ D2, D2, C1)
return D1 ∪ D2
Theorem 1 ([
Assume that MBD is applied to find an error in the
definition of a CSP. The CSP comprises the set of possibly faulty
constraints C. These are the elements of COMPS. The
system description SD corresponds to the semantics of the
constraints in C. Finally, the observations OBS are encoded as
unary constraints and are added to the background theory
B. During the HS-tree construction, QXP is called
whenever a new node is created and no conflict reuse is
possible. As a result, QXP can either return one minimal conflict ,
which can be used to label the new node, or return ’no
conflict’, which would mean that a diagnosis is found at the tree
node. Note that QXP can be used with other algorithms,
e.g., preference-based search [
3.1
The pseudo-code of MXP, which unlike QXP can return
multiple conflicts at a time, is given in Algorithm 2. MXP,
like QXP, is generally applicable to a variety of problem
domains. The mapping to the terminology used in MBD (SD,
COMPS, OBS) is straightforward as discussed in the previous
section. In the following, we will use the notation and
symbols from [
Note that there are applications of MBD in which the function isConsistent has to be “overwritten” to take the specifics of the underlying knowledge representation and reasoning system into account. The ontology debugging approach presented in [7] for example extends isConsistent with the verification of entailments of a logical theory. MXP can be used in such scenarios after the corresponding adaptation of the implementation of isConsistent.
Furthermore, MXP can be easily extended for cases in which the MBD approach has to support the specification of (multiple) test cases, i.e., sets of formulas that must be consistent or inconsistent with the system description, e.g., [21; 22]. 3.2
MXP (Algorithm 2) accepts two sets of constraints as inputs, B as the assumed-to-be-correct set of background constraints and C, the possibly faulty components/constraints.
In case C∪B is inconsistent, MXP returns a set of minimal conflicts Γ by calling the recursive function FINDCONFLICTS in line 3. This function again accepts B and C as an input and returns a tuple hC0, Γi, where Γ is a set of minimal conflicts and C0 ⊂ C is a set of constraints that does not contain any conflicts, i.e., B ∪ C0 is consistent.
The logic of FINDCONFLICTS is similar to QXP in that we decompose the problem into two parts in each recursive call (lines 7–9). Differently from QXP, however, we look for conflicts in both splits C1 and C2 independently and then combine the conflicts that are eventually found in the two halves (line 10)1. If there is, e.g., a conflict in the first part and one in the second, FINDCONFLICTS will find them independently from each other. Of course, there might also be conflicts in C whose elements are spread across both C1 and C2, that is, the set C10 ∪ C20 ∪ B is inconsistent. This situation is addressed in lines 11–15. The computation of a minimal conflict is done by two calls to GETCONFLICT (Algorithm 1). In the first call this function returns a minimal set X ⊆ C10 such that X ∪C2∪B is a conflict (line 12). In line 13, we then 0 look for a subset of C20, say Y , such that Y ∪ X corresponds to a minimal conflict CS . The latter is added to Γ (line 15). In order to restore the consistency of C10 ∪ C20 ∪ B we have to remove at least one element α ∈ CS from either C10 or C20. Therefore, in line 14 the algorithm removes α ∈ X ⊆ CS from C10.
Note that MXP allows us to use different split functions in line 7. In our default implementation we use a function that splits the set of constraints C into two equal parts, i.e., split(n) = n/2, where |C| = n. In the worst case this split function results in a perfect binary tree with n leaves. Consequently, the total number of nodes is 2n − 1, which correspond to 2(2n − 1) consistency checks (lines 5 and 11). Other split functions might result in a similar number of consistency checks in the worst case as well, since in any case MXP has to traverse a binary tree with n leaves. For instance, the function split(n) = n − 1 results in a tree with one branch of the depth n − 1 and n leaves, that is, 2n − 1 nodes to traverse. However, while the number of nodes to explore might be comparable, the important point is that the computational costs for the individual consistency checks can be different depending on the splitting strategy. Under the reasonable assumption that consistency checking of smaller sets of constraints requires less time, the function split(n) = n/2 allows MXP to split the set of constraints faster, thus, improving the overall runtime. 3.3
Consider a CSP consisting of six constraints {c0, ..., c5}. The constraint c0 is considered correct, i.e., B = {c0}. Let {{c0, c1, c3}, {c0, c5}, {c2, c4}} be the set of minimal conflicts. Algorithm 2 proceeds as follows (Figure 1).
Since the input CSP (B ∪ C) is not consistent, the algorithm enters the recursion. In the first step, FINDCONFLICTS partitions the input set (line 7) into the two subsets 1The calls in line 8 and 9 can in fact be executed in parallel.
Input: B: background theory, C: the set of possibly faulty constraints
Output: Γ, a set of minimal conflicts 1 if ¬isConsistent (B) then return ‘no solution’; 2 if isConsistent (B ∪ C) then return ∅; 3 h_, Γi ← FINDCONFLICTS(B, C) 4 return Γ; function FINDCONFLICTS (B, C) returns tuple hC0, Γi if isConsistent(B ∪ C) then return hC, ∅i; if |C| = 1 then return h∅, {C}i; Split C into disjoint, non-empty sets C1 and C2 hC10, Γ1i ← FINDCONFLICTS(B, C1) hC20, Γ2i ← FINDCONFLICTS(B, C2) Γ ← Γ1 ∪ Γ2; while ¬isConsistent (C10 ∪ C20 ∪ B) do
X ← GETCONFLICT(B ∪ C20, C20, C10) CS ← X ∪ GETCONFLICT(B ∪ X, X, C20) C10 ← C10 \ {α} where α ∈ X Γ ← Γ ∪ {CS } return hC10 ∪ C20, Γi C1 = {c1,c2,c3} and C2 = {c4,c5} and provides them as input to the recursive calls (lines 8 and 9). In the next level of the recursion – marked with 2 in Figure 1 – the input is found to be inconsistent (line 5) and again partitioned into two sets (line 7). In the subsequent calls, 3 and 4 , the two input sets are found to be consistent (line 5) and, therefore, the set {c1, c2, c3} has to be analyzed using GETCONFLICT (lines 12 and 13) defined in Algorithm 1. GETCONFLICT returns the conflict { c1,c3}, which is added to Γ. Finally, FINDCONFLICTS removes c1 from the set C10 and returns the tuple h{c2,c3}, {{c1,c3}}i to 1 .
Next, the “right-hand” part of the initial input, the set C2 = {c4,c5}, is provided as input to FINDCONFLICTS 5 . Since C2 is inconsistent, it is partitioned into two sets C1 = {c4} and C2 = {c5}. The first recursive call 6 returns h{c4}, ∅i since the input is consistent. The second call 7 , in contrast, finds that the input comprises only one constraint that is inconsistent with the background theory B. Therefore, it returns h∅,{{c5}}i in line 6. Since C10 ∪ C20 = {c4} ∪ ∅ is consistent with B, FINDCONFLICTS 5 returns h{c4}, {{c5}}i to 1 .
Finally, in 1 the set of constraints C10 ∪ C20 = {c2,c3} ∪ {c4} is found to be inconsistent with B (line 11) and GETCONFLICT is called. The method returns the conflict { c2,c4} and c2 is removed from C10. The resulting set {c3,c4} is consistent and MXP returns Γ = {{c1,c3}, {c5}, {c2, c4}}. Theorem 2. Given a background theory B and a set of constraints C, Algorithm 2 always terminates and returns • ‘no solution’, if B is inconsistent, • ∅, if B ∪ C is consistent, and • a set of minimal conflicts Γ, otherwise.
Proof. In the first case, given an inconsistent background theory B, the algorithm terminates in line 1 and returns ‘no solution’. In the second case, if the set B ∪ C is consistent, C1 = {c1, c2, c3} C2 = {c4, c5} h{c2, c3} , {{c1, c3}}i 1 : h{c4} , {{c5}}i Γ = {{c1, c3} , {c5}} ∪ {{c2, c4}} C = {c3, c4} y C1 = {c1, c2} C2 = {c3} h{c1, c2} , ∅i 2 : h{c3} , ∅i Γ = ∅ ∪ {{c1, c3}} C = {c2, c3} %
C1 = {c4} C2 = {c5} 5 : h{c4} , ∅i h∅, {{c5}}i isConsistent X 3 : iBsC∪oCns=ist{ecn0t, cX1, c2} 4 : iBsC∪oCns=ist{ecn0t, cX3} 6 : iBsC∪oCns=ist{ecn0t, cX4}
B ∪ C = {c0, c5} 7 : isConsistent |C| = 1 then no subset of C is a conflict. MXP terminates and returns ∅.
Finally, if the set B ∪ C is inconsistent, the algorithm enters the recursion in line 3. The function FINDCONFLICTS in each call partitions the input set C into two sets C1 and C2. The partitioning continues until either the found set of constraints C is consistent or a singleton conflict is detected. Therefore, every recursion branch ends after at most log |C|−1 calls. Consequently, FINDCONFLICTS terminates if the conflict detection loop in lines 11–15 always terminates.
We consider two situations. If the set C10 ∪ C20 is consistent with B, the loop terminates. Otherwise, in each iteration at least one conflict in the set C10 ∪ C20 is resolved. This fact follows from Theorem 1 according to which the function GETCONFLICT in Algorithm 1 always returns a minimal conflict if the input parameter C is inconsistent with B. Since the number of conflicts is finite and in each iteration one of the conflicts in C10 ∪ C20 is resolved in line 14, the loop will terminate after a finite number of iterations. Consequently, Algorithm 2 terminates and returns a set of minimal conflicts Γ.
Corollary 1. Given a consistent background theory B and a set of inconsistent constraints C, Algorithm 2 always returns a set of minimal conflicts Γ such that there exists a diagnosis Δi ⊆ SCSi∈Γ CS i.
The proof follows from the fact that – similar to the HStree algorithm – a conflict is resolved by removing one of its elements from the set of constraints C1 in line 14. The loop in line 11 guarantees that every conflict CS i ∈ C10 ∪ C20 is hit. Consequently, FINDCONFLICTS hits every conflict in the input set C and the set of constraints {α1, . . . , αn} removed in every call of line 14 is a superset or equal to a diagnosis of the problem. The construction of at least one diagnosis from the found conflicts Γ can be done by the HS-tree algorithm.
MXP can in principle use several strategies for the
resolution of conflicts in line 14. The strategy used in MXP
by default is conservative and allows us to find several
conflicts at once. Two additional elimination strategies can be
used in line 14: (1) C10 ← C10 \ X or (2) C10 ← C10 \ CS and
C2 ← C20 \ CS . These more aggressive strategies result in
0
a smaller number of conflicts returned by MXP in each call
but each call returns the results faster. However, for the latter
strategies MXP might not return enough minimal conflicts
for the HS-tree algorithm to compute at least one diagnosis.
For instance, let {{c1, c2} , {c1, c3} , {c2, c4}} be the set of
all minimal conflicts. If MXP returns Γ = {{c1, c2}}, which
is one of the possible valid outputs, then the HS-tree
algorithm fails to find a diagnosis as{c1, c2} must be hit twice.
In this case, the HS-tree algorithm must call MXP multiple
times or another algorithm for diagnosis computation must
be used, e.g., [
Corollary 2. Algorithm 2 is sound, i.e., every set CS ∈ Γ is a minimal conflict, and complete, i.e., given a diagnosis problem for which at least one minimal conflict exists, Algorithm 2 returns Γ 6= ∅.
The soundness of the algorithm follows from Theorem 1, since the conflict computation of MXP uses the GETCONFLICT function of QXP. The completeness is shown as follows: Let B be a background theory and C a set of faulty constraints, i.e., B ∪ C is inconsistent. Assume MXP returns Γ = ∅, i.e., no minimal conflicts are found. However, this is impossible, since the loop in line 11 will never end. Consequently, Algorithm 2 will not terminate which contradicts our assumption. Hence, it holds that MXP is complete. 4
We have evaluated the efficiency of computing multiple conflicts at once with MXP using a number of different diagnosis benchmark problems. As a baseline for the comparison, we use QXP as a Theorem Prover, which returns exactly one minimal conflict at a time. Furthermore, we made measurements with a variant of MXP called PMXP in which the lines 8 and 9 are executed in parallel in two threads on a multi-core computer.
We made experiments with different benchmark problems.
First, we used the five first systems of the DX Competition
(DXC) 2011 Synthetic Track. For each system, 20 scenarios
are specified in which artificial faults were injected. In
addition, we made experiments with a number of CSP problems
from the CSP solver competition 2008 and several CSP
encodings of real-world spreadsheets. The injection of faults
was done in the same way as in [
We implemented all algorithms in a Java-based MBD
framework, which uses Choco as an underlying constraint
solver, see [
Since MXP can return more than one conflict at a time, it is expected to be particularly useful when the problem is to find a set ofn first (leading) diagnoses, e.g., in the context of applying MBD to software debugging [5; 7]. We therefore report the results for the tasks “find-one-diagnosis” (as an extreme case) and “find-n-diagnoses”.
The task of finding a single diagnosis is comparably
simple and “direct encodings” or algorithms like
INVERSEQUICKXPLAIN [
DXC Benchmark Problems Table 1 shows the characteristics of the analyzed and CSP-encoded DXC benchmark problems. Since we consider multiple scenarios per system, the number of faults and the corresponding diagnoses can vary strongly across the experiment runs.
Table 2 shows the observed performance gains when using MXP instead of QXP in terms of absolute numbers (ms) and the relative improvement. For the problem of finding the first 5 diagnoses (QXP-5/MXP-5), the observed improvements range from 15% up to 45%. For the extreme case of finding one single diagnosis, even slightly stronger improvements can be observed. The improvements when searching for, e.g., the first 10 diagnoses are similar for cases in which significantly more than 10 diagnoses actually exist.
System #C #V #F #D #D |D| #Cf |Cf| 74182 21 28 4 - 5 30 - 300 139 4.66 4.9 3.3 74L85 35 44 1 - 3 1 - 215 66.4 3.13 5.9 8.3 74283 38 45 2 - 4 180 - 4,991 1,232.7 4.42 78.8 16.1 74181 67 79 3 - 6 10 - 3,828 877.8 4.53 7.8 10.6 c432 162 196 2 - 5 1 - 6,944 1,069.3 3.38 15.0 19.8
for the next set of benchmark problems (six CSP
competition instances, five CSP-encoded real-world spreadsheets
with injected faults [
Scenario #C #V #F #D |D| #Cf |Cf| c8 523 239 8 4 6.25 7 1.6 costasArray-13 87 88 2 >5 3.6 >565 45.6 domino-100-100 100 100 3 81 2 2 15 graceful–K3-P2 60 15 4 >117 2.94 >12 29.2 mknap-1-5 7 39 1 2 1 1 2 queens-8 28 8 15 9 10.9 15 2.8 hospital payment 38 75 4 40 4 4 3 profit calculation 28 140 5 42 4.25 11 9 course planning 457 583 2 3024 2 2 55.5 preservation model 701 803 1 22 1 1 22 revenue calculation 93 154 4 1452 3 3 15.7
The results for determining the five first minimal diagnoses are shown in Table 42. Again, performance improvements of up to 54% can be observed. The obtained improvements vary quite strongly across the different problem instances: the higher the complexity of the underlying problem, the stronger are the improvements achieved with our new method. Only in the two cases in which only one single conflict exists (see Table 3), the performance can slightly degrade as MXP performs an additional check if further conflicts among the remaining constraints exist.
systematically analyze which factors potentially influence the obtained performance improvements, we developed an MBD problem generator in which we could vary (i) the 2The results for finding one diagnosis follow the same trend. Scenario c8 costasArray-13 domino-100-100 graceful–K3-P2 mknap-1-5 queens-8 hospital payment profit calculation course planning preservation model revenue calculation overall number of COMPS, (ii) the number of conflicts and their average size (and as a consequence the number of diagnoses), and (iii) the position of the conflicts in the database. We considered the last aspect because the performance of QXP and MXP can largely depend on this aspect3. If, e.g., there is only one conflict and the conflict is represented by the two “left-most” elements in SD, QXP’s divide-andconquer strategy will be able to rule out most other elements very fast.
We evaluated the following configurations regarding the position of the conflicts (see Table 5): (a) Random: The elements of each conflict are randomly distributed across SD; (b) Left/Right: All elements of the conflict appear in exactly one half of SD; (c) LaR (Left and Right): Conflicts are both in the left and right half, but not spanning both halves; (d) Neighb.: Conflicts appear randomly across SD, but only involve “neighboring” elements.
One specific rationale of evaluating these constellations individually is that conflicts in some application domains (e.g., when debugging knowledge bases) might represent “local” inconsistencies in SD.
Since the conflicts are known in advance in this experiment, no CSP solver is needed to determine the consistency of a given set of constraints. Because zero computation times are unrealistic, we added simulated consistency checking times in each call to the TP. The value of the simulated time quadratically increases with the number of constraints to be checked and is capped in the experiments at 10 milliseconds. We made additional tests with different consistency checking times to evaluate to which extent the improvements obtained with MXP depend on the complexity of an individual consistency check for the underlying problem. However, these tests did not lead to any significant differences.
Table 5 shows some of the results of this simulation. In this evaluation, we also include the results of the parallelized PMXP variant. The following observations can be made.
(1) The performance of QXP strongly depends on the position of the conflicts. In the probably most realistic Random case, MXP helps to reduce the computation times around 20-30%. In the constellations that are “unfortunate” for QXP, the speedups achieved with MXP can be as high as 75%. When QXP is “lucky” and all conflicts are clustered 3We assume a splitting strategy in which the elements are simply split in half in the middle with no particular ordering of the elements.
Random
Left Right
LaR Neighb.
Random
Left Right
LaR Neighb.
Random
Left Right
LaR Neighb. in the left part of SD, some improvements or light deteriorations can be observed for MXP. The latter two situations (all conflicts are clustered in one half) are actually quite improbable but help us better understand which factors influence the performance.
(2) When comparing the results of the first two blocks in the table, it can be seen that the improvements achieved with MXP are stronger when there are more components in SD and more time is needed for performing the individual consistency checks. This is in line with the results of the other experiments.
(3) Parallelization can help to obtain modest additional improvements. The strongest improvements are observed for the LaR configuration, which is intuitive as PMXP by design explores the left and right halves independently in parallel. Note that in the experiments with the DXC and the CSP benchmark problems, in most cases we could not observe runtime improvements through parallelization. This is caused by two facts. First, the consistency checking times are often on average below 1 ms, which means that the relative overhead of starting a new thread can be comparably high. Second, the used CSP solver causes some additional overheads and thread synchronization when used in multiple threads in parallel. 5
In [
Technically, Junker proposes to set a choice point whenever a constraint ci is found to be consistent with a partial relaxation during search and thereby look for (a) branches that lead to conflicts not containing ci and (b) branches leading to conflicts in which the removal of ci leads to a solution.
Unfortunately, it is not fully clear from the informal
sketch in [
From the algorithm design, note that QXP applies a constructive conflict computation procedure prior to partitioning, whereas MXP does the partitioning first – thereby removing multiple constraints at a time – and then uses a divide-and-conquer conflict detection approach. Finally, our method can, depending on the configuration, make a guarantee about the existence of a diagnosis given the returned conflicts without the need of computing all existing conflicts.
In general, our work is related to a variety of
(complete) approaches from the MBD literature which aim to
find diagnoses more efficiently than with Reiter’s original
method. Existing works for example try to speed up the
process by exploiting existing hierarchical, tree-like or
distributed structural properties of the underlying problem [16;
26], through parallelization [
Beside complete methods, a number of approximate
diagnosis approaches have been proposed in the last years,
which for example use stochastic and heuristic search [30;
31]. The relation of our work to these approaches is limited
as we are focusing on application scenarios where the goal
is to find a few first diagnoses more quickly but at the same
time maintain the completeness property. Finally, for some
domains, “direct” and SAT-based, e.g., [
The concept of conflicts plays a central role in different
other reasoning contexts than Model-Based Diagnosis, e.g.,
explanations or dynamic backtracking. Specifically, in
recent years a number of approaches were proposed in the
context of the maximum satisfiability problem (MaxSAT),
see [
We have proposed and evaluated a novel, general-purpose and non-intrusive conflict detection strategy called MERGEXPLAIN, which is capable of detecting multiple conflicts in a single call. An evaluation on various benchmark problems revealed that MERGEXPLAIN can help to significantly reduce the required computation times when applied in a Model-Based Diagnosis setting in which the goal is to find a defined number of diagnoses and in which no assumption about the underlying reasoning engine should be made.
One additional property of MERGEXPLAIN is that the
union of the elements of the returned conflict sets is
guaranteed to be a superset of one diagnosis of the original
problem. Recent methods like the one proposed in [
This work was supported by the Carinthian Science Fund (KWF) contract KWF-3520/26767/38701, the Austrian Science Fund (FWF), and the German Research Foundation (DFG) under contract numbers I 2144 N-15 and JA 2095/41 (Project “Debugging of Spreadsheet Programs”).