On the Difference of Horn Theories^{∗}

Thomas Eiter Institut und Ludwig Wittgenstein Labor für Informationssysteme, Technische Universität Wien, Favoritenstraße 9–11, A-1040 Wien, Austria. (eiter@kr.tuwien.ac.at)

Toshihide Ibaraki Department of Applied Mathematics and Physics, Graduate School of Informatics, Kyoto University, Kyoto 606, Japan. (ibaraki@kuamp.kyoto-u.ac.jp)

Kazuhisa Makino Department of Systems and Human Science, Graduate School of Engineering Science, Osaka University, Toyonaka, Osaka 560, Japan (makino@sys.es.osaka-u.ac.jp)

April 27, 2000

∗An extended abstract of this paper appears in Proceedings of the 16th International Symposium on Theoretical Aspects of Computer Science (STACS ’99), Germany, March 4-6, 1999 [8]. The authors gratefully acknowledge the partial support of the Scientific Grant in Aid by the Ministry of Education, Sports, Science and Culture of Japan. Part of this research was conducted while the first author visited Kyoto University in 1995 and 1998, by the support of the Scientific Grant in Aid by the Ministry of Education, Sports, Science and Culture of Japan (Grant 06044112).

Running head: On the Difference of Horn Theories

Mailing address:

Kazuhisa MAKINO Department of Systems and Human Science, Graduate School of Engineering Science, Osaka University, Toyonaka, Osaka 560, Japan. E-mail: makino@sys.es.osaka-u.ac.jp Phone: +81-6-6850-6388 Fax: +81-6-6850-6341

Abstract

In this paper, we consider computing the difference between two Horn theories. This problem may arise, for example, if we take care of a theory change in a knowledge base. In general, the difference of Horn theories is not Horn. Therefore, we consider Horn approximations of the difference in terms of Horn cores (i.e., weakest Horn theories included in the difference) and the Horn envelope (i.e., the strongest Horn theory containing the difference), which have been proposed and analyzed extensively in the literature. We study the problem under the familiar representation of Horn theories by Horn CNFs, as well as under the recently proposed model-based representation in terms of the characteristic models. For all problems and representations, polynomial time algorithms or proofs of intractability for the propositional case are provided; thus, our work gives a complete picture of the tractability/intractability frontier in the propositional Horn theories.

1 Introduction

When we use logical formulas for representing a certain problem, it is in general necessary that different formulas are combined in way to obtain a more comprehensive and accurate description of the problem. Among the basic operations for combining logical formulas are the Boolean operations, i.e., conjunction ∧, disjunction ∨, and complement ¬. In this paper, we consider another basic operation, the difference \, which can represent the complement ¬ (because ¬Σ can be represented by the difference of {0, 1}^{n} and Σ, i.e., {0, 1}^{n} \ Σ, for a theory Σ ⊆ {0, 1}^{n}), and can be represented by the complement ¬ and conjunction ∧ (because Σ_{1} \ Σ_{2} = Σ_{1} ∧ \overline{Σ}_{2} for theories Σ_{1}, Σ_{2} ⊆ \{0, 1\}^{n}, where ∧ is regarded as the set operation ∩). In principle, all these operations are easily accomplished, since the language of propositional logic provides the boolean connectives ∧, ∨, and ¬ (or \), which can be readily applied to combine formulas as desired. However, there are two obstacles to this immediate approach in practice. One obstacle is that the problem description is frequently required to be in a special format. A predominant such format is conjunctive normal form (CNF), i.e., a logical theory Σ is represented by a set of clauses. Another is the model-based format, where a theory is represented by characteristic models. Combining two theories Σ_{1} and Σ_{2} in some format may then require that the result is also cast to the same format. For example, if Σ_{1} and Σ_{2} are represented by CNFs φ_{1} and φ_{2}, respectively, then we can easily obtain the formula φ_{1} \ φ_{2} ≡ φ_{1} ∧ \overline{φ}_{2} of the difference Σ_{1} \ Σ_{2}. Namely, it is represented by the conjunction of the CNF φ_{1} and the disjunctive normal form (DNF) φ_{3}, where φ_{3} is the formula obtained from \overline{φ}_{2} by De Morgan’s law. However, φ_{1} ∧ \overline{φ}_{2} is not a CNF, and moreover we do not know how to efficiently compute the CNF representation from it. Another obstacle is computational complexity. As is well-known, even in propositional logic, the satisfiability problem of a CNF is NP-complete. In trading expressiveness for tractability, theories have been restricted to fragments of the full language. A most important such fragment is the class of Horn theories. Fields such as Logic Programming and Deductive Databases are based on their appealing semantical and computational properties, cf. [11]. In fact, deduction of a clause from a propositional Horn theory is possible in linear time [5], while this is co-NP-complete in general. In this paper, we study the problem of computing the Boolean difference between two Horn theories Σ_{1} and Σ_{2}, i.e., Σ = Σ_{1} \ Σ_{2}. In general, the resulting theory Σ is not Horn. Therefore, we consider approximating Σ by a Horn theory, in order to maintain the desired closure property. Different such approximations are possible, but Horn cores and the Horn envelope, which have been introduced in [21], appear to be most natural.

A Horn theory Π is a Horn core (or a Horn greatest lower bound) of a theory Σ, if Π is included in Σ, i.e., Π logically implies Σ, and there is no weaker Π of this property. A theory R is the Horn envelope (or the Horn least upper bound) of Σ, if it is the strongest Horn theory R which includes Σ, i.e. Σ logically implies R. While there is more than one Horn core in general, the Horn envelope is always unique. Semantical and computational issues on Horn cores and the Horn envelope have been studied extensively, and a number of results have been obtained, cf. [21, 16, 2, 17, 18, 3, 4, 10, 1]. The main results of the present paper can be summarized as follows.

• We present characterizations of the Horn cores and the Horn envelope of a Horn difference Σ_{1} \ Σ_{2}, which will form a basis of the algorithms discussed in this paper.

• We either present a polynomial time algorithm or prove intractability (unless P=NP) for each of the problems mentioned above. (For a concise overview, see Table 1 in Section 6.)

• Besides the familiar representation in terms of Horn CNFs, we also consider the modelbased representation of Horn theories through their sets of characteristic models [14, 15]. This alternative has also been studied repeatedly, since it offers advantages to formula-based representation in certain cases; see [19, 18, 15, 6] for more details.

• Both formula-based and model-based representations allow polynomial time algorithms for many problems. In some cases, however, formula-based representation is polynomial while model-based representation is intractable, and vice versa. Thus, like with many other problems [15, 19, 6], formula-based and model-based representations complement each other with respect to their tractability/intractability profile.

Our results on the difference of Horn theories have applications in different contexts. On one hand, we extend the results on propositional knowledge base (KB) approximation in [16, 2, 10, 1], by providing a polynomial time algorithm for computing some Horn core of a KB which is expressible as the difference of two Horn theories. This should be compared with the general result [2] that computing a Horn core of a KB described by an arbitrary CNF formula φ is not possible in polynomial time, unless P = NP, and most likely impossible with a constant number of queries to an NP oracle. On the other hand, we establish that computing the Horn envelope of the difference φ_{1} \ φ_{2} is intractable. This complements the results in [17, 18, 16, 3, 4] that computing a Horn CNF of the Horn envelope is difficult from a CNF or the extensional description of an arbitrary theory (i.e., its set of models). (Section 6 contains a more detailed discussion.)

Our results find an application in the area of theory change, which has grown into an important research area within AI during the last decade. Here we consider the case in which the change does not need to be retracted. Taking the difference between Horn theories is meaningful in the following scenario, for example. Assume that we have a Horn theory Σ, which is a description of all the possible worlds of a state of affairs; i.e., the real “world” amounts to one of the models in Σ, say w, but is unknown to us. Suppose that we now obtain the information that a formula φ is false in w. Since w is a categorical description of the world, either ψ or ¬ψ is true in it (but not both), for any formula ψ. Hence, in this case, we conclude that ¬φ is true in w, and thus all models v that satisfy φ can be discarded from Σ. This amounts to updating Σ to Σ_{new} = Σ \ Σ′, where Σ′ is the set of models satisfying φ; if φ is Horn, this gives an instance of our problem. If Σ_{new} is not Horn, its Horn envelope and the collection of all Horn cores provide sound and complete approximations of Σ_{new} in terms of Horn theories. Notice that for inference of Horn formulas, the Horn envelope of Σ_{new} is sound and complete [19, 3]. Our algorithms can be applied in this scenario for computing Σ_{new} or its Horn approximations. Observe that computing a Horn core and the Horn envelope in the context of theory change was studied in [10], in which the theory φ ∘ ψ, given by two Horn CNFs φ and ψ, is studied for some revision operators “∘” (see [13]). However, this is only weakly related to ours, since the operation of taking the difference of φ and ψ was not considered, and moreover, the formula ψ is restricted to be a single Horn clause. The remainder of this paper is structured as follows. The next section recalls elementary concepts and provides basic notations. In Section 3, we consider the problem of deciding whether the difference of Horn formulas is Horn, and computing a representation of it if this is the case. After that, we study in Sections 4 and 5 computing Horn cores and the Horn envelope of the difference, respectively. The final Section 6 gives a discussion of the results and related work, as well as outlines further research issues.

2 Preliminaries

We assume a supply of propositional variables x_{1}, x_{2}, …, x_{n}, where each x_{i} evaluates to either 1 (true) or 0 (false). Negated variables are denoted by \overline{x}_{i}. The x_{i} and \overline{x}_{i} are called literals. A clause is a disjunction c = ℓ_{1} ∨ ⋯ ∨ ℓ_{k} of literals, while a term is a conjunction t = ℓ_{1} ∧ ⋯ ∧ ℓ_{k} of literals. By P (c) and N(c) (resp., P (t) and N(t)) we denote the sets of variables occurring positively and negatively in c (resp., t); ⊥ (resp., ⊤) denotes the empty clause (resp., empty term) representing falsity (resp., truth). A conjunction of clauses φ = ⋀_{i} c_{i} (resp., a disjunction of terms φ = ⋁_{i} t_{i} ) is called a conjunctive normal form (CNF) (resp., disjunctive normal form (DNF)). A model is a vector v ∈ {0, 1}^{n}, whose i-th component is denoted by v_{i}, and a theory is any set Σ ⊆ {0, 1}^{n} of models. The models (0, 0, …, 0) and (1, 1, …, 1) are denoted by 0 and 1, respectively. We use v ≤ w for the usual bitwise ordering of models, i.e., v_{i} ≤ w_{i} for all i = 1, …, n, where 0 ≤ 1. A model v ∈ Σ is minimal in Σ, if there is no w ∈ Σ such that w < v. For any formula φ, let T (φ) = {v ∈ {0, 1}^{n} | φ(v) = 1} be the set of its models. A formula φ represents a theory Σ if T (φ) = Σ. We often do not distinguish a formula from the theory it represents, if no confusion arises. For formulas φ and ψ, we write φ ≤ ψ, if T (φ) ⊆ T (ψ) holds. A nontautological clause c (resp., noncontradictory term t) is an implicate (resp., implicant) of a theory Σ if c(v) = 1 for all v ∈ Σ, i.e., {0, 1}^{n} ⊃ T (c) ⊇ Σ (resp., t(v) = 0 for all v ∉ Σ, i.e., ∅ ⊂ T (t) ⊆ Σ); it is prime, if no proper subclause (resp., subterm) is an implicate (resp., implicant) of Σ. A theory Σ is Horn if Σ = Cl_{∧}(Σ) holds, where Cl_{∧}(S) is the closure of S ⊆ {0, 1}^{n} under bitwise AND (i.e., intersection) of models v and w, denoted by v ⋀ w. Observe that any Horn theory Σ has the least (unique smallest) model, which is given by ⋀_{v∈Σ} v. For a Horn theory Σ, a model v ∈ Σ is called characteristic [14], if v ∉ Cl_{∧}(Σ \ {v}) holds. The set of all characteristic models of Σ, the characteristic set of Σ, is denoted by C^{∗}(Σ). Note that every Horn theory Σ has the unique characteristic set C^{∗}(Σ). For example, the theory Σ = {(0101), (1001), (1000), (0001), (0000)} is Horn, and has C^{∗}(Σ) = {(0101), (1001), (1000)}. A clause c is Horn (resp., negative, positive) if |P (c)| ≤ 1 (resp., |P (c)| = 0, |N(c)| = 0), and a CNF is Horn (resp., negative, positive) if it contains only Horn (resp., negative, positive) clauses. It is well-known that a theory Σ is Horn if and only if it is represented by some Horn CNF, and that all prime implicates of a Horn theory are Horn. A theory is negative (resp., positive), if it is represented by some negative (resp., positive) CNF. Observe that every negative theory is Horn. A Horn theory Σ_{c} is a Horn core of a theory Σ, if Σ_{c} ⊆ Σ holds and no Horn theory Σ′ exists such that Σ_{c} ⊂ Σ′ ⊆ Σ. Observe that, in general, Σ has more than one Horn core; e.g., Σ = {(110), (101)} has two Horn cores Σ_{1} = {(110)} and Σ_{2} = {(101)}, respectively. The Horn envelope of Σ is the Horn theory Σ_{e} ⊇ Σ such that no Horn theory Σ′ with Σ_{e} ⊃ Σ′ ⊇ Σ exists. For the above Σ, its Horn envelope is given by Σ_{e} = {(110), (101), (100)}. As easily seen, the Horn envelope is always unique (in fact, Σ_{e} = Cl_{∧}(Σ)). Let φ be a formula representing a theory Σ, and let φ_{c} and φ_{e} be Horn formulas representing a Horn core and the Horn envelope of Σ, respectively. Then φ_{c} and φ_{e} are also called a Horn core and the Horn envelope of φ, respectively.

