Keywords

1 Introduction

In financial and public sectors, regulations and policies are often specified in terms of rules describing relationships between input and expected output. As an example, consider a rewarding policy for a vehicle insurance company. Beside the normal contracts, the company offers two special rewards in the form of discounts (in percentages) for the insurance and shopping coupons. The availability of the rewards to customers depends on the duration (number of years) of the contracts, their online account status (whether or not they already have an online account), and their VIP membership status. The policies on how rewards are offered to a customer are as follows.

  • (R1) If the customer has an online account then either a discount of 3 % or a 100$ coupon is offered.

  • (R2) If the customer is a VIP then a discount of at least 5 % and a coupon valued between 50$ and 100$ are offered.

  • (R3) If the customer is not a VIP and the contract duration is less than 2 years then either a discount of less than 5 % or a coupon valued between 30$ and 50$ is offered.

  • (R4) If the customer is a VIP and the duration of the contract is at least 2 years then a discount of at least 7 % and a 50$ coupon are offered.

Each rule comprises a constraint on the input and a constraint on the output, imitating logical implication. In particular, the rules are non-deterministic, i.e., given a rule and some input, there could be more than one satisfying output. This type of specification rules is particularly useful in the early system design process, where requirements are obscure and the system details cannot be decided. Non-determinism is essentially what makes specification rules different from production rules used in production rules used in Business Rule Management Systems (BRMSes) [7]. Production rules are designed for execution, and hence they are necessarily deterministic. More discussion on the similarities and differences between specification rules and production rules can be seen in Sect. 6.

Given a set of rules, i.e., a rule base, various properties can be statically analysed. One of the most important properties of a rule base is consistency: the rule base should be conflict-free, i.e., there must be some possible output for any valid input. Otherwise, the regulations represented by the rule base are infeasible and cannot be implemented. In the example of the vehicle insurance company, the policy is inconsistent. More specifically, when a customer is a VIP with a 3-year contract and an online account, there are no possible values for the insurance discount and the shopping coupon satisfying the rewarding policy.

This paper focuses on the consistency analysis of a special type of specification rules, namely those where the output constraints do not refer to the input (e.g., the vehicle insurance example). This type of specification rules is sufficient to stipulate many policies in financial and public sectors such as taxation regulations or insurance policies. Consistency analysis of this type of rules is a challenging problem. In the worst cases, there can be exponentially many set of inconsistent rules within a rule base. Moreover, even in the case where the rule base is consistent, one (potentially) has to consider every combination of the rules. Our motivation is to develop some program for efficiently validating the consistency of specification rules.

Within our knowledge, there are no existing technologies for formally verifying consistency of non-deterministic specification rules. However, given the fact that each rule is made up of an input constraint and an output constraint, the consistency of rules is related to the satisfiability of constraints. Recent advancement in the field of SMT solvers enables the possibility of checking satisfiability for a large and complex set of constraints of different types [4]. In particular, SMT solvers have been showed to be applicable to hardware designs, programs verification, etc. Various SMT-based problems have been investigated. Amongst them is “infeasibility analysis”, the study about constraint sets for which no satisfying assignments exist. Given an unsatisfiable constraint set, useful information about this set includes to identify where the “problem” occurs. There exist efficient algorithms for extracting a Minimal Unsatisfiable (sub-)Set (MUS), i.e., the unsat-core, of an unsatisfiable constraint set [6, 13, 15]. Recently, algorithms for finding all MUSes have been proposed [3, 10, 11].

In order to validate the consistency of a rule base, we enumerate all Minimal Inconsistent Sets (MISes) of the rule base. A MIS is a set of inconsistent rules that is minimal, with respect to the set-inclusion ordering. Similar to the MUSes of constraints, the MISes of rules identify where the problems occur within the rule base. By exploring the relationship between the MISes of the rule base, the MUSes of the output constraints, and satisfiability of individual input constraint, we reduce the problem of enumerating the MISes to that of the MUSes of the output constraints. We use SMT solvers as black-boxes for solving satisfiability problems. Furthermore, our approach is constraint-agnostic, i.e., independent of the type of the input and output constraints.

We identify the relationship between the MISes of the rules, the MUSes of the output constraints, and the satisfiability of the input constraints. Our contribution is a novel algorithm for fast enumeration of MUSes. We compare our algorithm against the state-of-the-art program for MUSes enumeration from [10] using some publicly available benchmarks. The correctness of our approach is ensured by the formalisation of the algorithms using the Event-B modelling method [1] and the mechanical proofs using the supporting Rodin platform [2]. A more detailed version of this paper including the Event-B formalisation can be found elsewhere [9].

