4.3.1. Encoding of static consistency criteria

Considering the informal static consistency criteria of Section 4.1, we can now give the following precise validation conditions:

Inadmissible codes: Code x is inadmissible iff PO ⇒ ¬x is valid.

Superfluous parts: Part p can be removed from a position in the system documentation provided that PO ⇒ ¬P(p).

Ambiguities in the parts list: Parts p₁ and p₂, which are assumed to be mutually exclusive, are never selected simultaneously provided that PO ⇒ ¬(P(p₁) ∧ P(p₂)) holds.

Necessary codes: Code x is necessarily contained in any constructible order if PO ⇒ x holds.

Groups of mutually exclusive codes: The group of codes G = {x₁,…, x_n} is mutually exclusive provided that

Valid additional equipment options: A valid order fulfilling the additional restriction F can be extended by equipment option x iff PO ∧ F ∧ x is satisfiable.

Whereas all these criteria can be formulated without referring to multiple computation states (regarding the order processing algorithm), this is not the case any more when we consider the question of consistency of the order completion process. Here, the situation is more complicated, as references to at least two computation states must be made: in case of orders invalidated by the order completion process, we need to compare states describing the order before and after adding the supplemented code; in case of ordering of rule applications we have to compare two states arising from applying different supplementing steps.

Reference to two different states, that is, two different variable assignments, is not (directly) possible in propositional logic. Fortunately, however, the variable assignments corresponding to two different states simultaneously under consideration are almost identical, and differ only on very few variables. This enables us to use formula restrictions F|_x=b, which are defined for a formula F, a propositional variable x, and a Boolean value b ∈ {0,1} as the (unique) homomorphic extension of the function

to the set of all propositional formulae. Informally, the formula restriction F|_x=b can be understood as partially evaluating F for the assignment x = b.

Formally defining the supplementing action relation

of Section 2.1 we get

is the smallest relation with O

O′ provided that these three conditions hold:

and O [vdash ] S(x). Thus, the supplementing action relation can be understood as a shorthand for simultaneous satisfaction of all three conditions. Here, we identify the order as a set of codes O with the order as a characteristic function on the set of all known codes

We can now state a lemma allowing assertions involving several computation states.

Lemma 4.1. Let

Then O′ [vdash ] F iff O [vdash ] F|_x=1. (See Küchlin & Sinz, 2000).█

Proof: First, note that

We prove the lemma by induction on the structure of F. The lemma is obvious for F = [top ] and F = ⊥. Assume that F is atomic, that is, F = y for some propositional variable y. We distinguish two cases. First, if x ≠ y, then y|_x=1 = y and, as O′(y) = O(y), the claim holds. Second, if x = y, then, by F|_x=1 = x|_x=1 = [top ], O [vdash ] F|_x=1 holds, and O′ [vdash ] F, because x ∈ O′. Now, assume F = ¬G. Because (¬G)|_x=1 = ¬(G|_x=1), the induction hypothesis already proves the lemma. The cases F = G ∨ H and F = G ∧ H are handled accordingly using the fact that the restriction is a homomorphism.█

Note that the consequence of this lemma also holds for states O with O [nvDash ] S(x), but then the supplementing rule would not be applicable. We are now placed in a position to formally express the remaining static consistency properties about the supplementing process.

Consistency of the order completion process: Let

be the verification semantics of all constructibility rules, that is, CO describes the constructible, but not necessarily fully supplemented, orders. Then no orders are invalidated by the supplementing process exactly when

holds for all

The order of supplementing rule application for rules S(x) and S(y) is irrelevant provided the following holds:

The last property is a sufficient, but not necessary, condition for order invariance, as it even requires permutability of the two supplementing rules for x and y. The general case demands for a propositional logic specification of the (local) Church–Rosser property for relation

and therefore requires encoding arbitrarily long supplementing chains that may lead to a reunification of the initially different orders. A more in-depth discussion of the limitations of our approach can be found in Küchlin and Sinz (2000).