3 Horn Property of the Difference

In this section, we consider the problem of deciding whether the difference Σ_{1} \ Σ_{2} of two Horn theories Σ_{1} and Σ_{2} is Horn. In Subsection 3.1, we study the problem under Horn CNF representation of Horn theories, and in Subsection 3.2, the model-based representation. As we will see, the problem is tractable in both cases.

3.1 Formula-based representation

Let φ_{1} = ⋀_{j=1}^{m_{1}} c_{1,j} and φ_{2} = ⋀_{j=1}^{m_{2}} c_{2,j} be Horn CNFs. Then

φ_{1} \ φ_{2} ≡ ⋁_{j=1}^{m_{2}}(φ_{1} ∧ ¬c_{2,j}) = ⋁_{j=1}^{m_{2}}(φ_{1} ∧ t_{2,j}),  (3.1)

where t_{2,j} is the term equivalent to ¬c_{2,j}; e.g., if c_{2,j} = (\overline{x}_{1} ∨ \overline{x}_{2} ∨ x_{3}), then t_{2,j} = x_{1}x_{2}\overline{x}_{3}. Note that each ψ_{j} = φ_{1} ∧ t_{2,j} is a Horn CNF. Hence φ_{1} \ φ_{2} can be represented by the disjunction of m_{2} Horn theories ψ_{j}. It is known [7] that, in general, the problem of checking the Horn property of the disjunction of Horn theories is co-NP-complete. However, we shall show below that the Horn property of the difference of Horn theories can be checked in polynomial time. If φ_{2} ≡ ⊥, then

φ_{1} \ φ_{2} ≡ φ_{1}  (3.2)

clearly holds, and hence the difference is Horn. Otherwise, we compute the least model v in φ_{2}, and separately consider the two cases: (1) φ_{1}(v) = 0 and (2) φ_{1}(v) = 1. Case (1). Since φ_{1} is Horn, there is a Horn clause c^{∗} ∈ φ_{1} such that c^{∗} ≥ φ_{1} and c^{∗}(v) = 0. For a model u, let HC(u) denote the set of all maximal Horn clauses c such that c(u) = 0. E.g., if u = (111000), then HC(u) = \{(\overline{x}_{1}∨\overline{x}_{2}∨\overline{x}_{3}∨x_{4}), (\overline{x}_{1}∨\overline{x}_{2}∨\overline{x}_{3}∨x_{5}), (\overline{x}_{1}∨\overline{x}_{2}∨\overline{x}_{3}∨x_{6})\}. Now, some c in HC(v) satisfies c ≥ c^{∗}(≥ φ_{1}). We claim that if v ≠ 1, then

φ_{1} \ φ_{2} ≡ φ_{1} \ (φ_{2} ∧ x_{i})  (3.3)

holds for the x_{i} which appears in c (i.e., P (c) = {x_{i}}). To prove this, note that (3.3) is equivalent to

φ_{1} ∧ φ_{2} ≡ φ_{1} ∧ φ_{2} ∧ x_{i},  (3.4)

which we shall prove. Clearly φ_{1} ∧ φ_{2} ≥ φ_{1} ∧ φ_{2} ∧ x_{i} holds. For the opposite inequality, since v is the least model of φ_{2} and c ≥ φ_{1} holds, all models w with (φ_{1} ∧φ_{2})(w) = 1 satisfy w_{i} = 1. This means φ_{1} ∧ φ_{2} ≤ φ_{1} ∧ φ_{2} ∧ x_{i}.

On the other hand, if v = 1, then T (φ_{2}) = {1} and

φ_{1} \ φ_{2} ≡ φ_{1}  (3.5)

immediately follows. Case (2). Clearly (φ_{1} \ φ_{2})(v) = 0 holds. Thus, if φ_{1} \ φ_{2} represents a Horn theory, there exists a Horn clause c^{∗} such that c^{∗} ≥ φ_{1} \ φ_{2} and c^{∗}(v) = 0. By the definition of HC(v), some c in HC(v) then satisfies c ≥ c^{∗}(≥ φ_{1} \ φ_{2}). We claim that if v ≠ 1, then

φ_{1} \ φ_{2} ≡ (φ_{1} ∧ c) \ (φ_{2} ∧ x_{i})  (3.6)

holds, where the x_{i} appears in c (i.e., P (c) = {x_{i}}). First note that φ_{1} \ φ_{2} ≡ (φ_{1} ∧ c) \ φ_{2} holds by c ≥ φ_{1} \ φ_{2}. Thus, (3.6) is equivalent to

φ_{1} ∧ c ∧ φ_{2} ≡ φ_{1} ∧ c ∧ φ_{2} ∧ x_{i}.  (3.7)

Then this can be proved similarly to (3.4). On the other hand, if v = 1, then

φ_{1} \ φ_{2} ≡ φ_{1} ∧ c  (3.8)

can be proved in a manner similar to (3.5). Now we can apply the above modifications repeatedly as long as possible. In this process, if φ_{2} = ⊥ or v = 1 holds, then we can conclude that φ_{1} \ φ_{2} is Horn by (3.2), (3.5) or (3.8). If there is no c ∈ HC(v) such that c ≥ φ_{1} \ φ_{2}, then we can conclude that φ_{1} \ φ_{2} is not Horn. In the remaining cases, we apply (3.3) or (3.6) (i.e., φ_{1} is modified to φ_{1} ∧ c in case of (3.6), and φ_{2} is modified to φ_{2} ∧ x_{i} in both cases). Let us show that this procedure halts in finitely many steps. Let v^{(k)} be the least model of φ_{2} in the k-th iteration. Then we can see that

v^{(k)} < v^{(k+1)}  (3.9)

holds for k = 1, 2, . . .. Indeed, in either of Cases (1) and (2), φ_{2} is updated to φ ∧ x_{i} in each iteration, which implies v^{(k)} ≤ v^{(k+1)}. Moreover, since the x_{i} that appears in c ∈ HC(v^{(k)}) satisfies v_{i}^{(k)} = 0 by c(v^{(k)}) = 0, and v_{i}^{(k+1)} = 1 by (φ_{2} ∧ x_{i})(v^{(k+1)}) = 1, we have v^{(k)} < v^{(k+1)}. This implies that the number of iterations (i.e., different v^{(k)}) is at most n + 1. Formally, the algorithm can be written as follows.

Algorithm CHECK-HORN Input: Horn CNFs φ_{1} and φ_{2}.

Output: If φ_{1} \ φ_{2} is a Horn theory Σ, then output a Horn CNF for Σ; otherwise, “No”.

Step 0. ϕ_{1} := φ_{1}; ϕ_{2} := φ_{2};

Step 1. if ϕ_{2} ≡ ⊥ then output ϕ_{1} and halt

else begin compute the least model v of ϕ_{2} if ϕ_{1}(v) = 0 then goto Step 2 else (i.e., ϕ_{1}(v) = 1) goto Step 3

end;

Step 2. if v = 1 then output ϕ_{1} and halt

else begin find a Horn clause c in HC(v) such that c ≥ ϕ_{1}; ϕ_{2} := ϕ_{2} ∧ x_{i}, where P (c) = {x_{i}}; goto Step 1

end;

Step 3. Find a Horn clause c in HC(v) such that c ≥ ϕ_{1} \ ϕ_{2}; if no such c exists then output “No” and halt else begin ϕ_{1} := ϕ_{1} ∧ c;

if v = 1 then output ϕ_{1} and halt else ϕ_{2} := ϕ_{2} ∧ x_{i}, where P (c) = {x_{i}}; goto Step 1

end. □

Example 3.1 Let us apply CHECK-HORN to φ_{1} = (\overline{x}_{1}∨\overline{x}_{2})∧(\overline{x}_{1}∨x_{3})∧(\overline{x}_{2}∨x_{3})∧(\overline{x}_{2}∨x_{4}) and φ_{2} = \overline{x}_{4} ∧ (\overline{x}_{1} ∨ \overline{x}_{3}) ∧ (\overline{x}_{2} ∨ \overline{x}_{3}). As we can check, the theory represented by φ_{1} \ φ_{2} is Σ = {(0111), (1011), (1010), (0011), (0001)}. Let ϕ_{1} := φ_{1} and ϕ_{2} := φ_{2}. Since ϕ_{2} ≢ ⊥ in Step 1, the least model v = (0000) of ϕ_{2} is computed. Since ϕ_{1}(v) = 1, we branch to Step 3. Then HC(v) = {x_{i} | i = 1, 2, …, 4}, and we can check that ϕ_{1} \ ϕ_{2} ≰ x_{i} holds for all i = 1, 2, …, 4. Thus, the algorithm outputs “No” in Step 3. Observe that this is correct, since (1010), (0001) ∈ Σ but (0000) = (1010) ∧ (0001) ∉ Σ, which means that Σ is not Horn. On the other hand, let φ_{1} be as above and φ′_{2} = \overline{x}_{4} ∧ (\overline{x}_{2} ∨ \overline{x}_{3}). In this case, φ_{1} \ φ′_{2} represents Σ′ = {(0111), (1011), (0011), (0001)}. Let ϕ_{1} := φ_{1} and ϕ_{2} := φ′_{2}. Then, in Step 1 the least model is v = (0000), and we again branch to Step 3, where HC(v) is the same as the previous one. Now it holds that φ_{1} \ φ′_{2} ≤ x_{4}. Hence, we update ϕ_{1} to ϕ_{1} = ϕ_{1} ∧ x_{4} and ϕ_{2} to ϕ_{2} ∧ x_{4}. After returning to Step 1, we find that ϕ_{2} ≡ ⊥ now holds.

Hence, the formula

ϕ_{1} = (\overline{x}_{1} ∨ \overline{x}_{2}) ∧ (\overline{x}_{1} ∨ x_{3}) ∧ (\overline{x}_{2} ∨ x_{3}) ∧ (\overline{x}_{2} ∨ x_{4}) ∧ x_{4}
= (\overline{x}_{1} ∨ \overline{x}_{2}) ∧ (\overline{x}_{1} ∨ x_{3}) ∧ (\overline{x}_{2} ∨ x_{3}) ∧ x_{4}

is output. Observe that Σ′ is represented by this ϕ_{1}, and thus the output is correct. □

Theorem 3.1 Let φ_{1} and φ_{2} be Horn CNFs. Then, algorithm CHECK-HORN checks whether φ_{1} \ φ_{2} is Horn in O(n^{4} + n^{3}|φ_{2}| + n^{2}|φ_{1}| + n|φ_{1}||φ_{2}|) time.

Proof. The correctness of algorithm CHECK-HORN follows from the discussion before its description. We thus consider its time complexity. Clearly, Step 0 can be done in O(|φ_{1}| + |φ_{2}|) time. In Step 1, since ϕ_{2} is Horn, we can check if ϕ_{2} ≢ ⊥ (i.e., the satisfiability of ϕ_{2}) and compute the least model v of ϕ_{2} in O(|ϕ_{2}|) time [5]. Then we can compute ϕ_{1}(v) in O(|ϕ_{1}|) time. Note that, in each iteration, ϕ_{1} and ϕ_{2} might be replaced by ϕ_{1} ∧ c and ϕ_{2} ∧ x_{i}, respectively. Since the number of iterations is at most n + 1, we have O(|ϕ_{1}|) = O(|φ_{1}| + n^{2}) and O(|ϕ_{2}|) = O(|φ_{2}| + n). Thus, Step 1 requires totally O(n(|ϕ_{1}| + |ϕ_{2}|)) = O(n^{3} + n(|φ_{1}| + |φ_{2}|)) time. In Step 2, since ϕ_{1} is Horn, we can compute a Horn clause c of the desired property in O(|ϕ_{1}|) = O(n^{2} + |φ_{1}|) time. Updating ϕ_{2} to ϕ_{2} ∧ x_{i} takes O(1) time. Since we have at most n iterations, Step 2 can be executed in O(n^{3} + n|φ_{1}|) time. Let us finally consider Step 3. Note that the difference ϕ_{1} \ ϕ_{2} can be represented by the disjunctions of m_{2} Horn CNFs ψ_{1}, ψ_{2}, …, ψ_{m_{2}}, where m_{2} is the number of clauses in ϕ_{2} (see (3.1)). It is easy to see that c ≥ ϕ_{1} \ ϕ_{2} if and only if c ≥ ψ_{k} for all k. For each k, we can compute the set S_{k} of all (candidate) Horn clauses c ∈ HC(v) such that c ≥ ψ_{k} in O(|ψ_{k}|) time (the clauses are stored by their positive literals; e.g., we simply keep S_{k} = {x_{3}, x_{4}, x_{5}} instead of S_{k} = \{(\overline{x}_{1}∨\overline{x}_{2}∨x_{3}), (\overline{x}_{1}∨\overline{x}_{2}∨x_{4}), (\overline{x}_{1}∨\overline{x}_{2}∨x_{5})\}). Thus by taking the intersection of all S_{k}, we can find a c ∈ HC(v) of the desired property in