The rest of the paper is structured as follows. In Sect. 2, we present some background information including the problem of constraints satisfiability and rules consistency. In Sect. 3, we discuss the relationship between MISes and MUSes, showing that the problem of finding MISes can be reduced to enumerating MUSes. In Sect. 4, we present a novel and efficient algorithm for enumerating MUSes. In Sect. 5, we give our empirical analysis of the new algorithm and its application in finding MISes. Finally, we draw some conclusions in Sect. 6.

2 Background

2.1 Constraints Satisfiability

In this paper, we often discuss satisfiability problems related to different generic sets of constraints. For each set of constraints, the constraint type and variables domain are omitted. In general, we will consider some indexed set of constraints . Each constraint specifies some restrictions on the problem’s variables. Constraint is satisfied by any assignment of the variables that meets ’s restriction. We use the notation to denote the fact that satisfies , and otherwise.

Given a set of constraints , if there exists some assignment satisfying every constraint in then is said to be satisfiable . Otherwise, is unsatisfiable . More formally, given a set of constraints , we have

(1)
(2)

In this paper, we will be interested in two special types of sets of constraints, namely: Maximal Satisfiable (sub-)Set (MSS) and Minimal Unsatisfiable (sub-)Set (MUS). A set of constraints is an MSS if it is a satisfiable subset of and cannot be expanded without compromising satisfiability, i.e.,Footnote 1

(3)

Conversely, a set of constraints is a MUS if it is an unsatisfiable subset of and is minimal with respect to the set-inclusion ordering, i.e.,

(4)

MUSes are valuable since they indicate the core reason for unsatisfiability of a constraint set. In particular, as showed in Sect. 3, MUSes play an important role in verifying rules consistency.

2.2 Rules Consistency

Consider a generic set of rules , where n is a positive number. Each rule consists of a constraint over the input variables and a constraint over the output variables. The set of input and output variables are disjoint. The types of constraints are not specified.

Definition 1

(Rule Satisfiability). A rule is satisfied by an assignment of the input variables and an assignment of the output variables —denoted as — if either does not satisfy or satisfies , i.e., .

A subset of rules is “consistent” () if for every input assignment, there exists some output assignment such that the assignments satisfy all rules in . Otherwise, it is inconsistent . For convenience, when the generic set of rules is known, we identify its subsets by sets of indices, i.e., subsets of the range 1 . . n. The consistency definition is lifted accordingly to sets of indices.

Definition 2

(Rule Consistency). Given a set of indices \(S \subseteq 1 . . n\),

(5)
(6)

From now on, we will use set of rules and set of rule indices interchangeably.

Given an inconsistent rule base , some indicating facts about should be given to “explain” ’s inconsistency. We define the following notion of Minimal Inconsistent Set (MIS) of a set of rules, the inconsistent core of .

Definition 3

(MIS). Given a set of rules \(S \subseteq 1 . . n\), S is a MIS if and only if S is inconsistent and is minimal with respect to the set-inclusion ordering, i.e., .

Clearly, a rule base without any MIS is consistent. In the case where is inconsistent, ideally, all MISes of should be found. In general, the problem of finding all MISes is intractable: the number of MISes may be exponential in the size of the rule base. Our main objective is to quickly enumerate MISes.

Example 1

Consider the rewarding policy mentioned in Sect. 1. The input and output constraints of the rules can be formalised as follows.

figure a

In the above example, input assignment “\(account, VIP, duration := \mathsf {F}, \mathsf {T}, 1\)” and output assignment “\(discount, coupon := 5, 50\)” satisfy all rules. The set of rules is inconsistent (as mentioned before) and has one MIS, i.e., .

3 Relationship Between MISes and MUSes

In this section, we investigate the relationship between MISes and satisfiability problems on the input and output constraints. Since the input and output variables are disjoint, satisfiability problems on input constraints and output constraints are independent. Given a set of rules S, the following lemmas express some relationships between the consistency of S and the satisfiability of S’s input and output constraints. The lemmas can be proved directly from the corresponding definitions. Below, we use the notation for (similarly for and ).

Lemma 1

Lemma 2

In general, S’s consistency cannot be directly determined by the satisfiability/unsatisfiability of its input and output constraints. In particular, when and , S’s consistency is determined by the consistency of S’s proper-subsets. Consider Example 1, and have unsatisfiable input and output constraints, but only the former one is consistent. To avoid iterating the subsets of rules, we prove the following theorem.