4.3.2. Dynamic consistency criteria

Formalizing the requirements of Section 4.2 we arrive at the following criteria:

Induced change on the parts level: The implications of changes on the product overview consist of additional and superfluous parts. We will handle this and various specializations in detail below.

Summary of product changes: Assuming fixed times t₀ and t₁ with t₀ before t₁, the models of formulae PO(t₁) ∧ ¬PO(t₀) and PO(t₀) ∧ ¬PO(t₁) describe the newly constructible and no longer constructible orders, respectively.

Time intervals with no constructible orders: Assuming an additional restriction F on orders, the times T_F during which no orders fulfilling property F are constructible is determined by

Computation of this set of times is accomplished by first extracting all relevant starting and stopping times

from the documentation, ordering this set such that T_R = {t₀,…, t_k} for some k and t_i < t_i+1, and then performing the check whether PO(t) ∧ F is satisfiable for each sample point t = ½(t_i + t_i+1) and 0 ≤ i < k. The result for such a t then holds for the whole interval [t_i, t_i+1).

5.1.1. Parts exchange

The reasons that make the exchange of parts necessary can be manifold, for example, technical progress, change between in-house production and external procurement, or change of the supplier. The ways in which the exchange is performed may also vary. There might be a cutoff date at which part p₁ is replaced immediately by part p₂ as depicted in Figure 4(a). Or the exchange has to take place over a period of time during which both variants with either part p₁ or part p₂ have to be manufactured, and for each product instance it is exactly determined by control codes which of the two parts has to be used, as shown in Figure 4(b). A third possibility is that the new part p₂ has to be used as soon as part p₁ runs out of stock. This is similar to the first case, but now the cutoff date is not fixed, but variable. As none of our dynamic consistency criteria directly deals with part exchange, we do not consider this special case any further.

Part exchange: (a) fixed time and (b) overlapping.

Fixed-time as well as overlapping parts exchange can be modeled easily with the control code and time interval additions of Dialog/P.

In the fixed-time case we get the following conditions for the selection rules P₁ = P.p₁ and P₂ = P.p₂ of parts p₁ and p₂ to model a parts exchange at time t₁:

The other time values t_α(P₁) and t_ω(P₂) may be set to sensible values arbitrarily, and the control codes are left unspecified.

To model an overlapping parts exchange we need support from the control codes. Leaving the start time of the overlap interval open, and assuming the end of the overlap at time t₂, we get:

where x_c is the control code of the overlap, that is, all orders containing x_c use part p₂ and orders not containing x_c use part p₁. Again, the remaining time values may be set to any suitable value, and the control codes not mentioned are left unspecified. If the interval start time is to be fixed, this has to be controlled using the constructibility rule of control code x_c. Adding t_α(C.x_c) = t₁ we get the behavior depicted in Figure 4(b).

5.1.2. Equipment code start-up and expiry

New equipment codes may show up as part of the continuous development of products. Other equipment codes may run out because they are not requested by customers anymore or they have been integrated into standard packages. Most of these changes are triggered by the engineering or even the sales department. This is in contrast to the case of timing control codes, which are set by the production department, mainly to handle model year change. Model year change is an important issue and requires a lot of redocumentation, as usually quite substantial parts of the product change from one year to another. Most of the overlapping parts exchanges mentioned above stem from this modification.

What makes code startup and expiry a nontrivial documentation task is that the high-level changes of the product overview influence the low-level parts structure via the parts selection rules P.p. In case of starting and stopping control codes the direct influence is clearly visible, but this may not be the case for other codes, or if a timing control code is used inside a rule.

Such induced, dependent changes are often very hard to detect, as can be seen from the following example: Assume a part p with an unrestricted validity time interval I(P.p) = (−∞,+∞) and no timing control codes, and a selection rule's formula P(p) = x ∧ y. Furthermore, let the constructibility formula of code x be C(x) = z and assume an intended code expiry for code z at time t₁, which is t_ω(C.z) = t₁. Then after t₁, p cannot be part of a valid order, because the expiration of z induces the invalidity of code x, which forces the selection rule of p to false.