O(∑_{k=1}^{m_{2}} |ψ_{k}| + nm_{2}) = O(|ϕ_{1}||ϕ_{2}| + nm_{2}) = O(n^{3} + n^{2}|φ_{2}| + n|φ_{1}| + |φ_{1}||φ_{2}|) (3.10)

time. Furthermore, updating ϕ_{1} and ϕ_{2} can be done in O(n^{2} + |φ_{1}| + |φ_{2}|) time. Thus Step 3 can be done in O(n^{4} + n^{3}|φ_{2}| + n^{2}|φ_{1}| + n|φ_{1}||φ_{2}|) time. In total, algorithm CHECK-HORN requires O(n^{4} + n^{3}|φ_{2}| + n^{2}|φ_{1}| + n|φ_{1}||φ_{2}|) time. □ Remark. Since the formulas ϕ_{1} and ϕ_{2} monotonically increase (by adding conjuncts), it is possible to use appropriate data structures which support incremental computation. This will lead to savings on the running time of the algorithm.

3.2 Model-based representation

In this section, we consider Horn theories represented by their characteristic sets. As in the case of formula representation, we find that deciding whether the difference φ_{1} \ φ_{2} of two Horn formulas is Horn is solvable in polynomial time. Let Σ_{1} and Σ_{2} be Horn theories. Let S be the set of models defined by

S = C^{∗}(Σ_{1}) ∪ {v ⋀ w | v, w ∈ C^{∗}(Σ_{1})}.  (3.11)

That is, S augments C^{∗}(Σ_{1}) by one step of the closure operator Cl_{∧}(·). We split S into S_{1} and S_{2} as follows:

\begin{matrix}S_{1} ∩ Σ_{2} = ∅ \\ S_{2} ⊆ Σ_{2}. \end{matrix}  (3.12)

It is easy to see that

S_{1} ⊆ Σ_{1} \ Σ_{2}  (3.13)
Cl_{∧}(S_{2}) ⊆ Σ_{2}.  (3.14)

We furthermore have the following lemma, where a similar result is obtained in [7].

Lemma 3.2 For a Horn theory Σ, let S = C^{∗}(Σ) ∪ {v ⋀ w | v, w ∈ C^{∗}(Σ)}, and let S_{1} and S_{2} be sets of models such that S_{1} ∪ S_{2} = S. Then

Cl_{∧}(S_{1}) ∪ Cl_{∧}(S_{2}) = Σ.  (3.15)

Proof. Since S_{1}, S_{2} ⊆ Σ and Σ is Horn, Cl_{∧}(S_{1}) ∪ Cl_{∧}(S_{2}) ⊆ Σ holds. For the converse inclusion, assume that there exists a model v ∈ Σ \ (Cl_{∧}(S_{1}) ∪ Cl_{∧}(S_{2})). Then v can be represented by v = ⋀_{w∈Q_{1}} w ∧ ⋀_{u∈Q_{2}} u for some Q_{1} ⊆ S_{1} ∩ C^{∗}(Σ) and Q_{2} ⊆ S_{2} ∩ C^{∗}(Σ). If Q_{1} = ∅ (resp., Q_{2} = ∅), then v ∈ Cl_{∧}(S_{2}) (resp., v ∈ Cl_{∧}(S_{1})) holds, which is a contradiction. Thus Q_{1}, Q_{2} ≠ ∅. For a model w ∈ Q_{1}, let Σ_{w} = {w ∧ u | u ∈ Q_{2}}. By the definition of S, Σ_{w} ⊆ S holds for all w. Assume that some w^{∗} ∈ Q_{1} satisfies Σ_{w^{∗}} ⊆ S_{1}. Then, since Q_{1}, Σ_{w^{∗}} ⊆ S_{1}, and since v can be represented by v = ⋀_{w∈Q_{1}} w ∧ ⋀_{u∈Σ_{w^{∗}}} u, we have v ∈ Cl_{∧}(S_{1}), a contradiction. Thus, for every w ∈ Q_{1}, there is a model u^{(w)} ∈ Σ_{w} such that u^{(w)} ∈ S_{2}. We can see that v = ⋀_{w∈Q_{1}} w ∧ ⋀_{u∈Q_{2}} u = ⋀_{w∈Q_{1}} u^{(w)} ∧ ⋀_{u∈Q_{2}} u holds. Since this says v ∈ Cl_{∧}(S_{2}), we again have a contradiction. □ By this lemma,

Cl_{∧}(S_{1}) ∪ Cl_{∧}(S_{2}) = Σ_{1}  (3.16)

holds for the S_{1} and S_{2} of (3.12). The next lemma leads then to a polynomial time algorithm for our problem.

Lemma 3.3 Let Σ_{1} and Σ_{2} be Horn theories, and let S_{1} be the set of models defined by (3.12). Then Cl_{∧}(S_{1}) ∩ Σ_{2} = ∅ holds if and only if Σ_{1} \ Σ_{2} is a Horn theory. Furthermore, if Σ_{1} \ Σ_{2} is a Horn theory, then Cl_{∧}(S_{1}) = Σ_{1} \ Σ_{2} (i.e., C^{∗}(S_{1}) = C^{∗}(Σ_{1} \ Σ_{2})) holds.

Proof. If Σ_{1}\Σ_{2} is Horn, then S_{1} ⊆ Σ_{1}\Σ_{2} implies Cl_{∧}(S_{1}) ⊆ Σ_{1}\Σ_{2}. Hence Cl_{∧}(S_{1})∩Σ_{2} = ∅ holds. On the other hand, if Cl_{∧}(S_{1})∩Σ_{2} = ∅, then Cl_{∧}(S_{1})∩Cl_{∧}(S_{2}) = ∅ holds, since Cl_{∧}(S_{2}) ⊆ Σ_{2}. This, combined with (3.16), implies that (Cl_{∧}(S_{1}), Cl_{∧}(S_{2})) forms a partition of Σ_{1}. Moreover, it follows from (3.14) and the assumption Cl_{∧}(S_{1}) ∩ Σ_{2} = ∅ that

Cl_{∧}(S_{1}) = Σ_{1} \ Σ_{2}  (3.17)

holds. Hence Σ_{1} \ Σ_{2} is Horn. The second part of the lemma also follows from (3.17). □

Theorem 3.4 Let Σ_{1} and Σ_{2} be Horn theories. Given C^{∗}(Σ_{1}) and C^{∗}(Σ_{2}), we can check whether Σ_{1} \ Σ_{2} is Horn in O(n|C^{∗}(Σ_{1})|^{2}|C^{∗}(Σ_{2})|) time. Furthermore, if Σ_{1} \ Σ_{2} is Horn, C^{∗}(Σ_{1} \ Σ_{2}) can be computed in O(n|C^{∗}(Σ_{1})|^{2}(|C^{∗}(Σ_{1})|^{2} + |C^{∗}(Σ_{2})|)) time.

Proof. For the first statement, by Lemma 3.3, we only check if Cl_{∧}(S_{1}) ∩ Σ_{2} = ∅, where S_{1} is given by (3.12). Let us first consider the time complexity to construct S_{1}. By the definition (3.11) of S, S can be constructed from C^{∗}(Σ_{1}) in O(n|C^{∗}(Σ_{1})|^{2}) time. For each v ∈ S, we can check if v ∈ S_{1} by checking whether

v = ⋀_{w∈C^{∗}(Σ_{2}):w≥v} w  (3.18)

holds. This can be done in O(n|C^{∗}(Σ_{2})|) time. Since |S| ≤ |C^{∗}(Σ_{1})|^{2}, therefore, S_{1} can be constructed in O(n|C^{∗}(Σ_{1})|^{2}|C^{∗}(Σ_{2})|) time. It is known [6] that the condition Cl_{∧}(Q_{1})∩Cl_{∧}(Q_{2}) = ∅ can be checked from Q_{1} and Q_{2} in O(n(|Q_{1}|+|Q_{2}|)) time. Based on this, the condition Cl_{∧}(S_{1})∩Σ_{2} (= Cl_{∧}(S_{1})∩Cl_{∧}(Σ_{2})) = ∅ can be checked from S_{1} and C^{∗}(Σ_{2}) in O(n(|S_{1}| + |C^{∗}(Σ_{2})|)) = O(n(|C^{∗}(Σ_{1})|^{2} + |C^{∗}(Σ_{2})|)) time. Therefore, in total, the algorithm requires O(n|C^{∗}(Σ_{1})|^{2}|C^{∗}(Σ_{2})|) time. For the second statement, by Lemma 3.3, C^{∗}(S_{1}) = C^{∗}(Σ_{1} \ Σ_{2}) holds. As already shown, S_{1} can be constructed in O(n|C^{∗}(Σ_{1})|^{2}|C^{∗}(Σ_{2})|) time. Furthermore, C^{∗}(S_{1}) can be computed from S_{1} in O(n|S_{1}|^{2}) = O(n|C^{∗}(Σ_{1})|^{4}) time, since |S_{1}| ≤ |Σ_{1}|^{2} holds. Thus, O(n|C^{∗}(Σ_{1})|^{2}(|C^{∗}(Σ_{1})|^{2} + |C^{∗}(Σ_{2})|)) time is required in total. □ We close this section with a remark on an important special case of Σ_{1} = {0, 1}^{n}, i.e., Σ_{1} contains all models. In [9], the class of double Horn functions has been introduced, which are those functions f such that both f and its complement \overline{f} are Horn.^{1} In this case, we obtain the following relation.

Proposition 3.5 Let Σ_{1} = {0, 1}^{n}, and let Σ_{2} be an arbitrary Horn theory. Then the difference Σ_{1} \ Σ_{2} is Horn if and only if Σ_{2} is double Horn. □

By this proposition and the results in [9], if Σ_{1} is fixed to {0, 1}^{n} (and thus it may be omitted from the input), then the problem of checking whether Σ_{1} \ Σ_{2} is Horn can be solved in linear time under formula-based representation, and, as a consequence of results in [9], in O(n^{2}|C^{∗}(Σ_{2})|) time under model-based representation.

4 Horn Cores

In this section, we investigate computing Horn cores of the difference of Horn theories. Since in general, multiple Horn cores can exist, several variants of this task are of interest. One is computing some Horn core of the difference, while the other is the enumeration of all Horn cores. A further interesting problem is whether the difference has a unique Horn core. As it is easy to see that the difference has a unique Horn core if and only if it is Horn, the algorithms from the previous section can be used to solve this problem. As previously, we first consider the problems under Horn CNFs, and then turn to model-based representation.

4.1 Formula-based representation

We first consider the problem of computing one Horn core of the difference φ_{1} \ φ_{2}, where φ_{1} and φ_{2} are Horn CNFs. The algorithm is a modification of algorithm CHECK-HORN, which checks whether the difference φ_{1} \ φ_{2} is Horn. In Step 3 of algorithm CHECK-HORN, if there is no Horn clause c in HC(v) such that c ≥ ϕ_{1} \ ϕ_{2}, we conclude that the difference is not Horn and halt. To compute a Horn core, however, we update ϕ_{1} and ϕ_{2} as ϕ_{1} := ϕ_{1} ∧ c and ϕ_{2} := ϕ_{2} ∧ x_{i}, respectively, for an appropriate c ∈ HC(v). This is because no Horn core contains the model v. Let us consider how to obtain the above appropriate c ∈ HC(v). For a formula ψ and a model w, let min_{≥w}(ψ) denote the set of minimal models u such that ψ(u) = 1 and u ≥ w. We claim that a clause c ∈ HC(v) such that c(u) = 1 for some u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}) is appropriate. The proof for this claim will be given (in different form) after presenting the algorithm and an example. For models v, u with v ≤ u, let HC(v; u) denote the set of Horn clauses c ∈ HC(v) whose positive literal x_{j} satisfies u_{j} = 1. For example, if v = (111000) and u = (111110), then HC(v; u) = \{(\overline{x}_{1} ∨\overline{x}_{2} ∨\overline{x}_{3} ∨x_{4}), (\overline{x}_{1} ∨\overline{x}_{2} ∨\overline{x}_{3} ∨x_{5})\}. To make the discussion clear and speed up the algorithm in practice, based on a model u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}), we update ϕ_{1} and ϕ_{2} respectively by

1Actually, in [9], DNF Horn functions have been considered, which are functions f = ⋁_{i} t_{i} such that each t_{i} is a Horn term, i.e., contains at most one negative literal. Clearly, the double Horn functions based on DNF and CNF representation coincide.

ϕ_{1} := ϕ_{1} ∧ ⋀_{c∈HC(v;u)} c,  (4.19)
ϕ_{2} := ϕ_{2} ∧ ⋀_{u_{j}=1∧v_{j}=0} x_{j}.  (4.20)

Thus, we have the following algorithm.

Algorithm HORN-CORE1 Input: Horn CNFs φ_{1} and φ_{2}. Output: A Horn core of φ_{1} \ φ_{2}.

Step 0. ϕ_{1} := φ_{1}; ϕ_{2} := φ_{2};

Step 1. if ϕ_{2} ≡ ⊥ then output ϕ_{1} and halt

