Decomposing Minimal Models Rachel Ben-Eliyahu-Zohary Fabrizio Angiulli, Fabio Fassetti and Luigi Palopoli Azrieli College of Engineering, DIMES, University of Calabria, DIMES, University of Calabria, Jerusalem, Israel Rende, Italy Rende, Italy rbz@jce.ac.il f.angiulli@dimes.unical.it {fassetti, palopoli}@dimes.unical.it Abstract 5; 2]. In particular, a recent work [1] shows how it is possi- ble to construct minimal models of positive theories by an Reasoning with minimal models is at the heart of incomplete algorithm, called IGEA, that always converges in many knowledge representation systems. Yet, it polynomial time by either declaring success or failure, while turns out that this task is formidable even when very it is guaranteed to end successfully at least on the class of simple theories are considered. It is, therefore, cru- HEF theories [16], which forms a significant strict superclass cial to be able to break this task into several sub- of HCF theories [3]. tasks that can be solved separately and in parallel. We show that minimal models of positive propo- This work looks for methods to decompose a theory into sitional theories can be decomposed based on the disjoint subsets of clauses, such that the formidable task of structure of the dependency graph of the theories. minimal model computation is split between subsets of the This observation can be useful for many applica- original theory. We do so by investigating the relationship be- tions involving computation with minimal models. tween a propositional theory and its super-dependency graph. As an example of such benefits, we introduce new We show that a minimal model of a theory can be generated algorithms for minimal model finding and check- by first computing, separately and in parallel, the minimal ing that are based on model decomposition. The models of the theories corresponding to sources of the graph algorithms’ temporal worst-case complexity is ex- and then by computing the minimal models of the rest of the ponential in the size s of the largest connected com- theory, after propagating the assignment to variables by the ponent of the dependency graph, but their actual minimal models computed at the sources. Regarding the op- cost depends on the size of the largest source ac- posite direction, we show that given a minimal model, if its tually encountered, which can be far smaller than projection on a source is a minimal model of the theory corre- s, and on the class of theories to which sources be- sponding to the source, then the rest of the model is a minimal long. Indeed, if all sources reduce to an HCF or model of the theory updated by the content of the minimal HEF theory, the algorithms are polynomial in the model computed at the sources. size of the theory. To demonstrate the merits of theory decomposition, we present two new algorithms- one for minimal model gener- ation and one for minimal model checking. The basic idea 1 Introduction of the model generation algorithm is to compute the minimal The tasks of minimal model finding and checking are central models bottom to up while traversing the graph source fol- in Artificial Intelligence (AI). These computational tasks are lowing source. Intuitively, the algorithm starts with an empty at the heart of several knowledge representation systems, in- model and iteratively adds to it “necessary” atoms. When a cluding circumscription [28; 29; 27], default logic [30], mini- source in the graph is encountered during the computation, mal diagnosis [11; 32], planning [21], multi-agents coordina- first the algorithm calls an external procedure like, for exam- tion [20], and logic programs under stable model semantics ple, IGEA, to compute a minimal model of the sub-theory [17; 6; 13]. induced by that source. In many cases, this external compu- Reasoning with minimal models has been the subject of tation will successfully terminate in polynomial time. Clearly several studies in the AI community [8; 7; 24; 14; 9; 3; 25; enough, any algorithm possibly proposed in the future might 4; 22; 18; 1]. Given a theory T , the Minimal Model Finding be plugged into the algorithmic schema to ameliorate its per- task consists of computing a minimal model of T , whereas the formance. The model checking algorithm works in a way op- Minimal Model Checking task is concerned with the problem posite to the model finding algorithm. It starts with a model, of checking whether a given set of atoms is indeed a minimal and it decomposes the model and the theory until both be- model of T . Both tasks have been proven to be intractable come empty, which means the model is, indeed, a minimal even if only positive theories are considered [8; 7]. Therefore, model of the given theory. we deem it relevant and interesting to single out classes of Noteworthy, almost all the studies mentioned above indi- theories for which these problems can be solved efficiently [1; cate that the source of intractability in minimal model find- ing 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 [1] fails. In particular, when run on HEF theories, our algorithm is guaranteed to find a mini- mal model in polynomial time. Note that our decomposition strategy has three related ad- vantages: (i) even if our algorithm resorts to an exponential- time complete procedure, the procedure will be executed on just one loop and not on the whole theory, (ii) even if a the- ory 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) Figure 1: The [super]dependency graph of the theory T . models of theories associated with sources of the graph can be computed in parallel and then combined with the rest of arc in G from a node in a strongly connected component c1 to the theory. a node in a strongly connected component c2 there is an arc in SG from the node associated with c1 to the node associated 2 Preliminaries with c2 . A theory T is Head-Cycle-Free (HCF) if there are We focus on propositional theories. We will refer to a theory no two atoms in the head of some clause in T that belong to as a set of clauses of the form the same component in the super-dependency graph of T [3]. A source in a directed graph is a node with no incoming a1 ∧ a2 ∧ ... ∧ am ⊃ c1 ∨ c2 ∨ ... ∨ cn (1) edges. By abuse of terminology, we will sometimes use the 1 where all the a’s and the c’s are atoms . We assume that all term “source” as the set of atoms in the source. A source in a the c’s are different. The expression to the left of ⊃ is called propositional theory will serve as a shorthand for “a source in the body of the clause, while the expression to the right of ⊃ the super dependency graph of the theory.” A source is called is called the head of the clause. We will sometimes denote a empty if the set of atoms in it is empty. Given a source S of clause by B ⊃ H, where B is the set of atoms in the body a theory T , TS denotes the set of clauses in T that uses only of the clause and H the set of atoms in its head. A clause is atoms from S. disjunctive if n > 1. A theory is called positive if, for every Our algorithms use function Reduce(T, X, Y ) which re- clause, n > 0. From now on, when we refer to a theory it is a sembels many reasoning methods in knowledge representa- positive theory. tion, like, for example, unit propagation in DPLL and other Let X be a set of atoms. X satisfies the body of a clause constraint satisfaction algorithms[10; 12]. Reduce returns if and only if all the atoms in the body of the clause belong the theory obtained from T where all atoms in X are set to X. X violates a clause if and only if X satisfies the body to true and all atoms in Y are set to false. More specifi- of the clause, but none of the atoms in the head of the clause cally, Reduce returns the theory obtained by first removing belongs to X. X is a model of a theory if none of its clauses all clauses that contain atoms in X in the head and atoms is violated by X. A model X of a theory T is minimal if there in Y in the body, and second removing all remaining atoms is no Y ⊂ X, which is also a model of T . Note that positive in X ∪ Y from T . So, for example, Reduce({a ∧ b ⊃ c ∨ theories always have at least one minimal model. d, c ⊃ d, a ⊃ d},{a}, {c}) returns the theory {b ⊃ d, ⊃ d}. With every theory T we associate a directed graph, called Example 2.1 (Running Example) Suppose we are given the the dependency graph of T , in which (a) each atom and each following theory T clause in T is a node, and (b) there is an arc directed from a δ1 : a∨b δ2 : b⊃a δ3 : a∨c node a to a clause δ if and only if a is in the body of δ. There δ4 : a ⊃ d∨e∨f δ5 : e⊃f δ6 : f ⊃e 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 In Figure 1 the dependency graph of T is illustrated in solid lines. from a dependency graph G as follows: for each strongly con- The nodes of the SG are marked with dotted lines. The arcs of the nected component c in G, there is a node in SG, and for each SG converge with the arcs of the dependency graph except the arcs going out of node δ4 , which are marked with dotted lines. 1 Note that the syntax of (1) is a bit unusual for a clause; usually, the equivalent notation ¬a1 ∨ ¬a2 ∨ ... ∨ ¬am ∨ c1 ∨ c2 ∨ ... ∨ cn 3 Modular properties of minimal models is employed. 2 In this section we show that it is possible to compute a min- Clause nodes in the dependency graph are mandatory to achieve a graph which is linear in the size of the theory. imal model of a theory T by computing a minimal model of TS for each source S of T , and then propagating the values Theorem 3.2 (Minimal model decomposition) Let T be a assigned to atoms in the source to the rest of the theory. We positive theory, let G be the SG of T , and let M be a min- also prove that in some theories, some of the minimal mod- imal model of T . Moreover, assume there is a source S in els can be decomposed to minimal models of the sources and G such that X = M ∩ S is a minimal model of TS , and let minimal models of the rest of the theory. T 0 = Reduce(T, X, S −X). Then M −X is a minimal model of T 0 . Theorem 3.1 (Theory decomposition) Let T be a theory, let G be the SG of T . For any source S in G, let X be a min- Proof: We first show that M 0 = M − X is a model of imal model of TS . Moreover, let T 0 = Reduce(T, X, S − X). T . Let B ⊃ H ∈ T 0 and assume B ⊆ M 0 . By the way 0 Then, for any minimal model M 0 of T 0 , M 0 ∪ X is a minimal Reduce works, there must be a possibly empty set D such model of T . that D ⊆ X, (B ∪ D) ⊃ H ∈ T , and H ∩ X = ∅. Since Proof: The proof has two steps. We prove that (1)- (M 0 ∪ B ⊆ M 0 and D ⊆ X, B ∪ D ⊆ M , and since M must X) is a model of T and (2) - that it is minimal. satisfy the clause (B ∪ D) ⊃ H, H ⊆ M . Since H ∩ X = ∅, H ⊆ M − X. Hence B ⊃ H is satisfied by M 0 . Assume 1. Assume that (M 0 ∪ X) is not a model of T . Then, there conversely that M − X is not a minimal model of T 0 . Then is a rule δ : B ⊃ H in T whose body B is fully contained there must be a nonempty subset of atoms W , such that M − in (M 0 ∪ X), and the head H has empty intersection with X − W is a model of T 0 . Note that W ∩ X = ∅ and hence (M 0 ∪ X). Note that δ is not in TS . Otherwise it would not X ⊆ M − W . We show that M − W is a minimal model of be violated by (M 0 ∪ X), since X is a model of TS , and no T , a contradiction to M being minimal. Let B ⊃ H ∈ T and atom in TS is in M 0 . assume B ⊆ M − W . We have to show that H ∩ (M − W ) 6= Since B is fully contained in (M 0 ∪ X), B can always be ∅. H can be written as H 0 ∪ HX ∪ HS−X , where HX = written as (BM 0 ∪ BX ), where BM 0 = (B ∩ M 0 ), BX = H ∩ X, HS−X = H ∩ (S − X), and H 0 = H − S. B can be (B ∩ X), and BM 0 ∩ BX = ∅. Analogously, since H has written as B 0 ∪ BX ∪ BS−X , where BX = B ∩ X, BS−X = empty intersection with (M 0 ∪ X), it can always be written B ∩(S −X), and B 0 = B −S. Since B ⊆ M −W , it must be as H 0 ∪ HS−X , where HS−X = (H ∩ (S − X)), and H 0 is that BS−X = ∅. In case HX 6= ∅, clearly H ∩ (M − W ) 6= ∅ the set of all the other atoms occurring in H. because X ⊆ M − W . So assume B ⊃ H is actually of the After executing procedure Reduce(), T 0 will contain the form (B 0 ∪BX ) ⊃ (H 0 ∪HS−X ). Hence the clause B 0 ⊃ H 0 rule δ 0 : BM 0 ⊃ H 0 . But, since H has an empty intersection must belong to T 0 . Since B 0 ⊆ M − W and B 0 ∩ S = ∅, it with (M 0 ∪ X), H 0 has an empty intersection with M 0 , thus must be that B 0 ⊆ M −X −W . Since M −X −W is a model δ 0 is violated by M 0 , and then M 0 is not a model of T 0 which of T 0 , it must be that H 0 ∩ (M − X − W ) 6= ∅. So clearly contradicts the hypothesis. H 0 ∩ (M − W ) 6= ∅. Since H 0 ⊆ H, H ∩ (M − W ) 6= ∅. 2 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 4 Minimal model finding belonging to X and AM 0 the atoms of A belonging to M 0 . We now show how the graph-based decompositions presented For A to be non-empty, AM 0 or AX has to be non-empty. We in the previous section can be exploited for minimal model prove that in both cases there is a contradiction. finding. We first introduce algorithm ModuMin, which can be [AX 6= ∅] Since X is a minimal model of TS , (X − AX ) is used to perform model finding. not a model of TS . Then, in TS there is a clause δS : Algorithm ModuMin uses the function head . Given a clause B ⊃ H, such that B is fully contained in (X − AX ) δ, head returns the set of all atoms belonging to the head of and no atom of H is in (X − AX ). Since δS is in TS , δ. The algorithm works on the super-dependency graph of by definition of TS no atom of H is outside S, and then the theory, from bottom to up. It starts with the empty set as a no atom of H is in M 0 . Thus, δS is a clause of TS (and minimal model and adds to it atoms only when proved to be then of T ) whose body is contained in X −AX (and then necessary to build a model. in M 0 ∪ X) and any atom in the head of δ is neither in Theorem 4.1 Algorithm ModuMin is correct: it outputs a M 0 nor in X. Thus, δS is violated by (M 0 ∪ X) − A. minimal model of the input theory. Since δS ∈ T , (M 0 ∪ X) − A is not a model of T , a contradiction. The following example demonstrates how ModuMin works. [AM 0 6= ∅] Since M 0 is a minimal model of T 0 , (M 0 − AM 0 ) Example. Suppose that the theory T of Example 2.1 is given as is not a model of T 0 . Then, there is in T 0 a clause δ 0 : input to ModuMin. At Step 1 of ModuMin, M := ∅. The condition B ⊃ H, such that B is fully contained in (M 0 − AM 0 ) in the If statement at Step 3 is false and we jump to the Else section and no atom of H is in (M 0 − AM 0 ). 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 By the way Reduce works, there must be in T the the graph because they are empty. At Step 9, we have to choose a clause δ : (B ∪ BX ) ⊃ H ∪ HS−X with BX a possibly source in G. We can choose either b or c. empty subset of X and HS−X a possibly empty subset 1. If we choose b: S is set to {b} and in Step 10, TS is the empty of S − X. This clause has the body fully contained in set, and so in Step 11, X is empty. In Step 12, M is still empty, (M 0 − AM 0 ) ∪ X and then also in (M 0 ∪ X) − A) and no and by calling Reduce(T, ∅, {b}), T becomes: atom of its head is in (M 0 ∪ X) − A. Thus, δ is violated δ1 : a δ3 : a ∨ c and (M 0 ∪ X) − A is not a model of T , a contradiction. 2 δ4 : a ⊃ d ∨ e ∨ f δ5 : e ⊃ f δ6 : f ⊃ e Algorithm 1: Algorithm ModuMin Algorithm 2: Algorithm CheckMin Input: A positive theory T Input: A positive theory T and a model M of T Output: A minimal model for T Output: true or false 1 Let G be the super-dependency graph of T ; 1 M := ∅ ; 2 Recursively delete from G all the empty sources; 2 while T 6= ∅ do 3 while There is a source S in G such that M ∩ S is a minimal 3 if There is a clause δ in T violated by M such that |head(δ)| = 1 then model of TS do 4 X := M ∩ S; M := M − X; 4 let X := head(δ); M := M ∪ X ; T := Reduce(T, X, (S − X)); 5 T := Reduce(T, X, ∅) ; G := the super dependency graph of T ; 6 else 5 Recursively delete from G all the empty sources; 7 let G be the super-dependency graph of T ; 8 Iteratively delete from G all the empty sources ; 6 if M = ∅ then 9 let S be the set of atoms in a source of G ; 7 return true 10 let TS be the subset of T containing all the clauses 8 else from T having only atoms from S; 9 return false 11 let X be a minimal model of TS ; 12 M := M ∪ X ; 13 T := T − TS ; T := Reduce(T, X, S − X); It is easy to see that taking steps as in previous cases, there are 14 return M two minimal models that the algorithm might return: {a, d} and {a, e, f }. 2 Now we go again to the While condition in Step 2. Since T is not empty, we check the If condition in Step 3. In As far as the complexity of ModuMin is concerned, ini- Step 4 we set X = {a} and M = {a} and after running tially the dependency graph associated with the whole theory Reduce(T, {a}, ∅), T becomes the following theory: is considered. This graph and the related super-dependency δ4 : d ∨ e ∨ f δ5 : e ⊃ f δ6 : f ⊃ e graph can be built in linear time with respect to the size of Now we go again to the While condition in Step 2. Since T the theory. At each iteration of the algorithm one connected is not empty, we check the If condition in Step 3. The condi- component S is taken into account. At the end of each iter- tion is false, and we jump to the Else section in Step 6. The ation the atoms in S are deleted from the theory. Thus, the graph G of T is built. In Step 8 the source containing δ4 is re- moved from the graph because it is empty. At Step 9 we have number of iterations is at most linear with the theory size. to choose a source in G. As for the cost of a single iteration, it depends on the cost We can choose between two sources : {d}, and {e, f }. of computing a minimal model of the theory TS induced by the source S considered. If, at each iteration, TS is such that 1.1 If we choose {d}: In this case TS is empty and so is X. In IGEA successfully outputs a minimal model, the cost of the Step 12 M is still {a}. After we run Reduce(T, ∅, {d}), whole algorithm is polynomial with respect to the size of the T becomes: input theory. Conversely, if for one theory TS IGEA fails, an δ4 : e ∨ f δ 5 : e ⊃ f δ 6 : f ⊃ e exponential procedure should be adopted to find a minimal Now we are left with only one source, {e, f }. TS is T . TS has only one minimal model which is {e, f }. So M model of TS and then the computational cost of the algorithm is set to {a, e, f }. Since now T becomes empty, the algo- is exponential in the size of the largest connected component rithm terminates returning {a, e, f } as a minimal model on which IGEA fails. of the input theory. Summarizing, let n be the size of a theory T , s the size 1.2 When we choose {e, f }: In this case TS = {e ⊃ f , of the largest connected component, and k be the number of f ⊃ e}, and the only minimal model of TS is the empty connected components in the dependency graph of T . The set. So in Step 12 nothing is added to M . After run- cost of ModuMin is upper bounded by ning Reduce(T, ∅, {e, f }), T becomes a theory with only one clause, d. We then go to Step 3. In Step 4 tub s ModuMin (n) = O(n + k · 2 ). M becomes {a, d}. Since now T becomes empty, the al- gorithm terminates returning {a, d} as a minimal model 5 Minimal model checking of the input theory. 2. If we choose c: S is set to {c}. In Step 10 TS is the empty set, In this section we show how the ideas of algorithm ModuMin so in Step 11 X is empty. In Step 12 M is still empty. By can be adopted to solving the minimal model checking prob- calling Reduce(T, ∅, {c}), T becomes: lem. The minimal model checking problem is defined as fol- δ1 : a ∨ b δ2 : b ⊃ a δ3 : a lows: Given a theory T and a model M , check whether M is δ4 : a ⊃ d ∨ e ∨ f δ5 : e ⊃ f δ6 : f ⊃ e a minimal model of T . Now we go to Step 2. Since T is not empty, we go to Step 3. Algorithm CheckMin in Figure 2 can be used to check The condition of the if statement is true, and we set X = {a} whether a model M of a theory T is a minimal model. It and M = {a}. After running Reduce(T, {a}, ∅), T becomes works through the super dependency graph of T , and it recur- the following theory: sively deletes from M sets of atoms that are minimal models δ4 : d ∨ e ∨ f δ5 : e ⊃ f δ6 : f ⊃ e of the sources of T . T is reduced after each such deletion, to reflect the minimal models found for the sources. This pro- in Example 1 that all its minimal models can be generated. cess goes on until T shrinks to the empty set. When this hap- It would be useful to identify the class of theories for which pens, we check if M has shrunk to be the empty set as well. ModuMin is complete. We will now define a subset of theories If this is the case, we conclude that M is indeed a minimal for which algorithms ModuMin and CheckMin are complete. model of T . Note that such a subset is orthogonal to the known class of As an example, suppose Algorithm CheckMin is given theory T HCF theories, because the theory T 0 above, for which the al- from Example 2.1 and the model M = {a, d}. The algorithm con- gorithms are not complete, is HCF, while the theory T from siders the super-dependency graph G in Figure 1 bottom to up. First Example 2.1 is not HCF, and for T the algorithms are com- it removes the empty sources δ1 and δ3 , and then it checks whether plete. there is a source S, such that S ∩ M is a minimal model of TS . The The question remains if we can find cases in which the al- source {b} is a good candidate because T{b} is empty, (there are no clauses in T written with the atom b only), M ∩ {b} = ∅, and the gorithms will be complete. We provide a partial answer here, empty set is a minimal model of the empty set of clauses. So fol- and leave the rest for further investigations. lowing the commands inside the While loop, M does not change, T We first define recursively a property called the Modular shrinks to be: property. δ1 : a δ3 : a ∨ c δ4 : a ⊃ d ∨ e ∨ f δ5 : e ⊃ f δ 6 : f ⊃ e Definition 6.2 1. A minimal model M of a positive theory and the source {b} is removed from the graph. Then the source T has the Modular property with respect to T , if the SG δ2 is removed from G, because it is an empty source. We now have of T has only one component. two sources: {a} and {c}. M ∩ {a} = {a} and {a} is indeed a 2. A minimal model M of a positive theory T has the Mod- minimal model of T{a} which is δ1 : a. So, following the com- ular property with respect to T , if there is a source S mands inside the While loop, M shrinks to be {d}, and T shrinks in T such that X = M ∩ S is a minimal model of to be: δ4 : d ∨ e ∨ f δ5 : e ⊃ f δ6 : f ⊃ e and the TS , and M − X, which is a minimal model of T 0 = sources {a} and {c} are removed from the graph. Next, we delete Reduce(T, X, S −X) according to Theorem 3.2, has the the source {δ4 } because it is an empty source. We are left with two Modular property with respect to T 0 . sources: {d} and {e, f }. The source {e, f } is a good candidate be- The following theorems hold: cause T{e,f } is {δ5 , δ6 }, M ∩ {e, f } = ∅, and the empty set is a minimal model of the theory that consists of δ5 and δ6 . Following Theorem 6.3 Let T be the theory which is input into the al- the commands inside the While loop, M does not change, and T gorithm ModuMin. If every minimal model of T has the mod- shrinks to be a theory that consists of the clause d. {d} is the only ular property w.r.t. T , then ModuMin is complete for T . source left in the graph and M ∩ {d} = {d} is the only minimal Theorem 6.4 Assume the theory T and a minimal model M model of d. Following the commands inside the While loop, both of T are given as input to the algorithm CheckMin. If M M and T shrink to be the empty set, and the algorithm terminates has the modular property w.r.t. T , then CheckMin will return returning true. The proof of the following theorem is straight- true. forward given the correctness of the algorithm ModuMin. It is also clear that the time complexity of CheckMin is the same Theorems 6.3 and Theorem 6.4 give us a useful analysis of as the time complexity of ModuMin. the cases in which the algorithms presented in this manuscript are complete. They guide us to look for subclasses of theories Theorem 5.1 If algorithm CheckMin returns true when with respect to which any minimal model has the modular given a theory T and a model of T ,M , then M is a minimal property. One example is theories that have the OSH Prop- model of T . erty, defined next. 6 Completeness Definition 6.5 (one-source-head (OSH) Property) A the- In this section we discuss the benefits and the limitations of ory T has the one-source-head (OSH) Property if there is a the algorithms presented. source S in T such that for every atom P ∈ S, if P is in the An important question is, “Can algorithm ModuMin gen- head of some clause δ in T , then all the other atoms in the erate any minimal model of a given input theory T ?” The head of δ are also in S. answer is that while ModuMin is guaranteed to return a min- imal model, for some theories there are minimal models that Consider, for example, Theory T from Example 6.1. This will never be generated by ModuMin. Consider the following theory does not have the OSH property. The SG of T has example. only two sources, and the clause c ⊃ b ∨ a has atoms from Example 6.1 Let T 0 be the theory {c, c ⊃ b∨a, a ⊃ d,d ⊃ c}. This both components. theory has two minimal models: {c, b} and {c, a, d}. However, in Theories having the OSH property are useful for complete- the graph of the theory the component {c, a, d} precedes the com- ness: ponent {b}, and therefore algorithm ModuMin will always pick the component {c, a, d} before it picks the component {b}. Therefore Theorem 6.6 If a theory T has the OSH property, then for the minimal model {c, a, d} will never be generated by ModuMin. every minimal model M of T there is a sourse S in T such Moreover, if the algorithm CheckMin gets as input the theory T 0 that X = M ∩ S is a minimal model of TS . and the minimal model {c, b}, it will return true. However, when Proof: Assume T has the OSH property. Then there is given T 0 and the model {c, a, d}, CheckMin will return false. a source S such that for every P ∈ S, if P is in the head of Clearly, there are theories for which ModuMin is complete. some clause δ in T , then all other atoms in the head of δ are An example is theory T from Example 2.1. We have shown 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 in a way that is different from what we present here and the of T , it is clear that X is a model of TS . We show that X paper deal with normal logic programs and not with disjunc- is minimal. Assume conversely that X is not minimal. Then tive ones. there must be a noempty set of atoms W ⊆ X ⊆ S such that The dlv system described in [25; 23] also make use of pro- X − W is a model of TS . We show that M − W is a model of gram decomposition based on the strongly connected compo- T , a contradiction of M being minimal. Let (B ⊃ H) ∈ T . nents of the dependency graph. However, they do not split the If H ∩ S 6= ∅. Since T has the OSH property, H ⊆ S, and program to subprograms having disjoint sets of atoms. As a since S is a source, it must be the case that (B ⊃ H) ∈ TS , result, the upper bound for the algorithm complexity that we and since X − W is a model of TS and X − W ⊆ M − W , show here is not achieved. clearly M − W satisfies (B ⊃ H). So assume H ∩ S = ∅, The author of [2] presents a hierarchy of tractable subsets and assume B ⊆ M − W . It follows that B ⊆ M . Since M for computing stable models, which are minimal models. The is a model of T , M ∩ H 6= ∅. Since H ∩ S = ∅ and W ⊆ S, idea is to exploit the structure of the theory as is reflected in it follows that (M − W ) ∩ H 6= ∅. So M − W is a model of its super-dependency graph, but a different algorithm is used. T , a contradiction. 2 There are several main differences between the work of [2] Corollary 6.7 Assume T has the OSH property, let M be a minimal and the current one. First, while we deal with disjunctive model of T , let S be a source such that X = M ∩ S is a minimal theories, that paper is about non-disjunctive ones. Second, model of TS (note that by Theorem 6.6 there is such S), and let the graph is built in a different manner. Third, the complexity T 0 = Reduce(T, X, S − X). If M − X (which is a minimal model estimate in [2] yields sometimes a higher complexity. Fourth, of T 0 according to Theorem 3.2) has the modular property w.r.t. T 0 , the decomposition used does not yield subtheories that are then M can be generated by ModuMin. completely independent of each other. Atoms in theories that Corollary 6.8 Assume T has the OSH property, let M be a minimal correspond to different strongly connected components may model of T , let S be a source such that X = M ∩ S is a minimal overlap. model of TS (note that by Theorem 6.6 there is such S), and let In sum, while past algorithms for computing minimal T 0 = Reduce(T, X, S − X). If M − X (which is a minimal model model did make efforts to exploit the structure of the depen- of T 0 according to Theorem 3.2) has the modular property w.r.t. T 0 , dency graph of the theory, they did not manage to decom- then CheckMin will return true when given T and M as input. pose the theory to totally independent sub-theories that can The notion of OSH property has practical implications. If T be computed in parallel as we do here. Hence past algorithms and all the smaller and smaller theories generated by algo- did not achieve the complexity analysis that we provide here, rithm CheckMin while working on a the input theory T and which shows that the complexity of model finding is exponen- a candidate minimal model M has the OSH property, then it tial in the size of the largest strongly connected component of can be certain that CheckM in will return true if and only if the dependency graph of the theory. M is a minimal model of T . Since the OSH property can be checked in linear time, we can easily check whether it holds 8 Conclusions for the theories generated during the execution of CheckMin. We have presented methods for decomposing minimal mod- 7 Related Work els of positive propositional theories based on the dependency graph of the theory. We have shown how those decomposing Many papers deal with complexity issues that rise due to the techniques can lead to efficient minimal model finding and cycles in the dependency graphs of theories. There were also checking for these theories. attempts to exploit parallelism to compute answer sets, but It has long been realized that the source of complexity in a different approach than here have been used [15]. In this computing minimal models of theories is the loops between section we discuss only the most relevant work that was not atoms that lie in the heads of disjunctive clauses. Algorithm mentioned in previous sections. ModuMin presented in this paper enables us to compute min- The algorithms presented in this paper are based on an idea imal models in time complexity that is directly dependent that appears in [26], where the authors show that in many on the size of the disjunctive head loops. ModuMin has cases a logic program can be divided into two parts. Our other virtues as well. First, it is possible to achieve in lin- algorithm, using the superstructure of the dependency graph, ear time, before the computation, a non-trivial upper-bound exploits a specific method for splitting the program. The work for the time it would take to compute a minimal model of of [19] is also about splitting a program into several modules the theory. Second, since any atom that is added to the out- to gain advantages in software development. The authors of put model M is guaranteed to be part of a minimal model, that paper have also found that strongly connected compo- we can answer some queries related to this atom before the nents of the dependency graph provide a key criterion when whole model is computed. Third, while working bottom-up, it comes to confining program composition. Our work is dif- we can employ AI search methods for picking the next source ferent, as it focuses on computational issues and provides spe- to compute. For example, assume each atom has a value, and cific complexity results. Another difference is that the mod- we need to compute a minimal model such that the sum of ules suggested in [19] overlap, while we split the program values of atoms in the model is below some threshold. We into disjoint sets of clauses. can use branch and bound approach to do this. In [31] the authors employ minimal model checking of strongly connected components while computing stable mod- els of logic programs. However, the program is decomposed References [17] M. Gelfond and V. Lifschitz. Classical negation in logic [1] F. Angiulli, R. Ben-Eliyahu-Zohary, F. Fas- programs and disjunctive databases. New Generation setti, and L. Palopoli. On the tractability Computing, 9:365–385, 1991. of minimal model computation for some cnf [18] E. Giunchiglia and M. Maratea. Sat-based planning theories. Artificial Intelligence, 2014. doi: with minimal-#actions plans and ”soft” goals. In AI*IA, http://dx.doi.org/10.1016/j.artint.2014.02.003. pages 422–433, 2007. [2] R. Ben-Eliyahu. A hierarchy of tractable subsets for [19] T. Janhunen, E. Oikarinen, H. Tompits, and S. Woltran. computing stable models. J. Artif. Intell. Res. (JAIR), Modularity aspects of disjunctive stable models. Jour- 5:27–52, 1996. nal of Artificial Intelligence Research, pages 813–857, [3] R. Ben-Eliyahu and R. Dechter. On computing minimal 2009. models. Annals of Mathematics and Artificial Intelli- [20] M. Kalech and G. A. Kaminka. On the design of coordi- gence, 18:3–27, 1996. nation diagnosis algorithms for teams of situated agents. [4] R. Ben-Eliyahu-Zohary. An incremental algorithm for Artificial Intelligence, 171(8):491–513, 2007. generating all minimal models. Artificial Intelligence, [21] H. A. Kautz, D. Mcallester, and B. Selman. Encoding 169(1):1–22, 2005. Plans in Propositional Logic. In Proceedings of the Fifth [5] R. Ben-Eliyahu-Zohary and L. Palopoli. Reasoning International Conference on the Principle of Knowledge Representation and Reasoning (KR’96), pages 374– with minimal models: Efficient algorithms and appli- 384, 1996. cations. Artificial Intelligence, 96(2):421–449, 1997. [22] L. M. Kirousis and P. G. Kolaitis. The complex- [6] N. Bidoit and C. Froidevaux. Minimalism subsumes de- ity of minimal satisfiability problems. Inf. Comput., fault logic and circumscription in stratified logic pro- 187(1):20–39, 2003. gramming. In Proceedings of the IEEE symposium on logic in computer science, pages 89–97, June 1987. [23] C. Koch, N. Leone, and G. Pfeifer. Enhancing disjunc- tive logic programming systems by sat checkers. Artifi- [7] M. Cadoli. The complexity of model checking for cir- cial Intelligence, 151(1):177–212, 2003. cumscriptive formulae. Inf. Process. Lett., 44(3):113– 118, 1992. [24] P. G. Kolaitis and C. H. Papadimitriou. Some computa- tional aspects of circumscription. J. ACM, 37(1):1–14, [8] M. Cadoli. On the complexity of model finding for non- 1990. monotonic propositional logics. In Proceedings of the 4th Italian conference on theoretical computer science, [25] N. Leone, P. Rullo, and F. Scarcello. Disjunctive stable pages 125–139. World Scientific Publishing Co., Octo- models: Unfounded sets, fixpoint semantics, and com- ber 1992. putation. Inf. Comput., 135(2):69–112, 1997. [9] Z. Chen and S. Toda. The complexity of selecting maxi- [26] V. Lifschitz and H. Turner. Splitting a logic program. In mal solutions. In Proc. 8th IEEE Int. Conf. on Structures ICLP, volume 94, pages 23–37, 1994. in Complexity Theory, pages 313–325, 1993. [27] V. Lifshitz. Computing circumscription. In IJCAI-85: [10] M. Davis, G. Logemann, and D. Loveland. A machine Proceedings of the international joint conference on AI, program for theorem-proving. Communications of the pages 121–127, 1985. ACM, 5(7):394–397, 1962. [28] J. McCarthy. Circumscription - a form of non- [11] J. de Kleer, A. K. Mackworth, and R. Reiter. Charac- monotonic reasoning. Artificial Intelligence, 13:27–39, terizing diagnoses and systems. Artificial Intelligence, 1980. 56(2-3):197–222, 1992. [29] J. McCarthy. Application of circumscription to formal- [12] R. Dechter. Constraint processing. Morgan Kaufmann, izing common-sense knowledge. Artificial Intelligence, 2003. 28:89–116, 1986. [13] C. Drescher, M. Gebser, T. Grote, B. Kaufmann, [30] R. Reiter. A logic for default reasoning. Art. Int., 13(1– A. König, M. Ostrowski, and T. Schaub. Conflict-driven 2):81–132, 1980. disjunctive answer set solving. KR, 8:422–432, 2008. [31] P. Simons, I. Niemelä, and T. Soininen. Extending and [14] T. Eiter and G. Gottlob. Propositional circumscription implementing the stable model semantics. Artificial In- and extended closed-world reasoning are iip2-complete. telligence, 138(1):181–234, 2002. Theor. Comput. Sci., 114(2):231–245, 1993. [32] R. T. Stern, M. Kalech, A. Feldman, and G. M. Provan. [15] M. Gebser, B. Kaufmann, and T. Schaub. Advanced Exploring the duality in conflict-directed model-based conflict-driven disjunctive answer set solving. In IJCAI, diagnosis. In AAAI, 2012. 2013. [16] M. Gebser, J. Lee, and Y. Lierler. Elementary sets for logic programs. In Proceedings of the 21st National Conference on Artificial Intelligence (AAAI), 2006.