Theorem 1

(MISes and MUSes). .

Proof

(Sketch).

  1. 1.

    From left to right: Assume , we have . We infer that since if , one of S’s proper-subset must be inconsistent, hence S cannot be minimal. We have since if then (Lemma 2). Subsequently, , since otherwise there exists a set \(T \subset S\) such that . From Lemma 1, we have , and hence S is not minimal inconsistent.

  2. 2.

    From right to left: Assume and . We deduce that from Lemma 1. For every \(T \subset S\), we have , hence (Lemma 2). As a result, S is minimal inconsistent.    \(\square \)

Theorem 1 reduces the problem of enumerating MISes to finding the MUSes of the output constraints, and then checking the satisfiability of the input constraints corresponding to each MUS found. As a result, the quicker output constraints’ MUSes are discovered, the faster we can enumerate MISes. In the next section, we present a novel and efficient algorithm for enumerating MUSes.

4 An Efficient Algorithm for Enumerating MUSes

In general, enumerating MUSes is a well-known problem and potentially intractable (since the number of MUSes may be exponential in the number of constraints). A detailed discussion on existing approaches for enumerating MUSes can be found in [10], including both constraint-specific and constraint-agnostic algorithms. In this paper, we present our algorithm for fast enumeration of MUSes, inspired by the state-of-the-art algorithm  [10].

The main feature of is the use of a powerset manager maintaining a powerset map for selecting subsets to be explored. Given, a constraint set , the powerset map is a set of propositions over a collection of indexed variables , with \(i \in 1 . . n\) where n is the number of constraints in . There are three basic operations for the powerset manager (Fig. 1). In , the powerset manager utilises the capability of the constraint solver to return a model for a satisfiable set of constraints, which corresponds to an unexplored subset (a subset required to be validated). Operations and are for pruning the unexplored subsets. Operation (resp. ) marks all subsets (resp. supersets) of the input set S as explored (no longer need to be validated).

Fig. 1.
figure 1

Operations of the powerset manager

Full size image

4.1 The algorithm

Intuitively, for each iteration, (Fig. 2) gets a new unexplored subset from the powerset manager. If is satisfiable, uses a sub-routine to obtain an MSS, and adds this MSS as a lower bound to restrict future iterations. Otherwise, i.e., if is unsatisfiable, uses a sub-routine to obtain a MUS, yields this MUS, and adds the found MUS as an upper bound. The correctness of the algorithm relies on the fact that MUS cannot be a subset of an MSS or a (strict-)superset of another MUS. At each iteration, the powerset manager is restricted hence the algorithm terminates.

Fig. 2.
figure 2

The algorithm

Full size image

The sub-routines and can be any off-the-shelf methods for finding an MSS (from a satisfiable seed) and a MUS (from an unsatisfiable seed). For example, the operation in Fig. 3 gradually adds new elements to a satisfiable subset S if this preserves satisfiability. Conversely, removes elements step-by-step from an unsatisfiable subset S if it preserves unsatisfiability. Both and are not the most efficient implementation for and sub-routine. For instance, the operation in Fig. 3 and its sub-routine perform binary search and potentially return a MUS faster than . A similar binary search algorithm exists for the routine. The algorithm and various and routines are not novel.

Fig. 3.
figure 3

Various and routines

Full size image

Example 2

A possible execution trace for (using and ) applied to the output constraints of the rules – in Example 1 is below. At each step, we show the seed obtained from the powerset manager and its satisfiability status. Depending on the satisfiability status of the seed, a growing or a shrinking sub-routine is called to obtain an MSS or a MUS. We also report the number of SMT calls (the number of times that the SMT solver is called to check the problem constraints) and the number of SAT calls (querying the powerset manager). For example, in Step 2, the powerset manager returns (at a cost of 1 SAT call) and checking satisfiability of this seed costs 1 SMT call. Afterwards, it takes 2 SMT calls to grow the seed to obtain the MSS .

figure b

4.2 The Algorithm

Notice that, in the algorithm, the powerset manager is only used for retrieving unexplored subsets. In particular, during the process of growing and shrinking seeds, many satisfiability checks are spurious: the sets are either supersets of some found MUS or subsets of some found MSS. Satisfiability checking of the problem constraints (possibly involving theories) is more expensive than querying the powerset manager (concerning only Boolean constraints). Furthermore, during the process of growing, often unsatisfiable subsets are found. By calling sub-routine on these unsatisfiable subsets, we can get MUSes faster. The challenge is to ensure that by shrinking immediately, we obtain a new MUS.