else begin compute the least model v of ϕ_{2} if ϕ_{1}(v) = 0 then goto Step 2 else (i.e., ϕ_{1}(v) = 1) goto Step 3

end;

Step 2. if v = 1 then output ϕ_{1} and halt

else begin find a Horn clause c in HC(v) such that c ≥ ϕ_{1}; ϕ_{2} := ϕ_{2} ∧ x_{i}, where P (c) = {x_{i}}; goto Step 1

end;

Step 3. if there exists a Horn clause c in HC(v) such that c ≥ ϕ_{1} \ ϕ_{2}

then begin ϕ_{1} := ϕ_{1} ∧ c; if v = 1 then output ϕ_{1} and halt else ϕ_{2} := ϕ_{2} ∧ x_{i}, where P (c) = {x_{i}}

end

else begin find a model u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}); ϕ_{1} := ϕ_{1} ∧ ⋀_{c∈HC(v;u)} c;

ϕ_{2} := ϕ_{2} ∧ ⋀_{u_{j}=1∧v_{j}=0} x_{j}

end

goto Step 1. □

Example 4.1 Let us reconsider the Horn CNFs φ_{1} and φ_{2} in Example 3.1. In Step 3 of CHECK-HORN, ϕ_{1} \ ϕ_{2} ≤ x_{i} was found false for all i = 1, 2, …, 4. We thus choose in Step 3 of HORN-CORE1 a model u in min_{≥v}(ϕ_{1} \ ϕ_{2}). Since v = (0000), min_{≥v}(ϕ_{1} \ ϕ_{2}) is the set of the minimal models in the theory Σ represented by ϕ_{1} \ ϕ_{2} (see Example 3.1). The model u = (0001) is such a minimal model. Then, HC(v; u) = {x_{4}}, and we update

ϕ_{1} := (\overline{x}_{1} ∨ \overline{x}_{2}) ∧ (\overline{x}_{1} ∨ x_{3}) ∧ (\overline{x}_{2} ∨ x_{3}) ∧ (\overline{x}_{2} ∨ x_{4}) ∧ x_{4},
ϕ_{2} := \overline{x}_{4} ∧ (\overline{x}_{1} ∨ \overline{x}_{3}) ∧ (\overline{x}_{2} ∨ \overline{x}_{3}) ∧ x_{4}.

Returning to Step 1 of HORN-CORE1, we now find that ϕ_{2} ≡ ⊥ is true; hence, the current ϕ_{1} is output. Observe that the output of CHECK-HORN for φ_{1} and φ′_{2} in Example 3.1 is the same as the output ϕ_{1}. The formula φ_{1} \ φ_{2} and the output formula ϕ_{1} represent the theories Σ = {(0111), (1011), (1010), (0011), (0001)} and Σ′ = {(0111), (1011), (0011), (0001)}, respectively. It is easily checked that the output is indeed a Horn core of φ_{1} \ φ_{2}. □

Let ϕ_{1}^{(k)} and ϕ_{2}^{(k)} respectively denote the ϕ_{1} and ϕ_{2} in Step 1 of the k-th iteration, and let v^{(k)} denote the least model in ϕ_{2}^{(k)}. Then we claim that

v^{(k)} < v^{(k+1)}  (4.21)

holds for k = 1, 2, …, which implies that the number of iterations is at most n + 1. In the case that either Step 2 or the if-condition of Step 3 was reached during the k-th iteration, the proof is similar to (3.9). Thus, assume that the else-condition of Step 3 was reached during the k-th iteration. Let u^{(k)} ∈ min_{≥v^{(k)}}(ϕ_{1}^{(k)} \ ϕ_{2}^{(k)}) be chosen in algorithm HORN-CORE1. Then we show that

v^{(k)} < u^{(k)} < v^{(k+1)},  (4.22)

which completes the proof of (4.21). It follows from the definition of u^{(k)} that u^{(k)} ≥ v^{(k)} holds. Moreover, ϕ_{2}^{(k)}(v^{(k)}) = 1 and ϕ_{2}^{(k)}(u^{(k)}) = 0 imply u^{(k)} ≠ v^{(k)}. We thus have u^{(k)} > v^{(k)}. As for the second inequality of (4.22), since v^{(k)} is the least model in ϕ_{2}^{(k)}, and ϕ_{2}^{(k)} is updated as (4.20), w ≥ u^{(k)} holds for all models w such that ϕ_{2}^{(k+1)}(w) = 1 (In particular for w = v^{(k+1)}). Moreover, since ϕ_{2}^{(k+1)} ≤ ϕ_{2}^{(k)} and ϕ_{2}^{(k)}(u^{(k)}) = 0, ϕ_{2}^{(k+1)}(u^{(k)}) = 0 holds, which implies u^{(k)} ≠ v^{(k+1)}. Hence u^{(k)} < v^{(k+1)} holds. We next present some properties of ϕ_{1}^{(k)} without their proofs, since they can be easily found.

Lemma 4.1 Let ϕ_{1}^{(k)} and ϕ_{2}^{(k)} be defined as above. Then ϕ_{1}^{(k)} ≤ φ_{1} and ϕ_{2}^{(k)} ≤ φ_{2} hold.

Lemma 4.2 Let v^{(k)}, ϕ_{1}^{(k)} and ϕ_{2}^{(k)} be defined as above.

(i) If Step 2 was reached during the k-th iteration, then ϕ_{1}^{(k+1)}(w) = ϕ_{1}^{(k)}(w) holds for all models w.

(ii) If the if-condition of Step 3 was reached during the k-th iteration, then ϕ_{1}^{(k+1)}(w) = ϕ_{1}^{(k)}(w) holds for all models w that satisfy either w ≱ v^{(k)} or w ≥ v^{(k+1)}.

(iii) If the else-condition of Step 3 was reached during the k-th iteration, then ϕ_{1}^{(k+1)}(w) = ϕ_{1}^{(k)}(w) holds for all models w that satisfy either w ≱ v^{(k)} or w ≥ u^{(k)}, and ϕ_{1}^{(k+1)}(w) = 0 holds for all models w that satisfy v^{(k)} ≤ w < u^{(k)}, where u^{(k)} ∈ min_{≥v^{(k)}}(ϕ_{1}^{(k)} \ϕ_{2}^{(k)}) is chosen in algorithm HORN-CORE1.

By Lemma 4.2 (iii), if the else-condition of Step 3 was reached during the k-th iteration, then ϕ_{1}^{(k+1)}(u^{(k)}) = ϕ_{1}^{(k)}(u^{(k)}) holds. It follows from (4.21) and (4.22) that u^{(k)} < v^{(l)} holds for all l ≥ k + 1. Since ϕ_{1}^{(k)}(u^{(k)}) = 1, Lemma 4.2 implies that the final output in the h-th iteration, φ_{1}^{(h)}, also satisfies ϕ_{1}^{(h)}(u^{(k)}) = 1. Let us next consider a model u′ ∈ min_{≥v^{(k)}}(ϕ_{1}^{(k)} \ ϕ_{2}^{(k)}) with u′ ≠ u^{(k)}. Since u^{(k)}, u′ ≥ v^{(k)} and u′ ≱ u^{(k)}, there is an index j such that v_{j}^{(k)} = u′_{j} = 0 and u_{j}^{(k)} = 1. This means

ϕ_{1}^{(k+1)}(u′) = 0.  (4.23)

Moreover, since u^{(k)} < v^{(k+1)} (by (4.22)) and u′ ≱ u^{(k)}, we have

u′ ≱ v^{(k+1)}.  (4.24)

By (4.23) and (4.24), Lemma 4.2 implies that the output ϕ_{1}^{(h)} satisfies ϕ_{1}^{(h)}(u′) = 0 for all models u′ ∈ min_{≥v^{(k)}}(ϕ_{1}^{(k)} \ ϕ_{2}^{(k)}) with u′ ≠ u^{(k)}. Therefore, the choice of u in the else-statement of Step 3 is in fact a choice of a Horn core ψ (= ϕ_{1}^{(h)}) of φ_{1} \ φ_{2} among all possible cores by imposing ψ(u) = 1.

Theorem 4.3 Let φ_{1} and φ_{2} be Horn CNFs. Then algorithm HORN-CORE1 outputs a Horn core of φ_{1} \ φ_{2} in O(n^{4} + n^{3}|φ_{2}| + n^{2}|φ_{1}| + n|φ_{1}||φ_{2}|) time.

Proof. Let us first prove that the output Horn CNF ϕ_{1} (= ϕ_{1}^{(h)}) satisfies ϕ_{1}^{(h)} ≤ φ_{1} \ φ_{2}. To prove this, it is sufficient to show that ϕ_{1}^{(k)} \ ϕ_{2}^{(k)} ≤ φ_{1} \ φ_{2} holds for all k. By the discussion before Algorithm CHECK-HORN, if either Step 2 or the if-statement of Step 3 was reached during the k-th iteration, then ϕ_{1}^{(k+1)} \ ϕ_{2}^{(k+1)} = ϕ_{1}^{(k)} \ ϕ_{2}^{(k)} holds. On the other hand, if the else-statement of Step 3 was reached during the k-th iteration, we have ϕ_{1}^{(k+1)} \ ϕ_{2}^{(k+1)} ≤ ϕ_{1}^{(k)} \ ϕ_{2}^{(k)}. Indeed, as ϕ_{2}^{(k+1)} = ϕ_{2}^{(k)} ∧ ⋀_{u_{j}^{(k)}=1∧v_{j}^{(k)}=0} x_{j} and v^{(k)} is the least model of ϕ_{2}^{(k)}, ϕ_{2}^{(k+1)}(w) = ϕ_{2}^{(k)}(w) holds for all w that satisfy either w ≱ v^{(k)} or w ≥ u^{(k)}. This combined with Lemma 4.2(iii) implies our claim. Let us next show ϕ_{1}^{(h)} is a Horn core of φ_{1} \ φ_{2}. Assume the contrary, i.e., there is a Horn core ψ such that ψ > ϕ_{1}^{(h)}. Let w be a minimal model such that ψ(w) = 1 and ϕ_{1}^{(h)}(w) = 0. Then ϕ_{1}^{(1)}(w) = φ_{1}(w) = 1 holds. By this and Lemma 4.1, there exists a k such that ϕ_{1}^{(k)}(w) = 1 and ϕ_{1}^{(k+1)}(w) = 0 holds. Moreover, we have ϕ_{2}^{(k)}(w) = 0. This follows from φ_{2}(w) = 0 (by ψ(w) = 1) and Lemma 4.1. Thus (ϕ_{1}^{(k)} \ ϕ_{2}^{(k)})(w) = 1 holds. This implies that ϕ_{1}^{(k)} was modified in the else-statement of Step 3, in which w > v^{(k)} and w ≱ u^{(k)} hold by Lemma 4.2 (iii). These facts, together with u^{(k)} > v^{(k)}, imply

u^{(k)} > (w ∧ u^{(k)}) ≥ v^{(k)}.

Since ψ(u^{(k)}) = ψ(w) = 1, ψ(w ∧ u^{(k)}) = 1 must hold. However, ϕ_{1}^{(k)}(w ∧ u^{(k)}) = 0 holds by Lemma 4.2 (iii), and hence ϕ_{1}^{(h)}(w ∧ u^{(k)}) = 0 follows from Lemma 4.2 and (4.21). This contradicts ψ > ϕ_{1}^{(h)}. Thus, algorithm HORN-CORE1 correctly outputs a Horn core of φ_{1} \ φ_{2}. For the time complexity, we only consider how to compute a model u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}), because the rest is similar to algorithm CHECK-HORN. Note that u ∈ min_{≥v}(ϕ_{1} \ϕ_{2}) holds if and only if u ∈ min((ϕ_{1} \ ϕ_{2}) ∧ ⋀_{v_{j}=1} x_{j}). Let the CNF of ϕ_{2} be ϕ_{2} = ⋀_{j=1}^{m} c_{j}. Then, similarly to (3.1),

(ϕ_{1} \ ϕ_{2}) ∧ ⋀_{v_{j}=1} x_{j} = ⋁_{j=1}^{m}(ϕ_{1} ∧ t_{j} ∧ ⋀_{v_{j}=1} x_{j}),  (4.25)

where t_{j} is the term equivalent to \overline{c}_{j}. Note that each ϕ_{1} ∧ t_{j} ∧ ⋀_{v_{j}=1} x_{j} is a Horn CNF and (4.25) is a disjunction of m Horn CNFs. Since any Horn theory has the least model, (4.25) has at most m minimal models. Since each disjunct in (4.25) has size O(|ϕ_{1}| + n), all candidates for u (the least models in ϕ_{1} ∧ t_{j} ∧ ⋀_{v_{j}=1} x_{j}, j = 1, 2, …, m) can be computed in O(m(|ϕ_{1}| + n)) time [5]. Since finding a minimal model u among all such candidates can be done in O(nm) time (i.e., linear time) by counting zero-bits, we can compute a model u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}) in O(m(|ϕ_{1}| + n) + nm) = O(m(|ϕ_{1}| + n)) time. Similarly to algorithm CHECK-HORN, we have |ϕ_{1}| ≤ |φ_{1}| + n^{2} and m ≤ m_{2} + n, where m_{2} is the number of clauses in φ_{2}. Thus O(n^{3} + n^{2}|φ_{2}| + n|φ_{1}| + |φ_{1}||φ_{2}|) time is required in this part. Since the rest is similar to algorithm CHECK-HORN, and the number of iterations is at most n + 1, algorithm HORN-CORE1 requires O(n^{4} + n^{3}|φ_{2}| + n^{2}|φ_{1}| + n|φ_{1}||φ_{2}|) time in total. □ Let us next consider the problem of computing all Horn cores of φ_{1} \ φ_{2}. We observe that in general, an exponential number of Horn cores might exist. This is shown by the following example.