What makes these induced expiry parts hard to detect for the documentation personnel is that the codes planned for expiry need not occur in the part selection rule as in the example above. Besides, for complex products, different persons may be involved in the documentation of change. Automatic support by a PDM system to find such induced expiry parts is therefore highly desirable. We now present our approach to solve this problem.

5.1.3. Assembly line reconfiguration

Our last scenario of change is largely caused by modifications of the production environment. For instance, assembly lines are reconfigured from time to time to adapt them to the actual production load. Less frequently, but entailing considerable changes of the documentation, entire or partial model lines are shifted from one assembly line to another or even between plants.

The challenges for the documentation personnel are similar to the case of equipment code change, but they often go even beyond that. The main problem is to determine the influence of the change on the parts level with the same problems as mentioned above.

Moreover, at least in our case, some changes are not documented, or not documented early enough, or even cannot be documented at all within the PDM system. This poses the problem of handling undocumented change. For the purpose of verification, we thus need an external formalism to specify certain documentation changes that cannot be handled by the PDM system itself.

5.2.1. The ±δ-Method

With the ±δ-method we can determine which parts become superfluous and which are additionally needed after a critical change that is already known to occur at a fixed time t_c in the future and where the change is already documented. The procedure works in three steps.

The resulting sets S and A give the sets of parts that are superfluous and are additionally needed, respectively, after the change. The parameter δ has to be chosen such that only the critical change falls into the time interval (t_c − δ, t_c + δ). Note that this is, at least theoretically, a limiting factor of the ±δ-method, as it may be impossible to separate the critical change from other changes. In practice, this effect occurs rarely, as the primary interest is in the situation after accumulating all changes at the critical time t_c.

5.2.2. The 3-point method

Substantial changes, as required, for example, for model year change or production relocation, cannot be performed in the short time interval presupposed by the ±δ-verification method. Moreover, some changes cannot easily be modelled within the documentation system Dialog, but fit quite naturally in the logical formulation used in BIS. We therefore developed another methodology to determine induced change on the parts level. This method also allows simulation and comparison of different future scenarios.

In contrast to the ±δ-method, the 3-point method is capable of handling documented as well as (yet) undocumented change. This is accomplished by providing an external (with respect to the PDM system) formalism for specifying change. The modifications that can be expressed within this formalism include

• equipment or control codes becoming valid or invalid and
• arbitrary code combinations becoming invalid.

In our formalism, changes are specified as modifications of the product overview's semantics. We denote the changed semantics by

is the set of codes for which the constructibility and supplementing rules are ignored and A is an additional side condition formula. The changed semantics is defined by

Validation of an invalid code x, which is a code with constructibility formula C(x) = ⊥, can be achieved by including code x into the set of newly valid codes

, thereby inactivating the unsatisfiable constructibility formula for code x. If it should be necessary, a new constructibility or supplementing rule can be specified as a conjunctive part of formula A. Invalidation of codes, as well as additional side conditions, are specified by conjunctively adding formulae to A; for example, ¬x indicates that code x becomes invalid.

For the 3-point method, two points in time, t₀ and t₁, have to be fixed, between which the undocumented changes should occur. Moreover, the modified product overview semantics

with a fixed set

and a side-condition formula A is employed to reflect undocumented changes. The 3-point method is composed of four steps:

Here, for example, A₁₀ indicates the additional parts needed at time t₁, ignoring undocumented changes, relative to the parts needed at time t₀. The relationship between the three sets of parts and the difference sets are graphically illustrated in Figure 5.

The 3-point approach.

To determine the impact of an intended product overview change on the part usage, we have to take a look at the difference sets. The sets A_*0 /S_*0 indicate the overall change between t₀ and t₁ if the intended (undocumented) change really is performed, including all changes induced by already documented events. The difference sets A_*1 /S_*1 reflect the changes induced at time t₁ by the undocumented modifications alone. Moreover, and similar to the ±δ-method, the sets A₁₀ /S₁₀ only show the impact of already documented changes during the time interval (t₀, t₁).

