Reasoning with minimal models is at the heart of many knowledge representation systems. Yet, it turns out that this task is formidable even when very simple theories are considered. It is, therefore, crucial to be able to break this task into several subtasks that can be solved separately and in parallel. We show that minimal models of positive propositional theories can be decomposed based on the structure of the dependency graph of the theories. This observation can be useful for many applications involving computation with minimal models. As an example of such benefits, we introduce new algorithms for minimal model finding and checking that are based on model decomposition. The algorithms' temporal worst-case complexity is exponential in the size s of the largest connected component of the dependency graph, but their actual cost depends on the size of the largest source actually encountered, which can be far smaller than s, and on the class of theories to which sources belong. Indeed, if all sources reduce to an HCF or HEF theory, the algorithms are polynomial in the size of the theory.
5; 2]. In particular, a recent work [
This work looks for methods to decompose a theory into disjoint subsets of clauses, such that the formidable task of minimal model computation is split between subsets of the original theory. We do so by investigating the relationship between a propositional theory and its super-dependency graph. We show that a minimal model of a theory can be generated by first computing, separately and in parallel, the minimal models of the theories corresponding to sources of the graph and then by computing the minimal models of the rest of the theory, after propagating the assignment to variables by the minimal models computed at the sources. Regarding the opposite direction, we show that given a minimal model, if its projection on a source is a minimal model of the theory corresponding to the source, then the rest of the model is a minimal model of the theory updated by the content of the minimal model computed at the sources.
To demonstrate the merits of theory decomposition, we present two new algorithms- one for minimal model generation and one for minimal model checking. The basic idea of the model generation algorithm is to compute the minimal models bottom to up while traversing the graph source following source. Intuitively, the algorithm starts with an empty model and iteratively adds to it “necessary” atoms. When a source in the graph is encountered during the computation, first the algorithm calls an external procedure like, for example, IGEA, to compute a minimal model of the sub-theory induced by that source. In many cases, this external computation will successfully terminate in polynomial time. Clearly enough, any algorithm possibly proposed in the future might be plugged into the algorithmic schema to ameliorate its performance. The model checking algorithm works in a way opposite to the model finding algorithm. It starts with a model, and it decomposes the model and the theory until both become empty, which means the model is, indeed, a minimal model of the given theory.
Noteworthy, almost all the studies mentioned above
indicate that the source of intractability in minimal model
finding stems from the presence of head-loops in the dependency
graphs of the theories. In fact, in HCF theories no such a
loop occurs, whereas in HEF theories only specific kinds of
loops are allowed. Starting from this, the work reported in
this manuscript presents an algorithm that finds a minimal
model of any positive theory in time exponential in the size
of the largest head-loop that induces a sub-theory on which
the incomplete algorithm of [
Note that our decomposition strategy has three related advantages: (i) even if our algorithm resorts to an exponentialtime complete procedure, the procedure will be executed on just one loop and not on the whole theory, (ii) even if a theory is initially neither HEF nor HCF, while considering loops from bottom to up it may hold that a sub-theory induced by a specific loop is either HEF or HCF; this is due to the fact that the forward propagation of values of resolved atoms towards forward components may decrease their complexity, and (iii) models of theories associated with sources of the graph can be computed in parallel and then combined with the rest of the theory. 2
We focus on propositional theories. We will refer to a theory as a set of clauses of the form a1 ^ a2 ^ ::: ^ am c1 _ c2 _ ::: _ cn (1) where all the a’s and the c’s are atoms1. We assume that all the c’s are different. The expression to the left of is called the body of the clause, while the expression to the right of is called the head of the clause. We will sometimes denote a clause by B H, where B is the set of atoms in the body of the clause and H the set of atoms in its head. A clause is disjunctive if n > 1. A theory is called positive if, for every clause, n > 0. From now on, when we refer to a theory it is a positive theory.
Let X be a set of atoms. X satisfies the body of a clause if and only if all the atoms in the body of the clause belong to X. X violates a clause if and only if X satisfies the body of the clause, but none of the atoms in the head of the clause belongs to X. X is a model of a theory if none of its clauses is violated by X. A model X of a theory T is minimal if there is no Y X, which is also a model of T . Note that positive theories always have at least one minimal model.
With every theory T we associate a directed graph, called the dependency graph of T , in which (a) each atom and each clause in T is a node, and (b) there is an arc directed from a node a to a clause if and only if a is in the body of . There is an arc directed from to a if a is in the head of 2.
A super-dependency graph SG is an acyclic graph built from a dependency graph G as follows: for each strongly connected component c in G, there is a node in SG, and for each 1Note that the syntax of (1) is a bit unusual for a clause; usually, the equivalent notation :a1 _ :a2 _ ::: _ :am _ c1 _ c2 _ ::: _ cn is employed.
2Clause nodes in the dependency graph are mandatory to achieve a graph which is linear in the size of the theory. arc in G from a node in a strongly connected component c1 to a node in a strongly connected component c2 there is an arc in SG from the node associated with c1 to the node associated with c2. A theory T is Head-Cycle-Free (HCF) if there are no two atoms in the head of some clause in T that belong to the same component in the super-dependency graph of T [3].
A source in a directed graph is a node with no incoming edges. By abuse of terminology, we will sometimes use the term “source” as the set of atoms in the source. A source in a propositional theory will serve as a shorthand for “a source in the super dependency graph of the theory.” A source is called empty if the set of atoms in it is empty. Given a source S of a theory T , TS denotes the set of clauses in T that uses only atoms from S.
Our algorithms use function Reduce(T; X; Y ) which resembels many reasoning methods in knowledge representation, like, for example, unit propagation in DPLL and other constraint satisfaction algorithms[10; 12]. Reduce returns the theory obtained from T where all atoms in X are set to true and all atoms in Y are set to false. More specifically, Reduce returns the theory obtained by first removing all clauses that contain atoms in X in the head and atoms in Y in the body, and second removing all remaining atoms in X [ Y from T . So, for example, Reduce(fa ^ b c _ d; c d; a dg;fag; fcg) returns the theory fb d; dg. Example 2.1 (Running Example) Suppose we are given the following theory T In this section we show that it is possible to compute a minimal model of a theory T by computing a minimal model of TS for each source S of T , and then propagating the values assigned to atoms in the source to the rest of the theory. We also prove that in some theories, some of the minimal models can be decomposed to minimal models of the sources and minimal models of the rest of the theory.
let G be the SG of T . For any source S in G, let X be a minimal model of TS . Moreover, let T 0 = Reduce(T; X; S X). Then, for any minimal model M 0 of T 0, M 0 [ X is a minimal model of T .
Proof: The proof has two steps. We prove that (1)- (M 0 [ X) is a model of T and (2) - that it is minimal.
1. Assume that (M 0 [ X) is not a model of T . Then, there is a rule : B H in T whose body B is fully contained in (M 0 [ X), and the head H has empty intersection with (M 0 [ X). Note that is not in TS . Otherwise it would not be violated by (M 0 [ X), since X is a model of TS , and no atom in TS is in M 0.
Since B is fully contained in (M 0 [ X), B can always be written as (BM0 [ BX ), where BM0 = (B \ M 0), BX = (B \ X), and BM0 \ BX = ;. Analogously, since H has empty intersection with (M 0 [ X), it can always be written as H0 [ HS X , where HS X = (H \ (S X)), and H0 is the set of all the other atoms occurring in H.
After executing procedure Reduce(), T 0 will contain the rule 0 : BM0 H0. But, since H has an empty intersection with (M 0 [ X), H0 has an empty intersection with M 0, thus 0 is violated by M 0, and then M 0 is not a model of T 0 which contradicts the hypothesis.
2. Assume that (M 0 [X) is not a minimal model of T , then there is a nonempty set of atoms A, such that (M 0 [ X) A is a model of T . In particular let AX denote the atoms of A belonging to X and AM0 the atoms of A belonging to M 0. For A to be non-empty, AM0 or AX has to be non-empty. We prove that in both cases there is a contradiction. [AX 6= ;] Since X is a minimal model of TS , (X AX ) is not a model of TS . Then, in TS there is a clause S : B H, such that B is fully contained in (X AX ) and no atom of H is in (X AX ). Since S is in TS , by definition of TS no atom of H is outside S, and then no atom of H is in M 0. Thus, S is a clause of TS (and then of T ) whose body is contained in X AX (and then in M 0 [ X) and any atom in the head of is neither in M 0 nor in X. Thus, S is violated by (M 0 [ X) A. Since S 2 T , (M 0 [ X) A is not a model of T , a contradiction. [AM0 6= ;] Since M 0 is a minimal model of T 0, (M 0 AM0 ) is not a model of T 0. Then, there is in T 0 a clause 0 : B H, such that B is fully contained in (M 0 AM0 ) and no atom of H is in (M 0 AM0 ).
By the way Reduce works, there must be in T the clause : (B [ BX ) H [ HS X with BX a possibly empty subset of X and HS X a possibly empty subset of S X. This clause has the body fully contained in (M 0 AM0 ) [ X and then also in (M 0 [ X) A) and no atom of its head is in (M 0 [ X) A. Thus, is violated and (M 0 [ X) A is not a model of T , a contradiction2.
positive theory, let G be the SG of T , and let M be a minimal model of T . Moreover, assume there is a source S in G such that X = M \ S is a minimal model of TS , and let T 0 = Reduce(T; X; S X). Then M X is a minimal model of T 0.
Proof: We first show that M 0 = M X is a model of T 0. Let B H 2 T 0 and assume B M 0. By the way Reduce works, there must be a possibly empty set D such that D X, (B [ D) H 2 T , and H \ X = ;. Since B M 0 and D X, B [ D M , and since M must satisfy the clause (B [ D) H, H M . Since H \ X = ;, H M X. Hence B H is satisfied by M 0. Assume conversely that M X is not a minimal model of T 0. Then there must be a nonempty subset of atoms W , such that M X W is a model of T 0. Note that W \ X = ; and hence X M W . We show that M W is a minimal model of T , a contradiction to M being minimal. Let B H 2 T and assume B M W . We have to show that H \ (M W ) 6= ;. H can be written as H0 [ HX [ HS X , where HX = H \ X, HS X = H \ (S X), and H0 = H S. B can be written as B0 [ BX [ BS X , where BX = B \ X, BS X = B \(S X), and B0 = B S. Since B M W , it must be that BS X = ;. In case HX 6= ;, clearly H \ (M W ) 6= ; because X M W . So assume B H is actually of the form (B0 [BX ) (H0 [HS X ). Hence the clause B0 H0 must belong to T 0. Since B0 M W and B0 \ S = ;, it must be that B0 M X W . Since M X W is a model of T 0, it must be that H0 \ (M X W ) 6= ;. So clearly H0 \ (M W ) 6= ;. Since H0 H, H \ (M W ) 6= ;. 2 4
We now show how the graph-based decompositions presented in the previous section can be exploited for minimal model finding. We first introduce algorithm ModuMin, which can be used to perform model finding.
Algorithm ModuMin uses the function head . Given a clause , head returns the set of all atoms belonging to the head of . The algorithm works on the super-dependency graph of the theory, from bottom to up. It starts with the empty set as a minimal model and adds to it atoms only when proved to be necessary to build a model.
Theorem 4.1 Algorithm ModuMin is correct: it outputs a minimal model of the input theory.
The following example demonstrates how ModuMin works. Example. Suppose that the theory T of Example 2.1 is given as input to ModuMin. At Step 1 of ModuMin, M := ;. The condition in the If statement at Step 3 is false and we jump to the Else section in Step 6. The graph G shown in Figure 1 is built, and in Step 8 the two sources containing 1 and 3, respectively, are removed from the graph because they are empty. At Step 9, we have to choose a source in G. We can choose either b or c.
d _ e _ f 1. If we choose b: S is set to fbg and in Step 10, TS is the empty set, and so in Step 11, X is empty. In Step 12, M is still empty, and by calling Reduce(T; ;; fbg), T becomes: 1 : a 3 : a _ c 4 : a 5 : e f 6 : f e
Input: A positive theory T
Output: A minimal model for T 1 M := ; ; 2 while T 6= ; do 3 if There is a clause in T violated by M such that jhead( )j = 1 then 4 : d _ e _ f 5 : 6 : Now we go again to the While condition in Step 2. Since T is not empty, we check the If condition in Step 3. The condition is false, and we jump to the Else section in Step 6. The graph G of T is built. In Step 8 the source containing 4 is removed from the graph because it is empty. At Step 9 we have to choose a source in G.
We can choose between two sources : fdg, and fe; f g. 1.1 If we choose fdg: In this case TS is empty and so is X. In Step 12 M is still fag. After we run Reduce(T; ;; fdg), T becomes:
4 : e _ f 5 : e f 6 : f e Now we are left with only one source, fe; f g. TS is T . TS has only one minimal model which is fe; f g. So M is set to fa; e; f g. Since now T becomes empty, the algorithm terminates returning fa; e; f g as a minimal model of the input theory. 1.2 When we choose fe; f g: In this case TS = fe f , f eg, and the only minimal model of TS is the empty set. So in Step 12 nothing is added to M . After running Reduce(T; ;; fe; f g), T becomes a theory with only one clause, d. We then go to Step 3. In Step 4 M becomes fa; dg. Since now T becomes empty, the algorithm terminates returning fa; dg as a minimal model of the input theory. 2. If we choose c: S is set to fcg. In Step 10 TS is the empty set, so in Step 11 X is empty. In Step 12 M is still empty. By calling Reduce(T; ;; fcg), T becomes: 1 : a _ b 2 : b a 3 : a 4 : a d _ e _ f 5 : e f 6 : f e Now we go to Step 2. Since T is not empty, we go to Step 3. The condition of the if statement is true, and we set X = fag and M = fag. After running Reduce(T; fag; ;), T becomes the following theory:
As far as the complexity of ModuMin is concerned, initially the dependency graph associated with the whole theory is considered. This graph and the related super-dependency graph can be built in linear time with respect to the size of the theory. At each iteration of the algorithm one connected component S is taken into account. At the end of each iteration the atoms in S are deleted from the theory. Thus, the number of iterations is at most linear with the theory size. As for the cost of a single iteration, it depends on the cost of computing a minimal model of the theory TS induced by the source S considered. If, at each iteration, TS is such that IGEA successfully outputs a minimal model, the cost of the whole algorithm is polynomial with respect to the size of the input theory. Conversely, if for one theory TS IGEA fails, an exponential procedure should be adopted to find a minimal model of TS and then the computational cost of the algorithm is exponential in the size of the largest connected component on which IGEA fails.
Summarizing, let n be the size of a theory T , s the size of the largest connected component, and k be the number of connected components in the dependency graph of T . The cost of ModuMin is upper bounded by
tMuobduMin(n) = O(n + k 2s): 5
In this section we show how the ideas of algorithm ModuMin can be adopted to solving the minimal model checking problem. The minimal model checking problem is defined as follows: Given a theory T and a model M , check whether M is a minimal model of T .
Algorithm CheckMin in Figure 2 can be used to check whether a model M of a theory T is a minimal model. It works through the super dependency graph of T , and it recursively deletes from M sets of atoms that are minimal models of the sources of T . T is reduced after each such deletion, to reflect the minimal models found for the sources. This process goes on until T shrinks to the empty set. When this happens, we check if M has shrunk to be the empty set as well. If this is the case, we conclude that M is indeed a minimal model of T .
As an example, suppose Algorithm CheckMin is given theory T from Example 2.1 and the model M = fa; dg. The algorithm considers the super-dependency graph G in Figure 1 bottom to up. First it removes the empty sources 1 and 3, and then it checks whether there is a source S, such that S \ M is a minimal model of TS. The source fbg is a good candidate because Tfbg is empty, (there are no clauses in T written with the atom b only), M \ fbg = ;, and the empty set is a minimal model of the empty set of clauses. So following the commands inside the While loop, M does not change, T shrinks to be: 1 : a 3 : a _ c 4 : a d _ e _ f 5 : e f 6 : f e and the source fbg is removed from the graph. Then the source 2 is removed from G, because it is an empty source. We now have two sources: fag and f g
c . M \ fag = fag and fag is indeed a minimal model of Tfag which is 1 : a. So, following the commands inside the While loop, M shrinks to be fdg, and T shrinks to be: 4 : d _ e _ f 5 : e f 6 : f e and the sources fag and fcg are removed from the graph. Next, we delete the source f 4g because it is an empty source. We are left with two sources: fdg and fe; f g. The source fe; f g is a good candidate because Tfe;fg is f 5; 6g, M \ fe; f g = ;, and the empty set is a minimal model of the theory that consists of 5 and 6. Following the commands inside the While loop, M does not change, and T shrinks to be a theory that consists of the clause d. fdg is the only source left in the graph and M \ fdg = fdg is the only minimal model of d. Following the commands inside the While loop, both M and T shrink to be the empty set, and the algorithm terminates returning true. The proof of the following theorem is straightforward given the correctness of the algorithm ModuMin. It is also clear that the time complexity of CheckMin is the same as the time complexity of ModuMin.
Theorem 5.1 If algorithm CheckMin returns true when given a theory T and a model of T ,M , then M is a minimal model of T .
In this section we discuss the benefits and the limitations of the algorithms presented.
An important question is, “Can algorithm ModuMin generate any minimal model of a given input theory T ?” The answer is that while ModuMin is guaranteed to return a minimal model, for some theories there are minimal models that will never be generated by ModuMin. Consider the following example.
Example 6.1 Let T 0 be the theory fc; c b_a, a d,d cg. This theory has two minimal models: fc; bg and fc; a; dg. However, in the graph of the theory the component fc; a; dg precedes the component fbg, and therefore algorithm ModuMin will always pick the component fc; a; dg before it picks the component f g b . Therefore the minimal model fc; a; dg will never be generated by ModuMin. Moreover, if the algorithm CheckMin gets as input the theory T 0 and the minimal model fc; bg, it will return true. However, when given T 0 and the model fc; a; dg, CheckMin will return false.
Clearly, there are theories for which ModuMin is complete. An example is theory T from Example 2.1. We have shown in Example 1 that all its minimal models can be generated. It would be useful to identify the class of theories for which ModuMin is complete. We will now define a subset of theories for which algorithms ModuMin and CheckMin are complete. Note that such a subset is orthogonal to the known class of HCF theories, because the theory T 0 above, for which the algorithms are not complete, is HCF, while the theory T from Example 2.1 is not HCF, and for T the algorithms are complete.
The question remains if we can find cases in which the algorithms will be complete. We provide a partial answer here, and leave the rest for further investigations.
We first define recursively a property called the Modular property.
Definition 6.2 1. A minimal model M of a positive theory T has the Modular property with respect to T , if the SG of T has only one component. 2. A minimal model M of a positive theory T has the Modular property with respect to T , if there is a source S in T such that X = M \ S is a minimal model of TS , and M X, which is a minimal model of T 0 = Reduce(T; X; S X) according to Theorem 3.2, has the Modular property with respect to T 0.
Theorem 6.3 Let T be the theory which is input into the algorithm ModuMin. If every minimal model of T has the modular property w.r.t. T , then ModuMin is complete for T . Theorem 6.4 Assume the theory T and a minimal model M of T are given as input to the algorithm CheckMin. If M has the modular property w.r.t. T , then CheckMin will return true.
Theorems 6.3 and Theorem 6.4 give us a useful analysis of the cases in which the algorithms presented in this manuscript are complete. They guide us to look for subclasses of theories with respect to which any minimal model has the modular property. One example is theories that have the OSH Property, defined next.
ory T has the one-source-head (OSH) Property if there is a source S in T such that for every atom P 2 S, if P is in the head of some clause in T , then all the other atoms in the head of are also in S.
Consider, for example, Theory T from Example 6.1. This theory does not have the OSH property. The SG of T has only two sources, and the clause c b _ a has atoms from both components.
Theories having the OSH property are useful for completeness: Theorem 6.6 If a theory T has the OSH property, then for every minimal model M of T there is a sourse S in T such that X = M \ S is a minimal model of TS .
Proof: Assume T has the OSH property. Then there is a source S such that for every P 2 S, if P is in the head of some clause in T , then all other atoms in the head of are also in S. Let M be a minimal model of T . We show that X = M \ S is a minimal model of TS . Since M is a model of T , it is clear that X is a model of TS . We show that X is minimal. Assume conversely that X is not minimal. Then there must be a noempty set of atoms W X S such that X W is a model of TS . We show that M W is a model of T , a contradiction of M being minimal. Let (B H) 2 T . If H \ S 6= ;. Since T has the OSH property, H S, and since S is a source, it must be the case that (B H) 2 TS , and since X W is a model of TS and X W M W , clearly M W satisfies (B H). So assume H \ S = ;, and assume B M W . It follows that B M . Since M is a model of T , M \ H 6= ;. Since H \ S = ; and W S, it follows that (M W ) \ H 6= ;. So M W is a model of T , a contradiction. 2 Corollary 6.7 Assume T has the OSH property, let M be a minimal model of T , let S be a source such that X = M \ S is a minimal model of TS (note that by Theorem 6.6 there is such S), and let T 0 = Reduce(T; X; S X). If M X (which is a minimal model of T 0 according to Theorem 3.2) has the modular property w.r.t. T 0, then M can be generated by ModuMin.
Corollary 6.8 Assume T has the OSH property, let M be a minimal model of T , let S be a source such that X = M \ S is a minimal model of TS (note that by Theorem 6.6 there is such S), and let T 0 = Reduce(T; X; S X). If M X (which is a minimal model of T 0 according to Theorem 3.2) has the modular property w.r.t. T 0, then CheckMin will return true when given T and M as input. The notion of OSH property has practical implications. If T and all the smaller and smaller theories generated by algorithm CheckMin while working on a the input theory T and a candidate minimal model M has the OSH property, then it can be certain that CheckM in will return true if and only if M is a minimal model of T . Since the OSH property can be checked in linear time, we can easily check whether it holds for the theories generated during the execution of CheckMin. 7
Many papers deal with complexity issues that rise due to the
cycles in the dependency graphs of theories. There were also
attempts to exploit parallelism to compute answer sets, but
a different approach than here have been used [
The algorithms presented in this paper are based on an idea
that appears in [
In [
The dlv system described in [25; 23] also make use of program decomposition based on the strongly connected components of the dependency graph. However, they do not split the program to subprograms having disjoint sets of atoms. As a result, the upper bound for the algorithm complexity that we show here is not achieved.
The author of [2] presents a hierarchy of tractable subsets for computing stable models, which are minimal models. The idea is to exploit the structure of the theory as is reflected in its super-dependency graph, but a different algorithm is used. There are several main differences between the work of [2] and the current one. First, while we deal with disjunctive theories, that paper is about non-disjunctive ones. Second, the graph is built in a different manner. Third, the complexity estimate in [2] yields sometimes a higher complexity. Fourth, the decomposition used does not yield subtheories that are completely independent of each other. Atoms in theories that correspond to different strongly connected components may overlap.
In sum, while past algorithms for computing minimal model did make efforts to exploit the structure of the dependency graph of the theory, they did not manage to decompose the theory to totally independent sub-theories that can be computed in parallel as we do here. Hence past algorithms did not achieve the complexity analysis that we provide here, which shows that the complexity of model finding is exponential in the size of the largest strongly connected component of the dependency graph of the theory. 8
We have presented methods for decomposing minimal models of positive propositional theories based on the dependency graph of the theory. We have shown how those decomposing techniques can lead to efficient minimal model finding and checking for these theories.
It has long been realized that the source of complexity in computing minimal models of theories is the loops between atoms that lie in the heads of disjunctive clauses. Algorithm ModuMin presented in this paper enables us to compute minimal models in time complexity that is directly dependent on the size of the disjunctive head loops. ModuMin has other virtues as well. First, it is possible to achieve in linear time, before the computation, a non-trivial upper-bound for the time it would take to compute a minimal model of the theory. Second, since any atom that is added to the output model M is guaranteed to be part of a minimal model, we can answer some queries related to this atom before the whole model is computed. Third, while working bottom-up, we can employ AI search methods for picking the next source to compute. For example, assume each atom has a value, and we need to compute a minimal model such that the sum of values of atoms in the model is below some threshold. We can use branch and bound approach to do this.