The algorithm can be seen in Fig. 4. Compared to , the main difference is the use of the powerset manager within the and sub-routines. In particular, returns either a MUS or an MSS. In the subsequent, we outline the implementation of and . First, we extend the powerset manager with satisfiability checking.

Fig. 4.
figure 4

The algorithm

Full size image

Satisfiability checking with powerset manager. The following operation is added to the powerset manager in order to check if a set of constraint need to be explored. This is done by checking the satisfiability of the set of propositions together with the constraint representing .

figure c

Theorem 2 states an important property of , in particular, for the explored subsets filtered out by the powerset manager.

Theorem 2

(Explored subsets of constraints). For the algorithm, given a subset of constraints , we have

(7)

Proof

(Sketch). This fact is trivial invariant of the algorithm since the set of unexplored subsets can only be pruned in the following two cases:

  1. 1.

    An MSS is added as a lower bound.

  2. 2.

    An MUS is added as a lower bound and an upper bound.

As a result, a set is explored if and only if either (a) is a subset of an MSS (some satisfying set L), or (b) is a subset of some MUS M, or (c) is a superset of some MUS M.    \(\square \)

The following Lemmas are consequences of Theorem 2.

Lemma 3

(Satisfiability during ). Given sets of constraints S and T, if , \(T \subseteq S\), and , then .

Proof

From , apply Theorem 2, we have three cases as follows.

  1. 1.

    There exists L where , we have trivially by anti-monotonicity of .

  2. 2.

    There exists M where , we have trivially by definition of  (4).

  3. 3.

    There exists M where . From \(T \subseteq S\), we obtain \(M \subseteq S\). Apply Theorem 2, we have which is a contradiction.

Lemma 4

(Unsatisfiability during ). Given sets of constraints S and T, if , \(S \subseteq T\), and , then .

The proof of Lemma 4 is similar to that of Lemma 3 and is omitted.

Lemmas 3 and 4 allow us to use the powerset manager to replace some of the satisfiability checks during shrinking and growing sub-routines.

The sub-routine. Comparing the subsequent with the sub-routine, before checking satisfiability of (Line 3) and (Line 6), we first check if these subsets are unexplored. Lemma 3 ensures that if they are already explored, they are satisfiable.

figure d

The sub-routine. The following returns either a new MSS or a new MUS. It is based on the routine showed earlier.

figure e

Similar to the sub-routine, before checking satisfiability for (Line 3), the sub-routine checks if it is unexplored. Lemma 4 ensures that if is already explored, it is unsatisfiable. Moreover, the fact that is unexplored guarantees that (Line 6) returns a new MUS.

Example 3

An example execution trace for the algorithm (using and ) applying to the set of output constraints for the rules – in Example 1 is below.

figure f

4.3 Comparing and

The main novelty of compared to is the use of the powerset manager for checking satisfiability of the problem constraints. In particular, the powerset manager allows to produce MUSes even in the case where the original seed is satisfiable, where must always produce MSSes. For our purpose of enumerating MUSes, finding a MUS is more valuable than MSS. When a MUS is found, blocks both its super-sets as well as subsets, where only blocks the super-sets of MUS. As a result, prunes the search space much faster than . Comparing the traces for and in Examples 2 and 3, does not need to find all MSSes before termination. In fact MSSes found by such as and are spurious, i.e., they are subset of the MUS , and does not require to be considered in searching for MUSes. For , MUS can be also added as a lower bound. Focusing on enumerating MUSes without finding all MSSes was mentioned as future work in [10].

5 Empirical Analysis

We implement our algorithms for finding MUSes and MISes using Java. In particular, for constraint solving (i.e., for the powerset manager and for satisfiability checks of the problem constraints), we use SMTInterpol [8]. We first compare the performance of the and algorithms (Sect. 5.1). Afterwards, we evaluate the performance of developed MISes finder program with using examples extracted from real-world policies (Sect. 5.2).

5.1 vs.