5.2.3. Discussion of both methods

Comparing the two methods, the ±δ-approach offers the advantage of simplicity. To find out the impact of a change on the parts' world only the point in time of this change has to be specified. On the other hand, the intended modification already has to be documented, and the time of the change has to be fixed. Whereas this is usually the case for planned, regularly occurring events like code start-up and expiry due to model year change, this may not be the case for other product modifications, for example, by further product development. Here the 3-point method can play out its strength of handling even undocumented modification events, however, at the cost of increased complexity in usage. This shows up in the need to specify the modified product overview semantics

In most cases, though, the undocumented changes follow certain patterns, so that special cases of the modified semantics may be pre-encoded and offered as specialized tests.

Note that the 3-point method properly includes the ±δ-method. By setting t_0/1 = t_c ± δ in the 3-point method, we get a specialization equivalent to the ±δ-approach, as PO_{Ø,[top ]}^*(t) = PO(t). In this case we have P_t1^* = P_t1, and only the difference sets A₁₀ and S₁₀ are of interest. Another weakness of the ±δ-method already mentioned in Section 5.2.1 is that the separation of two events may be impossible. The 3-point method allows us to handle such a case by remodeling the relevant events externally.

5.2.4. Mapping of typical cases

We now show how to map two important scenarios of change to our verification formalisms. Our first case handles equipment code start-up and expiry caused by model year change, for which we use the ±δ-method. Model year change usually is accompanied by lots of changes, mainly on the parts level, but also to a smaller fraction on the product overview level. During an overlapping interval, both models from the old and the new model year have to be manufactured. Assume codes m_o and m_n are responsible for controlling model year change, that is, orders for cars of the old model year are tagged with code m_o, for the new model year with code m_n. Assume further that the model year change is fixed to take place during the time interval (t₀, t₁). The interesting question is which parts are not needed any more after t₁. In the documentation, the expiry of the old model year is reflected by code m_o becoming invalid, as well as code m_n becoming mandatory at t₁. Moreover, some parts may happen to have t₁ as a starting or stopping time. In summary, the rules changing at time t₁ are:

as well as selection rules of parts p with either t_α(P.p) = t₁ or t_ω(P.p) = t₁. We thus set up the ±δ-method with t_c = t₁ and get resulting difference sets of A and S, indicating additionally needed and superfluous parts after the end t₁ of the model year change overlap interval. Obvious starting or expiring parts (i.e., parts with t_α(P.p) = t₁ or t_ω(P.p) = t₁) may additionally be filtered out to get a more concise result.

Let us now turn to production relocation, where we consider moving parts of the production from one assembly line (or plant) to another. Of this two-sided problem of moving in and off, we concentrate on the move-off part. Such a kind of change cannot (easily) be handled within the Dialog/E system, as not only individual codes, but arbitrary code combinations, representing the fraction of the production that is to be relocated, become invalid after the change. One important problem related to production move-off is to determine the induced parts shift.

To handle this case, we use the 3-point method to find out precisely the induced parts shift. We set up t₁ as the approximated time of the relocation event, and t₀ as the current time. The modified product overview semantics is set to PO_Ø,¬F^*(t), where F is a formula describing the fraction of the production to be moved off.

As an example, let us consider the situation where the production of cars containing the motor variants M1, M2, and M5, in cunjunction with automatic gears (A) is planned to be moved off but not for the destination countries C1, C3, and C4. The formula

describes this production shift.

The results delivered by the 3-point method are manifold. Perhaps the most important parts shift sets are A_*1 /S_*1. They indicate the additional and superfluous parts after the relocation at t₁ relative to the situation at the same time without the relocation. If the overall change on the parts level between the current situation (at t₀) and the projected situation after the relocation at t₁, also including already documented product changes, is of interest, then the difference sets A_*0 /S_*0 provide the appropriate information.