Example 4.2 Let φ_{1} = ⊤ and φ_{2} = ⋀_{i=1}^{n}[(\overline{x}_{i} ∨ y_{i}) ∧ (x_{i} ∨ \overline{y}_{i})], i.e., φ_{2} states that x_{i} is equivalent to y_{i} for all i = 1, 2, …, n. Then φ_{1} \ φ_{2} is described by the formula

⋁_{i=1}^{n}(x_{i}\overline{y}_{i} ∨ \overline{x}_{i}y_{i}),  (4.26)

which can be rewritten to the CNF

φ = ⋀_{S⊆\{1,2,...,n\}} ( ⋁_{i∈S}(x_{i} ∨ y_{i}) ∨ ⋁_{j∈\overline{S}}(\overline{x}_{j} ∨ \overline{y}_{j})),  (4.27)

where \overline{S} = \{1, 2, …, n\} \ S. Consider then the Horn CNF

ψ = (\overline{x}_{1} ∨ \overline{y}_{1} ∨ ⋯ ∨ \overline{x}_{n} ∨ \overline{y}_{n}) ∧ ⋀_{i=0}^{n−1}(\overline{x}_{1} ∨ \overline{y}_{1} ∨ ⋯ ∨ \overline{x}_{i} ∨ \overline{y}_{i} ∨ x_{i+1}),  (4.28)

where (\overline{x}_{1} ∨ \overline{y}_{1} ∨ ⋯ ∨ \overline{x}_{i} ∨ \overline{y}_{i} ∨ x_{i+1}) = x_{1} if i = 0. Observe that every clause in φ contains some clause in ψ; hence, ψ ≤ φ holds. Moreover, ψ is a Horn core of φ. Indeed, suppose some Horn ψ′ exists such that ψ < ψ′ ≤ φ. Then there exists a model v such that ψ′(v) = φ(v) = 1 but ψ(v) = 0. The latter implies that there is some i ≤ n − 1 such that v has value 1 on all components corresponding to x_{j}, y_{j} for j = 1, 2, …, i and value 0 for the component of x_{i+1}. Let w be the model which has value 1 on the components x_{j}, y_{j}, j = 1, 2, …, i and x_{i+1}, and has value 0 on all other components. Then, we have ψ(w) = ψ′(w) = 1, and since ψ′ is Horn, ψ′(v ∧ w) = 1 follows. However, φ(v ∧ w) = 0 holds, since x_{j} and y_{j} of v ∧ w are 1 for j = 1, 2, …, i, and 0 for j = i + 1, i + 2, …, n. This contradicts ψ′ ≤ φ. Hence, the ψ′ as hypothesized does not exist, which means that ψ is a Horn core of φ. Since x_{i+1} and y_{i+1} are symmetric in φ, it follows that we may replace in ψ arbitrarily the (unique) positive occurrence of x_{i} by y_{i}, and we obtain another Horn core of φ. Consequently φ has at least 2^{n} Horn cores. □

The previous example shows that computing all Horn cores is not always possible in polynomial time. However, this still leaves hope for a polynomial total time algorithm (called output-polynomial in [12]), i.e., which runs in polynomial time in the combined size of the input and the output. We will now show that such an algorithm does exist, and that even the enumeration of all Horn cores with polynomial delay [12] is possible. Recall that in HORN-CORE1, the choice of u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}) in the else-statement of Step 3 results in a Horn core ψ of φ_{1} \ φ_{2} such that ψ(u) = 1 and ψ(u′) = 0 for all other models u′ ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}) (see the discussion below Lemma 4.2). We show below that every Horn core ψ satisfies ψ(u) = 1 for some u. This means that every Horn core can be constructed by algorithm HORN-CORE1, if it properly chooses a model u in the else-statement of Step 3. Let ψ be a Horn core of φ_{1} \ φ_{2}. We execute algorithm HORN-CORE1 according to this ψ. That is, if the else-condition of Step 3 holds in some iteration, we find some u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}) such that ψ(u) = 1, and then update ϕ_{1} and ϕ_{2} according to such a u. We now show that such a u can always be found. Assume that such a u cannot be found in some iteration k; in what follows, we suppress superscripts ^{(k)} for convenience. Then ϕ_{2} ≤ φ_{2} holds by Lemma 4.1, and ϕ_{1}(w) = φ_{1}(w) holds for all w ≥ v by Lemma 4.2 and (4.21). These facts imply that

(φ_{1} \ φ_{2})(w) ≤ (ϕ_{1} \ ϕ_{2})(w)  (4.29)

holds for all w ≥ v^{(k)}. Since ψ is Horn, all models w such that ψ(w) = 1 and w ≥ v must satisfy w ≥ u for some u ∈ min_{≥v}(φ_{1} \ φ_{2}), and hence (4.29) implies

w ≥ u  (4.30)

for some u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}). For such a u, we have ψ ≤ ⋀_{c∈HC(v;u)} c, because any model w with v ≤ w < u satisfies (φ_{1} \ φ_{2})(w) ≤ (ϕ_{1} \ ϕ_{2})(w) = 0, and hence ψ(w) = 0. Based on this u, we can update ϕ_{1} and ϕ_{2}. Then continuing HORN-CORE1, we obtain a Horn core ψ′ such that ψ′ ≥ ψ. Since ψ was a Horn core, this implies that ψ′ = ψ and hence ψ(u) = 1. It follows that a u as hypothesized can be found. Thus, all Horn cores can be generated as follows.

Algorithm ALL-HORN-CORES(φ_{1}, φ_{2}) Input: Horn CNFs φ_{1} and φ_{2}. Output: All Horn cores of φ_{1} \ φ_{2}.

Step 0. ϕ_{1} := φ_{1}; ϕ_{2} := φ_{2}; Step 1. if ϕ_{2} ≡ ⊥ then output ϕ_{1} and halt

else begin compute the least model v of ϕ_{2} if ϕ_{1}(v) = 0 then goto Step 2 else (i.e., ϕ_{1}(v) = 1) goto Step 3

end;

Step 2. if v = 1 then output ϕ_{1} and halt

else begin find a Horn clause c in HC(v) such that c ≥ ϕ_{1}; ϕ_{2} := ϕ_{2} ∧ x_{i}, where P (c) = {x_{i}}; goto Step 1

end;

Step 3. if there exists a Horn clause c in HC(v) such that c ≥ ϕ_{1} \ ϕ_{2}

then begin ϕ_{1} := ϕ_{1} ∧ c; if v = 1 then output ϕ_{1} and exit; else begin ϕ_{2} := ϕ_{2} ∧ x_{i}, where P (c) = {x_{i}}; goto Step 1 end

end

else for each a model u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}) do begin ϕ_{1} := ϕ_{1} ∧ ⋀_{c∈HC(v;u)} c;

ϕ_{2} := ϕ_{2} ∧ ⋀_{u_{j}=1∧v_{j}=0} x_{j};

call ALL-HORN-CORES(ϕ_{1},ϕ_{2}) end{for}. □

Example 4.3 Consider again the Horn CNFs φ_{1} and φ_{2} from Examples 3.1 and 4.1. In Example 4.1, HORN-CORE1 found one Horn core ψ_{1} = (\overline{x}_{1} ∨ \overline{x}_{2}) ∧ (\overline{x}_{1} ∨ x_{3}) ∧ (\overline{x}_{2} ∨ x_{3}) ∧ (\overline{x}_{2} ∨ x_{4}) ∧ x_{4} of φ_{1} \ φ_{2}, based on the choice of u = (0001) from min_{≥v}(ϕ_{1} \ ϕ_{2}). This ψ_{1} is output by ALL-HORN-CORES. However, in Step 3, there is another model u = (1010) in min_{≥v}(ϕ_{1} \ ϕ_{2}). Then, based on this v = (0000), we have H(v; u) = {x_{1}, x_{3}}, and ϕ_{1} and ϕ_{2} are updated to

ϕ_{1} = (\overline{x}_{1} ∨ \overline{x}_{2}) ∧ (\overline{x}_{1} ∨ x_{3}) ∧ (\overline{x}_{2} ∨ x_{3}) ∧ (\overline{x}_{2} ∨ x_{4}) ∧ x_{1} ∧ x_{3} = x_{1} ∧ \overline{x}_{2} ∧ x_{3},
ϕ_{2} = \overline{x}_{4} ∧ (\overline{x}_{1} ∨ \overline{x}_{3}) ∧ (\overline{x}_{2} ∨ \overline{x}_{3}) ∧ x_{1} ∧ x_{3} = ⊥,

respectively. Thus, in the recursive call of ALL-HORN-CORES, ψ_{2} = x_{1} ∧ \overline{x}_{2} ∧ x_{3} is also output before exist from the entire procedure. Observe that ψ_{2} represents the theory Π_{2} = {(1010), (1011)}, which is indeed a Horn core of Σ = {(0111), (1011), (1010), (0011), (0001)}. □

Theorem 4.4 Algorithm ALL-HORN-CORES correctly generates all Horn cores of φ_{1} \φ_{2} with polynomial delay, where the delay is bounded by the time of computing one Horn core, i.e., O(n^{4} + n^{3}|φ_{2}| + n^{2}|φ_{1}| + n|φ_{1}||φ_{2}|).

Proof. The correctness of algorithm ALL-HORN-CORES follows from the discussion before the algorithm, and its time complexity can be analyzed similarly to the proof of Theorem 4.3. □

4.2 Model-based representation

In Subsection 3.2, we have seen that S_{1} of (3.12) characterizes the difference Σ_{1} \ Σ_{2} of two Horn theories Σ_{1} and Σ_{2}. In this subsection, we show that any maximal set Q ⊆ S_{1} such that Cl_{∧}(Q) ∩ Σ_{2} = ∅ gives a Horn core of Σ_{1} \ Σ_{2}, and conversely any Horn core of Σ_{1} \ Σ_{2} can be generated from such a maximal set Q ⊆ S_{1}. Note that, by the definition of S_{1}, any maximal set Q ⊆ S with Cl_{∧}(Q) ∩ Σ_{2} = ∅ is contained in S_{1}. Thus we prove the above statements by using a set S instead of S_{1}.

Lemma 4.5 Let Σ_{1} and Σ_{2} be Horn theories, and let Q be a maximal set Q ⊆ S such that Cl_{∧}(Q) ∩ Σ_{2} = ∅, where S is given by (3.11). Then Cl_{∧}(Q) is a Horn core of Σ_{1} \ Σ_{2}.

Proof. Since Cl_{∧}(Q) ∩ Σ_{2} = ∅, there exist a Horn core Π of Σ_{1} \ Σ_{2} such that Π ⊇ Cl_{∧}(Q). Assume that there exists a model v ∈ Π \ Cl_{∧}(Q). Since v ∈ Σ_{1}, v can be represented by

v = ⋀_{u∈Q_{1}} u ∧ ⋀_{w∈Q_{2}} w  (4.31)

for some Q_{1} ⊆ Q ∩ C^{∗}(Σ_{1}) and Q_{2} ⊆ (S \ Q) ∩ C^{∗}(Σ_{1}). If Q_{2} = ∅, then v ∈ Cl_{∧}(Q), which is a contradiction. If Q_{1} = ∅, then the maximality of Q implies that, for each w ∈ Q_{2}, there exists Q_{w} ⊆ Q such that

⋀_{u∈Q_{w}} u ∧ w ∈ Σ_{2}.

Let y^{(w)} = ⋀_{u∈Q_{w}} u and z^{(w)} = ⋀_{u∈Q_{w}} u ∧ w. Then, since Σ_{2} is Horn and Q_{1} = ∅, we have

⋀_{w∈Q_{2}} z^{(w)} = ⋀_{w∈Q_{2}} y^{(w)} ∧ ⋀_{w∈Q_{2}} w = ⋀_{w∈Q_{2}} y^{(w)} ∧ v ∈ Σ_{2}.  (4.32)

Note that y^{(w)} ∈ Cl_{∧}(Q) holds for all w ∈ Q_{2}. Thus ⋀_{w∈Q_{2}} y^{(w)} is also contained in Cl_{∧}(Q) ⊆ Π, and since Π is Horn and v = ⋀_{w∈Q_{2}} w ∈ Π, it follows ⋀_{w∈Q_{2}} z^{(w)} ∈ Π. But then Π ⊆ Σ_{1} \ Σ_{2} contradicts (4.32), showing that Q_{1} = ∅ is impossible.