Both algorithms were implemented using the same underlying infrastructure, sharing as much code as possible. For growing and shrinking, uses and sub-routines, whereas uses and sub-routines. Both algorithms use a powerset manager built on top of SMTInterpol without any modification, e.g., it is not biased towards producing large unexplored sets (which will be beneficial for ). The experiments were performed on a VMWare Virtual Machine with 4 \(\times \) 2.7 GHz CPUs running Linux. Each program was executed with 3 GB heap memory limit and an 1800-second timeout. There is no timeout for individual constraints satisfiability check. We selected 473 samples (from 4 to 881 constraints) selected from SMT-LIB for quantifier-free linear integer arithmetic (QF_LIA).Footnote 2 Even though our algorithm is constraint-agnostic, we have chosen the QF_LIA fragment of the SMT-LIB benchmarks since the input and output constraints of our rule verification case studies are within this sub-logic. We also restrict our evaluation to the sets of benchmarks where the SMT solver (SMTInterpol in our implementation) can verify their satisfiability in a reasonable time. We plan to evaluate our algorithm against other benchmarks in the future.

Overall. The summary of the results for running the two algorithms is in Table 1. While the numbers of cases where the algorithms terminate and find all MUSes are comparable, tends to run out of memory (hitting bad seeds) whereas tends to run out of time (making too many expensive SMT calls) more often. However, in most cases, usually finds more MUSes than . In particular, does not find any MUSes in over 20 % of the samples (105 cases), whereas that percentage for is 6 % (21 cases). This is the direct effect of : it can produce MUSes even in the case where the original seed is satisfiable. On average, found almost twice as many MUSes as .

Table 1. Empirical analysis summary
Full size table

Comparing the number of SMT calls for checking satisfiability of the problem constraints and SAT calls for the powerset manager, there is a clear difference between the two programs. makes heavy use of the powerset manager as a substitute for checking satisfiability of the problem constraints. Even though ’s total number of satisfiability calls is twice as many as that of , solving satisfiability problems in the powerset manager (related to Boolean constraints) are much faster than checking satisfiability of the problem constraints, which are (in our experiments) QF_LIA constraints.

Performance comparison between and is as follows.

figure h

We separate the benchmarks into two categories according to whether or not both algorithms terminate and find all MUSes. In the first case, an algorithm is better if it terminates faster. In the second case, we compare the number of MUSes that the algorithms found. Overall, outperforms by terminating faster or finding more MUSes (82 %).

Both programs terminate. The comparison between the (log-scale) speed of and in the case where they both terminate can be seen in Fig. 5a. In most cases (97 %), terminates faster than . Figure 6 compares the percentage of MUSes found against the time, both scaled to the range 0 . . 1 for samples that and terminate. For , it is typical that the MUSes are found early then subsequently, only MSSes are found. For , in most cases, MUSes are found gradually.

Fig. 5.
figure 5

Running time and MUSes found comparison

Full size image
Fig. 6.
figure 6

MUSes found vs. time

Full size image

One of the programs does not terminate. We focus on the number of MUSes found by each algorithm. In 76 % of cases, found more MUSes than . Figure 5b shows the comparison between the numbers of MUSes found by and for individual sample.

5.2 MISes Finder

We evaluate the MISes finder program on the following examples. With the exception of the first one, all of them are extracted from industrial case studies in financial and public sectors. The statistics can be seen as follows.

Example

Size

Time

MUSes

MSSes

MISes

SATs

SMTs

Test sample

8

195 ms

5

12

3

78

57

Vehicle insurance

4

69 ms

2

1

1

9

15

Care insurance

15

403 ms

62

0

10

106

335

Vehicle tax

108

13.4 s

2590

2

0

7223

19345

Registration

725

1800 s

436

1093

0

820455

373767

The performance of the MISes finder program largely depend on the underlying algorithm on finding MUSes of the output constraints. The last two examples (namely Vehicle tax and Registration) are consistent. However, MISes finder program does not terminate for the Registration example, fails to verify the rule base. In this case, all 436 MUSes (none of them are MISes) are found within 60 s. Afterwards, the program only found MSSes. Given the size of the rule base, we do not expect the program found all MSSes within a reasonable time. To validate this set of rules, we need to adopt some additional techniques to reduce the complexity of the problem.

6 Conclusion

In this paper, we present our approach for validating the consistency of specification rules describing the relationship between the system input and expected output. Our method explores the relationship between MISes of rules and MUSes of constraints. We developed a novel algorithm for fast enumeration of MUSes during the validation process and evaluated it against  [10], a state-of-the-art algorithm for enumerating MUSes. Our approach is constraint-agnostic and makes use of constraints solvers as black-boxes. Furthermore, we make use of the well-known routines such as and sub-routines to find MUSes and MSSes. Any state-of-the-art implementation for these sub-routines can be used within our algorithm. Since our algorithm relying on SMT solvers for satisfiability checking, consistency verification of specifications rules will be limited by the capability of the underlying SMT solvers.