Definition 6.1.

For each n ≥ 0 and M ⊆ {0,…, n}, S_Mⁿ is an n-ary operator, and S_Mⁿ(F₁,…, F_n) is true iff exactly k of the formulae F₁,…, F_n are true for some k ∈ M.█

Thus, for example, S_{0,1}ⁿ(F₁,…, F_n) denotes the fact that at most one of the formulae F₁,…, F_n is true.

Among the advantages of adding the selection operator to the language are the compact formula size for symmetrically related subformulae (such as mutually exclusive groups) and the conservation of structural properties that are lost by other encodings, including the opportunity to make use of the preserved structural information in automatic SAT checking.

6.4.1. Algorithm Basic

This algorithm (see Fig. 7) determines the sets of INO variables by testing for each variable x occurring in F whether the formulae F|_x=1 and F|_x=0 are satisfiable. The number of satisfiability tests is i + 2(o + n) for a formula that has i inadmissible, n necessary, and o optional variables. Investigating at first whether a variable is necessary would result in n + 2(i + o) calls to SAT.

The INO algorithms Basic, Filter, and the variable selection algorithm SAT-Heuristics-Directed.

6.4.2. Algorithm Filter

Algorithm Basic can be improved in two ways. If some variable is not inadmissible and not necessary, SAT returns a set of models A. For each variable x occurring positively in some model this allows the immediate conclusion that x cannot be inadmissible. Conversely, each variable occurring negatively in any model cannot be necessary. In the following I′ denotes the set of variables that are not inadmissible and N′ denotes the set of variables that are not necessary. We thus attain O = I′ ∩ N′. If the number of optional variables is dominant, as in our application area, this filtering criterion can reduce the number of required SAT tests dramatically. Moreover, by setting inadmissible and necessary variables as soon as possible to the only value they can take, we can gradually reduce formula size and hence accelerate the underlying SAT algorithm. Algorithm Filter in Figure 7 is an extension of Algorithm Basic and implements these ideas.

6.4.3. Algorithm Directed Filter

The effect of filtering depends on the set A of models returned by the SAT algorithm. The filtering works best if the models contain variables positively that have not yet been detected as admissible, and contain variables negatively that have not yet been classified as not necessary. In order to maximize in algorithm Filter the number of variables for which this condition holds, we use a corresponding variable selection strategy in the underlying Davis–Putnam style SAT checker, as implemented by the algorithm SAT-Heuristics-Directed shown in Figure 7. The second value B returned by the algorithm indicates whether the variable should be set first to true (1) or false (0) during model search. Thus, we obtain the algorithm Directed-Filter.

In order to check the effectiveness of our INO algorithms, we conducted experiments with a set of Mercedes model classes (Kaiser & Küchlin, 2001a). The results demonstrate the effectiveness of Filter and Directed-Filter compared to Basic. Comparing Basic to Filter, improvements between 47 and 91%, in terms of time, and 34 and 91%, in terms of SAT calls, could be measured. In addition, using the modified variable selection heuristics SAT-Heuristics-Directed further accelerated INO search by up to 90% and reduced the number of SAT calls by up to 89%. For only one formula that contained relatively few optional variables Directed-Filter performed worse.

6.5.1. Localization

Using the formalization PO of the product overview as presented in Section 3, we can reduce the localization problem for most controversial assertions a to the computation of a minimal unsatisfiable subformula (MUS) of PO ∧ a. Traditionally, a MUS is defined for a set of clauses. Slightly generalized, for a conjunction C = F₁ ∧ ··· ∧ F_n of a set of formulae S = {F₁,…, F_n} with C being unsatisfiable, a MUS of C is a subset S′ of S such that

is still unsatisfiable, but

is satisfiable for all S′′ ⊂ S′. See (Davydov et al., 1998; Kleine Büning & Xishun, 1998; Kullmann, 2000) for further elaborations and special purpose algorithms for MUS computation.