Finally, let us consider the remaining case (i.e., Q_{1}, Q_{2} ≠ ∅). For a model w ∈ Q_{2}, let Σ_{w} = {w ∧ u | u ∈ Q_{1}}. Since Q_{1}, Q_{2} ⊆ C^{∗}(Σ_{1}), Σ_{w} ⊆ S holds for all w. Assume that, for each w ∈ Q_{2}, there is a model u^{(w)} ∈ Σ_{w} such that u^{(w)} ∈ Q. Then v = ⋀_{w∈Q_{2}} u^{(w)} ∧ ⋀_{w∈Q_{1}} w holds. Since u^{(w)} ∈ Q and Q_{1} ⊆ Q, we have v ∈ Cl_{∧}(Q), a contradiction. Thus, there is a model w^{∗} ∈ Q_{2} such that Σ_{w^{∗}} ⊆ S \ Q. The maximality of Q implies that, for each w ∈ Q_{2} ∪ Σ_{w^{∗}}, there exists Q_{w} ⊆ Q such that

⋀_{u∈Q_{w}} u ∧ w ∈ Σ_{2}.

Let y^{(w)} = ⋀_{u∈Q_{w}} u and z^{(w)} = ⋀_{u∈Q_{w}} u ∧ w. Then similarly to the above case of Q_{1} = ∅, we can derive a contradiction. □ Let us next show the converse direction.

Lemma 4.6 Let Σ_{1} and Σ_{2} be Horn theories, and let Π be a Horn core of Σ_{1} \ Σ_{2}. Then Π = Cl_{∧}(Q) holds for some maximal set Q ⊆ S such that Cl_{∧}(Q) ∩ Σ_{2} = ∅, where S is given by (3.11).

Proof. Assume that Π is a Horn core of Σ_{1} \ Σ_{2} which cannot be represented by any maximal set Q ⊆ S such that Cl_{∧}(Q) ∩ Σ_{2} = ∅. Then there is a model v ∈ C^{∗}(Π) \ S. Since v ∈ Σ_{1}, v can be represented by v = ⋀_{w∈Q_{1}} w ∧ ⋀_{w∈Q_{2}} w for some Q_{1} ⊆ Π ∩ C^{∗}(Σ_{1}) and Q_{2} ⊆ C^{∗}(Σ_{1}) \ Π. Since v ∈ C^{∗}(Π) \ S, Q_{2} ≠ ∅ holds. Then by an argument similar to the case of Q_{2} ≠ ∅ in the proof of Lemma 4.5, we can derive a contradiction by showing v ∈ Σ_{2}.

□

From Lemmas 4.5 and 4.6, we have the next characterization.

Theorem 4.7 Let Σ_{1} and Σ_{2} be Horn theories, and let S be given by (3.11). Then Π is a Horn core of Σ_{1} \ Σ_{2} if and only if Π = Cl_{∧}(Q) holds for some maximal set Q ⊆ S such that Cl_{∧}(Q) ∩ Σ_{2} = ∅. □

Based on Theorem 4.7, we obtain the following polynomial time algorithm for computing a Horn core of Σ_{1} \ Σ_{2}.

Algorithm HORN-CORE2 Input: Characteristic sets C^{∗}(Σ_{1}) and C^{∗}(Σ_{2}) of Horn theories Σ_{1} and Σ_{2}. Output: The characteristic set C^{∗}(Π) of a Horn core Π of Σ_{1} \ Σ_{2}.

Step 0. Q := ∅; compute the set of models S given by (3.11); Step 1. for each w ∈ S do begin

if Cl_{∧}(Q ∪ {w}) ∩ Σ_{2} = ∅ then Q := Q ∪ {w}

end{for};

Step 2. output C^{∗}(Q) and halt. □

Example 4.4 Let us apply HORN-CORE2 to the Horn CNFs φ_{1} and φ_{2} from Example 3.1. They represent the theories Σ_{1} = {(0111), (1011), (1010), (0011), (0001), (0010), (0000)} and Σ_{2} = {(1100), (0010), (0100), (1000), (0000)}, respectively. Hence,

C^{∗}(Σ_{1}) = {(0111), (1011), (1010), (0001)},
C^{∗}(Σ_{2}) = {(1100), (0010), (0100), (1000)}.

Then, in Step 0, we compute

S = C^{∗}(Σ_{1}) ∪ {(0000), (0011), (0010)}
= {(0111), (1011), (1010), (0001), (0000), (0011), (0010)}.

By considering the models w ∈ S in the above order, we obtain in Step 1

Q = {(0111), (1011), (0001), (0011)}.

Thus, C^{∗}(Q) = {(0111), (1011), (0001)} is output in Step 2. Observe that C^{∗}(Q) is the characteristic set of the Horn core Π_{1} = {(0111), (1011), (0011), (0001)} of φ_{1} \ φ_{2}, which was already obtained in Example 4.1. □

Theorem 4.8 Let Σ_{1} and Σ_{2} be Horn theories. Then, algorithm HORN-CORE2 outputs the characteristic set of a Horn core of Σ_{1} \ Σ_{2} in O(n|C^{∗}(Σ_{1})|^{2}(|C^{∗}(Σ_{1})|^{2} + |Σ_{2}|)) time.