Related work. The similarity between specification rules and production rules [7] is in their composition: Each rule is composed of a guard (input constraints) and an action (output constraints). The main difference between them is the fact that specification rules can be non-deterministic while production rules are deterministic. Furthermore, the purpose of specification rules is to stipulate the relationships between input and output of the system, hiding the system state. The production rules often involve systems with explicit state (the working memory). Production rules are also written with some implicit rule execution engine in mind, e.g., firing enabled rules repeatedly. In term of validation, different properties have been considered for production rules [14]. Due to their deterministic nature, minimal inconsistency for production rules can only be pairwise.

In a more general context, Rule-Based Systems (RBSes) have been used in the field of Artificial Intelligence and Knowledge Engineering [12] for knowledge representation. Typically, an RBS contains a rule set and an inference control mechanism including some conflict resolution strategy. Each rule imitates logical implication and is used for backward or forward reasoning. Furthermore the conflict resolution strategies ensure that in the case where two or more rules can be activated at a time, only one is selected according to some pre-defined criteria. This is also the main difference between RBSes and the specification rules under our consideration. Verification of RBSes is also extensively discussed in [12]. A taxonomy of verifiable characteristics for RBSes is proposed concerning various anomalies such as consistency, completeness, and (non-)redundancy. In particular, the problem of conflicting and inconsistent rules are considered to be special cases of nondeterminism and is deferred to the conflict resolution mechanism. In fact, in some special representation of RBSes such as tabular systems with no explicit negation, purely logical inconsistency never appears [12].

In order to find all MISes of a set of rules, we need to find all MUSes of its output constraints. Comparison in [10] suggests the algorithm [11] can out-perform the algorithm in finding all MUSes. The disadvantage of is its inability to “enumerate” the MUSes, i.e., it can take a long time before outputting any MUS. Hence is unsuitable for any application where incremental responses are required. However, its ability of finding all MUSes quickly can be useful to validate a consistent set of rules. We plan to investigate and evaluate further.

Future work. Other properties for specification rules include redundancy and completeness. Similar to consistency, the problem of verifying redundancy and completeness can also be reduced to enumerating MUSes and this is the next logical step of our research. As mentioned before in Sect. 5.2, for the Registration example, our MISes finder program does not terminate. The main challenge is in the size of the example (725 rules). A possible solution for validating this set of rule is to syntactically decompose this set of rules into smaller sets. Rule separation will drastically reduce the complexity of the MISes finding problem, hence could be used as a pre-processing step for the current MISes finder program. Moreover, the specification rules can be combined to stipulate system requirements. We are currently investigating how consistency validation can be composed/decomposed for such specification of combined rule bases.

Currently, our implementation uses SMTInterpol [8] as the underlying solver of the powerset manager and for checking satisfiability of the problem constraints. While this is sufficient for our purpose, it would be of our interests to investigate other SMT solvers in place of SMTInterpol. Another possible improvement for our implementation is to take advantage of the incremental checking and backtracking ability of SMT solvers (i.e., using operations).

Parallelism has been considered for extracting a MUS [5, 15]. In a similar fashion, the problem of enumerating MUSes and MISes can take advantage of parallel and/or distributed architectures. In particular, enumeration of MUSes can be parallelised and distributed to a cluster. The essential point to consider is how to correctly and effectively use the powerset manager. Our formal model suggests that having a parallel/distributed version of the program is possible.

Parallel/distributed version of the program is also a solution to another limitation of the current MISes finder program. Currently, our MISes finder program will terminate (without finding all MISes) if the underlying SMT solver cannot solve a satisfiability problem (i.e., return unknown). This is often the case when the solver gets a “bad seed” such that its performance is deteriorated. By trying to solve several seeds at once, the MISes program can proceed even if some of the seeds are bad. Moreover, if the bad seeds are not MUSes or MSSes, the program can even terminate finding all MISes.

Often rule bases are developed step-by-step and subject to regular changes. It is necessary for the consistency validation to be carried out in an incremental fashion, where checks are only required to perform on the parts of the rule base that are affected by the changes. This is important for building a practical tool set supporting the development of specification rules.

The correctness of our MISes finder program relies on the separation between input and output constraints, in particular, the output constraints does not refer to any input variable. This is sufficient to model several regulations and policies. In the case where the output constraints refer to the input variables, our program does not guarantee to find all MISes for a rule base. What can be inferred is that any result of the program is an inconsistent set of rules (not necessarily minimal). Further investigation is required to validate this general type of rules, in particular, to consider solving constraints with quantifiers.