So, for a contradictory formula, a MUS is a smallest subset that is still contradictory. In our configuration setting, the cause of an inconsistency can thus be reduced to a (small) fraction of the rule base. Localization by MUS computation is possible for all assertions of the form PO ∧ a when formulated as a SAT problem, which indeed holds for all static and dynamic consistency properties with the exception of consistency of the supplementing process. However, using CO instead of PO allows a similar reduction in these cases, too.

It turned out to be practical to extend the notion of a MUS to arbitrary formulae in negation resp. selection normal form. Thus, MUS computation can be performed on a formula representation that is much closer to the original Dialog rules.

Definition 6.2.

For an unsatisfiable propositional formula f in negation normal form we call g a minimal unsatisfiable subformula (MUS) of f, if and only if the following conditions hold:

1. g is obtained from f by deleting arbitrary direct subformulae of conjunctions, that is, by replacing subformulae of the form h₁ ∧ ··· ∧ h_n by h_i1 ∧ ··· ∧ h_ik for {i₁,…, i_k} ⊆ {1,…, n}.
2. The formula g is unsatisfiable.
3. Removing an arbitrary direct subformula from a conjunction of g makes the resulting formula satisfiable. █

For an extension of this definition to formulae in SNF, we consider selection operators as atomic formulae, thereby forbidding subformula deletions under selection operators.

Consider the formula following as an example:

Deleting d from the main conjunction and replacing b ∧ d by b in the nested conjunction results in

which is still unsatisfiable. Removing any further direct subformulae of any conjunction in G makes it satisfiable, however. In this example, the only MUS of F is G. In many cases a formula's MUS is considerably smaller than the formula itself.

For an unsatisfiable F in selection normal form, the strategy to find a MUS is straightforward. Initially, we take F as an approximation of our MUS F_M, and for each conjunction C in formula F we remove direct subformulae from F_M, as long as the resulting formula is still unsatisfiable. This leads to an algorithm with a number of SAT-calls linear in the number of direct subformulae of conjunctions. More details on the algorithm can be found in (Kaiser & Küchlin, 2001b). An example of a MUS calculated by BIS is shown in Figure 8. In the upper part of the figure, each item shows a complete rule with highlighted literals corresponding to the MUS. In our formalization PO all rules are conjunctively connected, so that each item is a direct subformula of PO's main conjunction. The lower part shows a compressed view where nested subformulae that are not part of the MUS are not displayed. We will discuss the presentation of a MUS in BIS in more detail below.

A MUS in BIS.

We conducted experiments with this algorithm and could demonstrate the practical effectiveness and applicability of our MUS computation approach. For the localization of inconsistencies, the problem of finding a MUS, which in theory belongs to the second level of the Boolean hierarchy (Papadimitriou & Wolfe, 1988), turned out to be tractable in our application. With only simple heuristics, it never took the system more than one minute on a Sun Ultra E450 to find a MUS for formulae with several thousands of conjunctive subformulae (|S_F|), approximately 1,000 rules (|R_F|), and more than 1,000 variables (cf. Table 2). In many cases, the run time was even below 1 s.

The typical size of a MUS in BIS

To investigate the effectiveness of MUS computation for explaining inconsistencies we collected a set of 50 formulae originating from alerts due to inadmissible and necessary codes (Kaiser & Küchlin, 2001a) and measured some characteristics of MUS computation. Table 2 displays a short excerpt of the test results. In all cases, the number of conjunctive subformulae (|S_FM|) as well as the number of rules (|R_FM|) could be reduced by 99%. Thus, with only a couple of constraints and smaller subformulae within these constraints left, MUS computation enables our system to narrow the cause of an inconsistency to a manageable subset of the product database.

6.5.2. Presentation of results

In addition to the size of a conflicting rule set, the form in which the result is presented to the user is important for the usefulness of the explanation feature. Clearly, the MUS becomes tedious to read even for small formulae, and the relation to the original formula is not obvious. On the other hand, printing the whole formula of the consistency condition (possibly highlighting the contained MUS) yields a large complex formula, even if only relevant constraints are displayed.