Proof. The correctness of algorithm HORN-CORE2 follows from Theorem 4.7. For its time complexity, Step 0 clearly can be done in O(n|C^{∗}(Σ_{1})|^{2}) time. In Step 1, we can check if Cl_{∧}(Q ∪ {w}) ∩ Σ_{2} = ∅ for each w in O(n(|Q| + |C^{∗}(Σ_{2}|)) = O(n(|C^{∗}(Σ_{1})|^{2} + |C^{∗}(Σ_{2}|)) time [6]. By |S| ≤ |C^{∗}(Σ_{1})|^{2}, Step 1 requires O(n|C^{∗}(Σ_{1})|^{2}(|C^{∗}(Σ_{1})|^{2} + |C^{∗}(Σ_{2}|)) time. Step 2 is executable in O(n|Q|^{2}) = O(n|C^{∗}(Σ_{1})|^{4}) time. Therefore, algorithm HORN-CORE2 requires O(n|C^{∗}(Σ_{1})|^{2}(|C^{∗}(Σ_{1})|^{2} + |C^{∗}(Σ_{2}|)) time.

□

Also deciding whether a given theory Π is a Horn core of the difference Σ_{1} \ Σ_{2} is possible in polynomial time. For that, modify the algorithm HORN-CORE2 as follows. In Step 0, set Q to Π ∩ (S \ Σ_{2}). In Step 1, check whether Π = Cl_{∧}(Q) holds and no w ∈ S \ Q exists such that Cl_{∧}(Q ∪ {w}) ∩ Σ_{2} = ∅. If these are true, then output “yes” in Step 2, else output “no”. The correctness of this procedure, which runs obviously in polynomial time, follows from Theorem 4.7. By Theorem 4.7, we have a good characterization of a Horn core of the difference. Theorem 4.8 says that this characterization leads to a polynomial time algorithm for computing some arbitrary Horn core. However, as we will show next, However, there is no polynomial total time algorithm for generating all Horn cores, unless P = NP. For a (not necessarily Horn) theory Σ, let HC(Σ) denote the set of all Horn cores of Σ. In order to show the intractability of computing HC(Σ_{1} \ Σ_{2}) from C^{∗}(Σ_{1}) and C^{∗}(Σ_{2}), let us consider the following problem.

Problem ADDITIONAL-HCORE
Input: Characteristic sets C^{∗}(Σ_{1}) and C^{∗}(Σ_{2}) of Horn theories Σ_{1} and Σ_{2}, and

a family of the characteristic sets C^{∗}(Π) of Horn theories Π from a subset S ⊆ HC(Σ_{1} \ Σ_{2}).

Question: Does there exist some Π ∈ HC(Σ_{1} \ Σ_{2}) \ S?

Let V = {1, 2, …, n}, and let Φ = ⋀_{c∈C} c be a CNF on x_{1}, …, x_{n}. It is well-known [20] that the satisfiability problem (SAT) (i.e., deciding whether Φ(v) = 1 for some v ∈ {0, 1}^{n}) is NP-complete. Without loss of NP-hardness, we may assume that no literal appears in all c ∈ C. Let V′ = {1′, 2′, …, n′}, and define

Φ_{1} = ⋁_{j∈V} x_{j}x_{j′}.  (4.33)

Furthermore, let Φ_{2} be the positive CNF obtained from Φ by replacing every negative literal \overline{x}_{j} by x_{j′}, i.e.,

Φ_{2} = ⋀_{c∈C}( ⋁_{x_{j}∈P (c)} x_{j} ∨ ⋁_{\overline{x}_{j}∈N(C)} x_{j′}),  (4.34)

where P (c) and N(c) are the sets of positive and negative literals in c, respectively. Define

Φ′ = Φ_{1} ∨ Φ_{2}.  (4.35)

It is easy to see that Φ′ represents a positive theory. By the assumption that no literal appears in all c ∈ C, all terms x_{j}x_{j′} in Φ_{1} are prime implicants of Φ′. We then claim the following lemma.

Lemma 4.9 Let Φ and Φ′ be defined as above. Then Φ is satisfiable if and only if Φ′ has a prime implicant t which does not appear in Φ_{1}, and Φ is not satisfiable if and only if Φ′ ≡ Φ_{1}.

Proof. Let us prove the first half. Let v be a model such that Φ(v) = 1. Then construct a term t_{v} by

t_{v} = ⋀_{v_{j}=1} x_{j} ∧ ⋀_{v_{j}=0} x_{j′}.

Clearly, this t_{v} is positive, and t_{v} ≤ Φ_{2} holds. Since t_{v} contains exactly one of x_{j} and x_{j′} for every j, we have t_{v} ≰ Φ_{1}, which implies the only-if part. On the other hand, suppose that Φ′ has a prime implicant t which does not appear in Φ_{1}. Since t does not contain both x_{j} and x_{j′} for any j, we can define a model v ∈ {0, 1}^{V} by

v_{j} = \{ \begin{matrix}1, & if x_{j} ∈ P (t); \\ 0, & otherwise. \end{matrix}

Since Φ_{1}, Φ_{2} and t represent positive theories, t ≰ Φ_{1} implies t ≤ Φ_{2}. Hence we have Φ(v) = 1. This proves the if-part. The second half of the lemma is a restatement of the first half. □ Let W_{1} = V ∪ V′, W_{2} = {n + 1, n + 2, …, 2n + 1}, and W = W_{1} ∪ W_{2}. Let x^{U} denote the model with x_{j}^{U} = 1 if j ∈ U and 0 otherwise. Define sets of models M_{1}, M_{2} ⊆ {0, 1}^{W} by

M_{1} = {x^{U} | U ⊆ W_{1}, |U ∩ W_{1}| ≥ 2n − 1}  (4.36)
M_{2} = M_{2,1} ∪ M_{2,2},  (4.37)

where

M_{2,1} = {x^{U} | W \ U = {n + j, j} or {n + j, j′}, j ∈ V },
M_{2,2} = {x^{U} | W \ U = {2n + 1} ∪ c, c ∈ C_{2}},

and C_{2} corresponds to the set of clauses in Φ_{2} of (4.34). (Since c ∈ C_{2} is positive, we regard a clause c ∈ C_{2} as the corresponding index set; e.g., we write c = {1, 2′, 4} instead of c = (x_{1} ∨ x_{2′} ∨ x_{4}).) Let

Σ_{1} = Cl_{∧}(M_{1}) and Σ_{2} = Cl_{∧}(M_{2}).

As we will see in Lemma 4.12, these Σ_{1} and Σ_{2}, together with a suitable S, give rise to a desired instance of problem ADDITIONAL-HCORE. Then, since

Σ_{1} = {x^{U} | U ∩ W_{2} = ∅},  (4.38)

Σ_{1} \ Σ_{2} = Σ_{1} \ Σ′_{2} holds, where

Σ′_{2} = {x^{U} ∈ Σ_{2} | U ∩ W_{2} = ∅}.  (4.39)

This allows us to restrict our attention to W_{1}. That is, we will consider Σ_{1}[W_{1}] \ Σ′_{2}[W_{1}] ⊆ {0, 1}^{W_{1}} in place of Σ_{1} \ Σ_{2} ⊆ {0, 1}^{W}, where Σ[U] denotes the projection of Σ on U for a theory Σ and an index set U. The following lemma shows that Σ_{1}[W_{1}] \ Σ′_{2}[W_{1}] can be represented by the formula Φ′.

Lemma 4.10 Let Σ′_{2} and Φ′ be defined by (4.39) and (4.35), respectively. Then the theory Σ′_{2}[W_{1}] can be represented by ¬Φ′.

Proof. Note that

¬Φ′ = ⋀_{j∈V} (\overline{x}_{j} ∨ \overline{x}_{j′}) ∧ ⋁_{c∈C_{2}}( ⋀_{l∈c} \overline{x}_{l}).  (4.40)

Let v ∈ Σ′_{2}. Then v_{j} = 0 for all j ∈ W_{2} = {n + 1, n + 2, …, 2n + 1}. In order to have v_{n+k} = 0 for k = 1, 2, …, n, either v_{k} = 0 or v_{k′} = 0 (or both) must hold by the definition of Σ_{2}. This means that v satisfies the CNF

¬Φ_{1} = ⋀_{j∈V} (\overline{x}_{j} ∨ \overline{x}_{j′}).  (4.41)

Moreover, in order to make v_{2n+1} = 0, v must be generated by referring to some model in M_{2,2}. Hence, it follows that v also satisfies the next CNF,

¬Φ_{2} = ⋁_{c∈C_{2}}( ⋀_{l∈c} \overline{x}_{l}).  (4.42)

Thus (4.41) and (4.42) imply that all models v in Σ′_{2} satisfy ¬Φ′. Since ¬Φ′ depends only on W_{1}, all models u in Σ′_{2}[W_{1}] satisfies ¬Φ′. Conversely, we can easily see that all models u ∈ {0, 1}^{W_{1}} such that ¬Φ′(u) = 1 are contained in Σ′_{2}[W_{1}]. (Note that Σ′_{2} is a negative theory, and hence Σ′_{2}[W_{1}] is also a negative theory). □ It follows from Lemma 4.10 and Equation (4.38) that Σ_{1}[W_{1}] \ Σ′_{2}[W_{1}] can be represented by Φ′. Recall that Φ′ represents a positive theory. The Horn cores of a positive theory can be characterized as follows.

Lemma 4.11 Let Σ be a positive theory. Then Π is a Horn core of Σ if and only if Π = {w | w ≥ v} holds for some minimal model v of Σ.

Proof. For a minimal model v in Σ, consider a theory Π = {w | w ≥ v}. Clearly, Π is Horn. Since Σ is positive, Π ⊆ Σ holds. If Π is not Horn core of Σ, then there is a model u ∈ Σ \ Π such that Cl_{∧}(Π ∪ {u}) ⊆ Σ. Since u ∉ Π, v ⋀ u < v holds. Therefore, v ⋀ u ∈ Cl_{∧}(Π ∪ {u}) ⊆ Σ holds, a contradiction to the minimality of v. Thus Π is a Horn core of Σ. Conversely, assuming that Π is a Horn core of Σ, we consider the least model u of Π. Let v be a minimal model in Σ such that v ≤ u. Then it is easy to see that Π ⊆ {w | w ≥ v} ⊆ Σ. By the maximality of Π, we have Π = {w | w ≥ v}. □ Now we obtain the next lemma.

Lemma 4.12 Problem ADDITIONAL-HCORE is NP-complete.

Proof. We first show the membership in NP. Let Π ∈ HC(Σ_{1} \ Σ_{2}) \ S. Then Π \ Π_{i} ≠ ∅ holds for all Π_{i} ∈ S. Choose an arbitrary model v^{(i)} ∈ Π \ Π_{i} for each Π_{i} ∈ S, and let Q be the set of all the chosen v^{(i)}. Then (1) |Q| ≤ |S|, and (2) Cl_{∧}(Q) \ Π_{i} ≠ ∅ holds for all Π_{i} ∈ S. Moreover, since Q ⊆ Π, Q satisfies (3) Cl_{∧}(Q) ⊆ Σ_{1} and (4) Cl_{∧}(Q) ∩ Σ_{2} = ∅ (i.e., Cl_{∧}(Q) ⊆ Σ_{1} \ Σ_{2}). Conversely, if we have a set Q ⊆ Σ_{1} satisfying (1)–(4), we can conclude that HC(Σ_{1} \ Σ_{2}) \ S ≠ ∅. Now (1) can be trivially checked, (2)–(3) can be checked in polynomial time by applying a technique similar to (3.18), and polynomiality of the check (4) follows from the result in [6] that, given theories Σ and Σ′, deciding whether Cl_{∧}(Σ) ∩ Cl_{∧}(Σ′) = ∅ is possible in polynomial time. Thus any Q satisfying (1)–(4) is a polynomial certificate of the problem, i.e., a polynomial size proof for a Yes-instance which can be checked in polynomial time. Consequently, ADDITIONAL-HCORE is in NP. We next show the NP-hardness. Let Σ_{1} and Σ_{2} be constructed as above from an arbitrary CNF Φ. Lemmas 4.10 and 4.11 imply that Σ_{1}[W_{1}] \ Σ′_{2}[W_{1}] has a Horn core represented by x_{j}x_{j′}, for each j ∈ V. From (4.38), it thus follows that Σ_{1} \ Σ_{2} has a Horn core Π_{j} represented by

t_{j} = ( ⋀_{n+k∈W_{2}} \overline{x}_{k}) ∧ x_{j} ∧ x_{j′},

for every j ∈ V. Let S = {Π_{j} | j ∈ V } be the collection of all these Horn cores. Consider now the instance C^{∗}(Σ_{1}), C^{∗}(Σ_{2}), {C^{∗}(Π_{j}) | Π_{j} ∈ S} of ADDITIONAL-HCORE. It follows from Lemmas 4.9, 4.10, and 4.11 that HC(Σ_{1} \ Σ_{2}) \ S ≠ ∅ if and only if Φ is satisfiable. To complete the proof of NP-hardness, it remains to show that C^{∗}(Σ_{1}), C^{∗}(Σ_{2}) and {C^{∗}(Π_{j}) | Π_{j} ∈ S} are computable in polynomial time from the formula Φ. Clearly, C^{∗}(Σ_{1}) = M_{1} and C^{∗}(Σ_{2}) = C^{∗}(M_{2}) hold, where M_{1} and M_{2} are defined in (4.36) and (4.37); hence, both C^{∗}(Σ_{1}) and C^{∗}(Σ_{2}) are constructible in polynomial time from Φ. As easily seen, the characteristic set of Π_{j} ∈ S takes the form of

C^{∗}(Π_{j}) = {x^{U} | U ⊆ W_{1}, U ⊇ {j, j′}, |U| ≥ |W_{1}| − 1},

and hence, |C^{∗}(Π_{j})| = 2n − 2 + 1 = 2n − 1. Thus C^{∗}(Π_{j}) is constructible in polynomial time. Consequently, it follows that SAT is reducible to ADDITIONAL-HCORE in polynomial time, completing the proof. □ Based on this result, we can show in the next theorem that the enumeration of all Horn cores of a difference Σ_{1} \ Σ_{2} is a hard problem under model-based representation.

Theorem 4.13 There is no algorithm which, given the characteristic sets C^{∗}(Σ_{1}) and C^{∗}(Σ_{2}) of Horn theories Σ_{1} and Σ_{2}, computes the characteristic sets C^{∗}(Π) of all Horn cores Π ∈ HC(Σ_{1} \ Σ_{2}) in polynomial total time (i.e., polynomial in the combined size of the input and the output), unless P = NP.

Proof. Suppose such an algorithm A exists. We construct an algorithm B from it, which solves problem ADDITIONAL-HCORE in polynomial time. By Lemma 4.12, this implies P = NP. The algorithm B simulates algorithm A for at most p(n|C^{∗}(Σ_{1})| + n|C^{∗}(Σ_{2})|, n|S|) many steps, where p(I, O) is a polynomial bound on the runtime of A and I (resp., O) is the size of the input (resp., output). (As usual, any set S of n-ary vectors occupies n|S| bits.) Without loss of generality, suppose that p is a monotone function. If A stops within that time, B checks whether the computed output is identical to S; if yes, then it outputs “no”; otherwise, it outputs “yes”. It is not hard to see that B indeed correctly solves problem ADDITIONAL-HCORE; observe that if A does not halt within p(n|C^{∗}(Σ_{1})| + n|C^{∗}(Σ_{2})|, n|S|) many steps and S coincides with the set of computed Horn cores so far, then some additional Horn core exists. By the hypothesis, B runs in polynomial time in the size of C^{∗}(Σ_{1}), C^{∗}(Σ_{2}) and S. The result follows. □

5 Horn Envelope

In this section, we investigate the Horn envelope of the difference of two Horn theories. Recall that in contrast to Horn cores, the Horn envelope of a theory is always unique. We again start with Horn theories represented by Horn CNFs, and then consider the model-based case.

5.1 Formula-based representation

Prior to resolving the complexity of computing the Horn envelope, we consider the associated problem of its recognition. Intuitively, if it is difficult to recognize the Horn envelope, then so is computing it. As we will see, this is the case for the difference of Horn theories.

We now show that recognizing the Horn envelope of φ_{1} \ φ_{2} is co-NP-complete. To this end, we provide a reduction from the complement of SAT to this problem. Let V = {1, 2, …, n}, and let Φ = ⋀_{c∈C} c be a CNF on x_{1}, …, x_{n}. Furthermore, let V′ = {1′, 2′, …, n′} and define

φ_{1} = ⋀_{j∈V} ( \overline{x}_{j} ∨ \overline{x}_{j′} )  (5.43)
φ_{2} = ⋀_{c∈C}( ⋁_{x_{j}∈P (c)} \overline{x}_{j′} ∨ ⋁_{\overline{x}_{j}∈N(C)} \overline{x}_{j}).  (5.44)

Note that φ_{1} and φ_{2} represent negative (and hence Horn) theories.

Lemma 5.1 Let Φ, φ_{1} and φ_{2} be defined as above. Then Φ is not satisfiable if and only if φ_{1} is the Horn envelope of φ_{1} \ φ_{2}.

Proof. Let u be a model in {0, 1}^{V} such that Φ(u) = 1. Then we construct the model v ∈ {0, 1}^{V ∪V′} by v_{j} = u_{j} for j ∈ V and v_{j′} = 1 − u_{j} for j′ ∈ V′. Since either v_{j} = 0 or v_{j′} = 0 holds for every j ∈ V, φ_{1}(v) = 1 holds. Moreover, by the definition of φ_{2}, φ_{2}(v) = 1 holds. Thus (φ_{1} \ φ_{2})(v) = 0. Let c_{v} = ⋁_{l∈V ∪V′:v_{l}=1} \overline{x}_{l}. We claim that

φ_{1} > φ_{1} ∧ c_{v} ≥ φ_{1} \ φ_{2},

which completes the if-part, since φ_{1} ∧ c_{v} is Horn. The first inequality follows from φ_{1} ≥ φ_{1} ∧ c_{v}, φ_{1}(v) = 1 and (φ_{1} ∧ c_{v})(v) = 0. For the second inequality, it suffices to show that any model w ≠ v such that c_{v}(w) = 0 satisfies (φ_{1} \ φ_{2})(w) = 0. Clearly, w_{l} = 1 holds for every l ∈ V ∪ V′ such that v_{l} = 1. Since exactly one of v_{j} and v_{j′} has the value 1 for each j ∈ V, w ≠ v implies that there exists an index h ∈ V such that w_{h} = w_{h′} = 1. This means φ_{1}(w) = 0, and hence (φ_{1} \ φ_{2})(w) = 0. Consequently, the second inequality holds. To prove the only-if part, assume that Φ is not satisfiable. Then take a model v ∈ {0, 1}^{V ∪V′} with φ_{1}(v) = φ_{2}(v) = 1 (and hence (φ_{1} \ φ_{2})(v) = 0). Such a v has an index h ∈ V such that v_{h} = v_{h′} = 0. Let us consider the models w ≥ v such that exactly one of w_{j} or w_{j′} has the value 0 for every j ∈ V. Clearly, φ_{1}(w) = 1, and moreover it follows from the above discussion that (φ_{1} \ φ_{2})(w) = 1 holds. Since the model v is obtained by taking the intersection of all such w, this means that v is in the Horn envelope of φ_{1} \ φ_{2}. Thus the Horn envelope of φ_{1} \ φ_{2} contains all models v with φ_{1}(v) = φ_{2}(v) = 1, and hence φ_{1} is the Horn envelope. □

Theorem 5.2 Given Horn CNFs φ_{1}, φ_{2}, and φ, deciding whether φ represents the Horn envelope of φ_{1} \ φ_{2} is co-NP-complete. This is true even if φ = φ_{1}. □

Proof. We first show the membership in co-NP. The CNF φ does not represent the Horn envelope of φ_{1} \ φ_{2}, if either (i) φ_{1} \ φ_{2} ≰ φ holds or (ii) there exists a Horn clause c such that φ ≰ c and φ_{1} \ φ_{2} ≤ φ ∧ c. It is easily seen that φ_{1} \ φ_{2} ≰ φ holds if and only if φ_{1} ∧ ¬c ≰ φ_{2} holds for all clauses c in φ. The latter condition amounts to testing the implication of Horn formulas, which is well-known to be polynomial. Thus, the condition in (i) can be checked in polynomial time. For (ii), a suitable clause c can be guessed and then verified in polynomial time, similarly as in (i). (Observe that (ii) need only be checked if (i) fails.) It follows that deciding whether φ represents the Horn envelope of φ_{1} \ φ_{2} is in co-NP. The hardness part follows from Lemma 5.1. □ As an immediate consequence, we obtain the following result.

Corollary 5.3 Let φ_{1} and φ_{2} be Horn CNFs. Then computing the Horn envelope is co-NP-hard. □

By this result, an algorithm for computing the Horn envelope in polynomial time is unlikely to exist. Such an algorithm is in fact impossible, since the problem requires provably exponential time. This follows from the fact that the size of the Horn envelope of φ_{1} \ φ_{2} can be exponential in the sizes of φ_{1} and φ_{2}. This is shown by the following example.

Example 5.1 Let Horn CNFs φ_{1} and φ_{2} be defined as follows.

φ_{1} = ⋀_{i=1}^{n}(\overline{x}_{i} ∨ \overline{z}_{i}), φ_{2} = ⋀_{i=1}^{n}(\overline{x}_{i} ∨ y_{i}).

Then, the complement of φ_{2} amounts to the formula ⋁_{i=1}^{n} x_{i}\overline{y}_{i} = ⋀_{λ_{i}∈\{x_{i},\overline{y}_{i}\},i=1,2,...,n}(λ_{1} ∨ ⋯ ∨ λ_{n}), and hence the difference of φ_{1} and φ_{2} is described by

φ_{1} \ φ_{2} = ⋀_{i=1}^{n}(\overline{x}_{i} ∨ \overline{z}_{i}) ∧ ⋀_{λ_{i}∈\{x_{i},\overline{y}_{i}\}, i=1,2,...,n}(λ_{1} ∨ ⋯ ∨ λ_{n}).

The prime implicates of φ_{1} \ φ_{2} which are definite (or pure) Horn (i.e., containing exactly one positive literal) are all clauses

x_{i} ∨ λ_{i_{1}} ∨ ⋯ ∨ λ_{i_{n−1}},  (5.45)

such that \{i_{1}, …, i_{n−1}\} = \{1, …, n\}\\{i\} for some i and λ_{i_{j}} ∈ \{\overline{y}_{i_{j}}, \overline{z}_{i_{j}}\} for j = 1, 2, …, n−1. Observe that resolution is not applicable to any pair of such clauses. Consequently, any irredundant prime DNF for φ_{1} \ φ_{2} must contain all clauses (5.45). There are n2^{n−1} such clauses, and hence any Horn CNF for the Horn envelope of φ_{1} \ φ_{2} is exponential in the sizes of φ_{1} and φ_{2}. □

Since the size of the Horn envelope can be exponential, we have to resort to polynomial total time computability as an appropriate concept of tractability. However, from the previous results, we also obtain for this notion a negative result.

Theorem 5.4 There is no polynomial total time algorithm, which, given two Horn CNFs φ_{1} and φ_{2}, computes an (irredundant and prime) Horn CNF for the Horn envelope of φ_{1} \ φ_{2}, unless P = NP.

Proof. The proof is similar to the proof of Theorem 4.13. Assuming that such an algorithm A exists, we can construct an algorithm B that which decides in polynomial time whether φ_{1} is the Horn envelope of φ_{1} \ φ_{2} or not. By Theorem 5.2, this implies P = NP. □

5.2 Model-based representation

In Subsection 3.2, we showed that Cl_{∧}(S_{1}) = Σ_{1} \ Σ_{2} holds if Σ_{1} \ Σ_{2} is Horn, where S_{1} is given by (3.12). It is not difficult to see that, in general, this gives the Horn envelope of Σ_{1} \ Σ_{2}.

Lemma 5.5 Let Σ_{1} and Σ_{2} be Horn theories, and let S_{1} be the set of models defined by (3.12). Then Cl_{∧}(S_{1}) is the Horn envelope of Σ_{1} \ Σ_{2}.

Proof. By (3.13), the Horn envelope Π of Σ_{1} \ Σ_{2} must contain S_{1}. Since Π is Horn, Cl_{∧}(S_{1}) ⊆ Π holds. On the other hand, it follows from (3.14) and (3.16) that Cl_{∧}(S_{1}) ⊇ Σ_{1} \ Σ_{2}. Thus, Π = Cl_{∧}(S_{1}) holds, since Π is the Horn envelope. □

Theorem 5.6 Let Σ_{1} and Σ_{2} be Horn theories, and let Π be the Horn envelope of Σ_{1} \ Σ_{2}. Then, given C^{∗}(Σ_{1}) and C^{∗}(Σ_{2}), C^{∗}(Π) is computable in O(n|C^{∗}(Σ_{1})|^{2}(|C^{∗}(Σ_{1})|^{2} + |C^{∗}(Σ_{2})|)) time.

Proof. By Lemma 5.5, we have to compute C^{∗}(S_{1}). As already shown in the proof of Theorem 3.4, C^{∗}(S_{1}) can be constructed in O(n|C^{∗}(Σ_{1})|^{2}(|C^{∗}(Σ_{1})|^{2} + |C^{∗}(Σ_{2})|)) time. □

6 Discussion and Conclusion

In this paper, we have considered the issue of computing a Horn representation of the difference of two Horn theories Σ_{1} and Σ_{2}. For this purpose, we have presented characterizations of the differences Σ_{1} \ Σ_{2} which are Horn, and algorithms for computing its Horn representation. Moreover, for the case in which Σ_{1} \ Σ_{2} is not Horn, we have characterized and presented algorithms for computing Horn cores and the Horn envelope of Σ_{1} \ Σ_{2}. Our results on the complexity of these issues are summarized in Table 1, which gives a complete picture of the tractability/intractability frontier of these problems. We have considered both the standard representation of Horn theories by means of Horn CNFs, and by the set of its characteristic models [14, 17, 18, 19].

Table 1: Complexity of problems on the Horn difference Σ_{1} \ Σ_{2} (Σ_{1}, Σ_{2} and Π are Horn)

representation

Problem  formula-based (Horn CNF) model-based (characteristic set)
Is Σ_{1} \ Σ_{2} Horn?  P  P

Compute Σ_{1} \ Σ_{2},

if it is Horn P P

Is Π a Horn core

of Σ_{1} \ Σ_{2}? P P

Compute one Horn core

of Σ_{1} \ Σ_{2}  P  P
Compute all Horn cores  polynomial  not polynomial total
of Σ_{1} \ Σ_{2}  delay  time unless P = NP

Is Π the Horn

envelope of Σ_{1} \ Σ_{2}? co-NP-complete P
Compute the Horn  not polynomial total
envelope of Σ_{1} \ Σ_{2}  time unless P = NP  P

Our results on formula-based representation complement the results known from [21, 2, 16, 3, 4]. Observe that these works have focused on theories which are represented by CNFs or restricted classes of CNFs, i.e., the problem input is a (possibly restricted) CNF. In contrast, we deal with non-CNF formulas as a result of the difference operation \. The tractability of computing some Horn core of a Horn difference is a positive result, since this problem is intractable for a general theory. For the case, in which a theory is represented by a CNF formula, [2] contains a polynomial time algorithm which consults an NP oracle, and shows that the problem is P^{NP}[O(log n)]-hard. Most recently, in [1] another algorithm for computing a Horn core from a given CNF is represented, which is based on the classical Davis-Putnam procedure for the satisfiability problem. Observe, however, that these algorithms are not efficiently applicable to our problem, since they require a CNF formula for input; by rewriting the difference of Horn CNFs φ_{1} and φ_{2} to a CNF, the size of the formula might exponentially increase. Our positive result that all Horn cores of a Horn difference φ_{1} \ φ_{2} can be enumerated with polynomial delay parallels the analogous result that the Horn cores of a given theory Σ can be enumerated with polynomial delay [17]. Concerning the Horn envelope, our results complement the intractability results presented in [21, 16, 17, 18, 3]. It was known [21] that the Horn envelope of a CNF φ can be exponential in the size of φ; as already shown, the same holds for the difference of very simple Horn CNFs φ_{1} and φ_{2}. Furthermore, the result that computing the Horn envelope of φ_{1} \ φ_{2} is difficult even if a possible exponential size is taken into account, parallels a similar result for computing an irredundant prime CNF for the Horn envelope of a given theory Σ [17]. A result in [18] suggests that this problem is in fact difficult, and no polynomial total time algorithm is known. On the other hand, it remains open [18] whether such an algorithm would imply P = NP. Thus, finding a polynomial time reduction of computing the Horn envelope of a Horn difference φ_{1} \ φ_{2} to the problem setting in [17, 18] appears to be an intriguing nontrivial and perhaps impossible problem, even though a converse reduction is feasible. (For algorithms computing the Horn envelope of classes of CNFs, see [16, 3, 4] and references therein.) The results of the present and companion papers [6, 7] establish operations towards a Boolean “calculus” on Horn theories, in which Horn theories are combined using the operations of conjunction (∧), disjunction (∨), and difference (\). These operations are useful, for example, in the context of changing theories that are possible world representations of a state of affairs. The paper [6] considered conjunction ∧ for model-based representations of Horn theories. Note that the conjunction of Horn theories is also Horn, and the conjunction of Horn CNFs is also a Horn CNF. Therefore, in this case, we do not need to consider CNF representations and Horn approximation (such as core and envelope). As shown in [6], there exists no polynomial total time algorithm for computing model-based representation for the conjunction of Horn theories, but deciding consistency and deductive question for the conjunction of Horn theories are both polynomial. The paper [7] investigated the problems on the disjunction of Horn theories Σ_{1}, Σ_{2}, …, Σ_{l} similar as in this paper. In particular, we showed that deciding whether the disjunction represents a Horn theory is co-NP-complete in general, but is polynomial if l is bounded by some constant. Several issues remain for further work. One issue is giving a precise account to computing Horn cores and the Horn envelope of the complement \overline{Σ} = \{0, 1\}^{n} \Σ of a Horn theory. Our results imply polynomial time algorithms in some cases, but a complete picture remains to be drawn. Another issue is a more accurate account of the complexity of the polynomial time solvable problems in Table 1. Under formula-based representation, all these problems are complete for P under logspace reductions; this is an easy consequence of the fact that deciding the satisfiability of a Horn CNF is complete for P under logspace reductions, cf. [20]. Therefore, parallelization of these problems is most likely not possible. It remains to see which results can be obtained for the model-based representation. Another interesting issue is a generalization of the results from the propositional to the first order case. Here, in general only formula-based representation is meaningful, and the problems in Table 1 are nonrecursive in general. It remains to single out cases and restrictions under which these problems are effectively solvable. Finally, a study of the effect of Horn renamings (cf. [1]) could be worthwhile.

References

[1] Y. Boufkhad. Algorithms for Propositional KB Approximation. In Proceedings National Conference on AI (AAAI ’98), pages 280–285, Madison, Wisconsin, July 26–30 1998. AAAI Press.

[2] M. Cadoli. Semantical and Computational Aspects of Horn Approximations. In Proceedings International Join Conference on Artificial Intelligence (IJCAI ’93), pages 39–44, Chambery, France, August 1993. Full version, by M. Cadoli and F. Scarcello, (1997) available from the author.

[3] A. del Val. An Analysis of Approximate Knowledge Compilation. In Proceedings IJCAI ’95, pages 830–836, 1995.

[4] A. del Val. Approximate Knowledge Compilation: The First-Order Case. In Proceedings AAAI-96, pages 498–503, 1996.

[5] W. Dowling and J. H. Gallier. Linear-time Algorithms for Testing the Satisfiability of Propositional Horn Theories. Journal of Logic Programming, 3:267–284, 1984.

[6] T. Eiter, T. Ibaraki, and K. Makino. Computing Intersections of Horn Theories for Reasoning with Models. Artificial Intelligence, 110: 57–101, 1999.

[7] T. Eiter, T. Ibaraki, and K. Makino. Disjunctions of Horn Theories and their Cores. In K.- Y. Chwa and O. H. Ibarra, editors, Proceedings Ninth Annual Symposium on Algorithms and Computation (ISAAC ’98), LNCS 1533, pages 49–58, Korea, December 1998. Springer.

[8] T. Eiter, T. Ibaraki, and K. Makino. On the Difference of Horn Theories. In Proceedings 16th International Symposium on Theoretical Aspects of Computer Science (STACS ’99), LNCS 1563, pages 467–477, Germany, March, 1999, Springer.

[9] T. Eiter, T. Ibaraki, and K. Makino. Double Horn Functions. Information and Computation, 144:155–190, 1998.

[10] G. Gogic, C. Papadimitriou, and M. Sideri. Incremental Recompilation of Knowledge. Journal of Artificial Intelligence Research, 8:23–37, 1998.

[11] W. Hodges. Logical Features of Horn Clauses. In D. Gabbay, C. Hogger, and J. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume I : Logical Foundations, pages 449–503. Clarendon Press, Oxford; New York, 1994.

[12] D. S. Johnson, M. Yannakakis, and C. H. Papadimitriou. On Generating All Maximal Independent Sets. Information Processing Letters, 27:119–123, 1988.

[13] H. Katsuno and A. O. Mendelzon. Propositional Knowledge Base Revision and Minimal Change. Artificial Intelligence, 52:253–294, 1991.

[14] H. Kautz, M. Kearns, and B. Selman. Reasoning With Characteristic Models. In Proceedings AAAI-93, pages 34–39, 1993.

[15] H. Kautz, M. Kearns, and B. Selman. Horn Approximations of Empirical Data. Artificial Intelligence, 74:129–245, 1995.

[16] H. Kautz and B. Selman. Knowledge Compilation and Theory Approximation. Journal of the ACM, 43(2):193–224, 1996.

[17] D. Kavvadias, C. Papadimitriou, and M. Sideri. On Horn Envelopes and Hypergraph Transversals. In W. Ng, editor, Proceedings 4th International Symposium on Algorithms and Computation (ISAAC-93), LNCS 762, pages 399–405, Hong Kong, December 1993. Springer.

[18] R. Khardon. Translating between Horn Representations and their Characteristic Models. Journal of Artificial Intelligence Research, 3:349–372, 1995.

[19] R. Khardon and D. Roth. Reasoning with Models. Artificial Intelligence, 87(1/2):187–213, 1996.

[20] C. H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.

[21] B. Selman and H. Kautz. Knowledge Compilation Using Horn Approximations. In Proceedings AAAI-91, pages 904–909, Anaheim, August 1991.