Our answer is to list all relevant rules of the original formula, and to replace within these rules any maximal irrelevant subformula by a wild card like ···, as shown in Figure 8. In the 71-kB formalization of a C-class limousine (consisting of 694 constructibility and 127 supplementing rules) the system finds a total of three constraints to become contradictory in combination with the (inadmissible) code 030. While the complete constraints displayed in the upper part of Figure 8 are still hard to analyze, it is feasible to understand the inadmissibility of code 030 from the maximally reduced yet structure preserving representation in the lower part of the example. Here the relation to the original constraints is obvious. However, it may still not be immediately obvious why the MUS is unsatisfiable. Hence we need more of an explanation.

6.5.3. Reasoning

Approaches to explain the unsatisfiability of a propositional formula are as numerous as SAT algorithms. For example, any execution trace of a complete SAT algorithm, such as a resolution refutation tree (Robinson, 1965) or the search tree of the Davis–Putnam algorithm (Davis & Putnam, 1960), yields an exhaustive explanation. The specific form of the resulting explanation depends considerably on heuristics, like variable selection for SAT (Hooker & Vinay, 1995), which fill some indeterminism within the general algorithm. These heuristics critically influence the efficiency of the search, and consequently the size of an explanation, which is the main determinant of its quality. Besides size, intuition and intelligibility are important factors for the quality of an explanation. Even though there is no objective measure of these two factors, we cannot leave them out because they are directly related to the explanation size. For example, the listing of a set of constraints together with the notice that they are unsatisfiable may be sufficient for someone who knows the formalization and is trained in logical reasoning, whereas for the documentation personnel at least a step by step refutation in terms of codes is desirable.

In BIS, we use a linear execution trace of the backtracking SAT algorithm proposed by Davis, Logemann, and Loveland (1962). Explanations therefore indeed are refutation proofs: We start with the converse of the assumption and show that this leads to a contradiction. The applied reasoning process contains immediate consequences and case distinctions. Immediate consequences are due to constraints containing only a single propositional variable, and therefore rule out all orders either including or excluding this code. Such constraints are considered first (unit propagation). If there are no such constraints, we choose a code for case distinction and explain in two steps why we did not find a valid order with or without this code.

Figure 9 illustrates how the system justifies its conclusion that code 680 is inadmissible in a C-class limousine. It lists five vehicle variants (955+R, 955+−R, −955+M112, −955+−M112+R, −955+−M112+−R) which all lead to inconsistencies in conjunction with code 680. For example, an order with codes 680 and M112 and without 955 (case 1.2.1, Fig. 9), makes codes M55, 954, M113, and R inadmissible and codes 498 and L necessary. This leads to a contradiction because L becomes inadmissible (due to the first part of the conjunction of the seventh rule) and necessary at the same time. Listing with each reduction step the formula causing the implication would make the justification more intelligible but considerably longer. It should also be noted that we do not use any kind of SAT learning techniques (Bayardo & Schrag, 1997; Silva & Sakallah, 1999) to shorten explanations, because there is no obvious way to integrate this kind of argument into a causal explanation without confusing the user.

An example of an explanation in BIS.

To measure the practicability of this explanation technique in our application domain, we tested this functionality on the minimal unsatisfiable formulae (F_M) computed during the experiments of Section 6.5.1. We collected the total number of variables (|V_FM|) occurring in F_M, as well as the total number of leaves in the search tree of an unsuccessful complete model search (|SAT(F_M)|). Table 3 lists the results for some of those formulae.

The typical size of an explanation in BIS

No MUS contained more than 13 different variables which limits the size of a justification to a worst-case value of 2¹³ = 8192 distinguishable cases. The actual number of cases displayed in the third column of Table 3 clearly shows that the automatically generated justifications are even tractable for humans. Due to unit propagation, never more than five cases needed to be analyzed, and indeed, for most formulae the contradiction is immediate without any case distinction.