On the Difference of Horn Theories

(Extended Abstract)

Thomas Eiter^{1}, Toshihide Ibaraki^{2}, and Kazuhisa Makino^{3}

1 Institut und Ludwig Wittgenstein Labor für Informationssysteme, Technische Universität

Wien, Treitlstraße 3, A-1040 Wien, Austria. (eiter@kr.tuwien.ac.at) 2 Department of Applied Mathematics and Physics, Graduate School of Informatics, Kyoto University, Kyoto 606, Japan. (ibaraki@kuamp.kyoto-u.ac.jp)

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

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), 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.

Keywords: computational issues in AI, knowledge compilation, Horn approximation

1 Introduction

Among the basic operations for combining logical theories are the Boolean operations, i.e., conjunction ∧, disjunction ∨, and complement ¬. We consider another basic operation, the difference \, which can represent the complement ¬, as for a theory (i.e., set of models) Σ ⊆ {0, 1}^{n}, the complement ¬Σ is given by the difference of {0, 1}^{n} and Σ (i.e., {0, 1}^{n} \ Σ). In principle, these operations are easily accomplished, since the language of propositional logic provides the boolean connectives ∧, ∨, and ¬, which can be applied to combine formulas representing theories. However, if they are from a particular fragment, it is in general desired to know whether their combination also belongs to this fragment, and to find a suitable representation for it.

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, among which Horn cores [11, 12] are quite natural.

A Horn theory Π ⊆ {0, 1}^{n} is a Horn core (or a Horn greatest lower bound) of a theory Σ ⊆ {0, 1}^{n}, if Π ⊆ Σ, i.e., Π logically implies Σ, and there is no weaker Π of this property, i.e., no Horn Π′ exists such that Π ⊂ Π′ ⊆ Σ. Observe that, in general, a theory Σ has more than one Horn core; e.g., Σ = {(110), (101)} has two Horn

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

cores Σ_{1} = {(110)} and Σ_{2} = {(101)}, respectively. Approximating a propositional logic theory by Horn theories (or Horn cores) is used for knowledge compilation in [11]. Because of its theoretical and practical importance, semantical and computational issues on Horn cores have been studied extensively, and a number of results have been obtained, cf. [11, 2, 12, 7, 1].

The main contributions of the present paper can be summarized as follows.

• We present characterizations of the Horn cores 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.)

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

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. The table also shows results on the Horn envelope [11, 12] of the difference, i.e., the (unique) least Horn theory E such that Σ_{1} \ Σ_{2} ⊆ E, which we do not discuss here. The interested reader is referred to [6].

The results on formula-based representation complement the results known from [2, 11, 1]. Observe that these works have focussed 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. 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 result that the Horn cores of a Horn difference φ_{1} \ φ_{2} can be enumerated with polynomial delay parallels the analogous result if all models of a theory Σ are given for input [12].

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. Taking the difference between Horn theories is, for instance, meaningful in the following scenario. 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, the Horn cores and the Horn envelope provide sound and complete approximations of the set Σ_{new} in terms of Horn theories. Our algorithms can be applied 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 [7], in which the theory φ ∘ ψ, given by two Horn CNFs φ and ψ, is studied for some revision operators “∘” (see [9]). However, this is only weakly related to ours, since taking the difference of φ and ψ was not considered, and moreover, the formula ψ is restricted to be a single Horn clause.

For space reasons, most proofs are omitted. They are given in [6].

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 conjunctive normal form (CNF) (resp., disjunctive normal form (DNF)) is a conjunction of clauses φ = ⋀_{i} c_{i} (resp., a disjunction of terms φ = ⋁_{i} t_{i}).

A model is a vector v ∈ {0, 1}^{n}, whose i-th component is denoted by v_{i}. 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 theory is any set Σ ⊆ {0, 1}^{n} of models. A model v ∈ Σ is minimal in Σ, if no w ∈ Σ exists 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 (φ) = Σ. If unambiguous, we do not distinguish a formula from the theory it represents. 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 [10], 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). 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. If φ represents a theory Σ, and ψ is Horn CNF representing a Horn core of Σ, then ψ is also called a Horn core of φ.

3 Horn Property of the Difference

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}. Observe that in general, deciding whether a disjunction of Horn CNFs is Horn is co-NP-complete [5]. However, we sketch a proof that checking the Horn property of the difference of Horn theories is polynomial.

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}).

It can be shown that if v ≠ 1, then

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

holds for the x_{i} such that P (c) = {x_{i}}. On the other hand, if v = 1, then T (φ_{2}) = {1} and it follows

φ_{1} \ φ_{2} ≡ φ_{1}.  (3.4)

Case (2). Clearly (φ_{1} \ φ_{2})(v) = 0. Thus, if φ_{1} \ φ_{2} represents a Horn theory, there exists a Horn clause c^{∗} such that c^{∗} ≥ φ_{1} \ φ_{2} and c^{∗}(v) = 0. Some c in HC(v) then satisfies c ≥ c^{∗}(≥ φ_{1} \ φ_{2}). It can be shown that if v ≠ 1, then

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

holds, where the x_{i} appears in c (i.e., P (c) = {x_{i}}).

On the other hand, if v = 1, then in a manner similar to (3.4), we prove

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

Now we iterate as long as possible. As soon as φ_{2} = ⊥ or v = 1 holds, we can conclude that φ_{1} \ φ_{2} is Horn by (3.2), (3.4) or (3.6). If there is no c ∈ HC(v) such that c ≥ φ_{1} \ φ_{2}, then φ_{1} \ φ_{2} is not Horn. In the remaining cases, we apply (3.3) or (3.5) (i.e., φ_{1} is modified to φ_{1} ∧ c in case of (3.5), and φ_{2} to φ_{2} ∧ x_{i} in both cases).

It can be shown that this procedure halts in finitely many steps. 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 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} as above and φ′_{2} = \overline{x}_{4}∧(\overline{x}_{2}∨\overline{x}_{3}). Then, φ_{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 as previous. Now, φ_{1} \ φ′_{2} ≤ x_{4} holds. Hence, we update ϕ_{1} to ϕ_{1} = ϕ_{1} ∧ x_{4} and ϕ_{2} to ϕ_{2} ∧ x_{4}. Returning to Step 1, we find that ϕ_{2} ≡ ⊥ holds. Hence,

ϕ_{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. □

An analysis of the time complexity yields the first result. Note φ ≡ ⊥ for Horn φ is decidable in linear time [3], and that by (3.1), a Horn difference φ_{1} \φ_{2} is representable as Horn disjunction ψ_{1}∨⋯∨ψ_{m_{2}}. Thus, c ≥ φ_{1}\φ_{2} is equivalent to Horn ψ_{i}∧¬c ≡ ⊥ for all i = 1, 2, …, m_{2}.

Theorem 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.

3.2 Model-based representation

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.7)

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:

S_{1} ∩ Σ_{2} = ∅ and S_{2} ⊆ Σ_{2}.  (3.8)

It is easy to see that S_{1} ⊆ Σ_{1} \ Σ_{2} and Cl_{∧}(S_{2}) ⊆ Σ_{2}.

Lemma 1. For a Horn theory Σ, let S as in (3.7), 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}) = Σ.

By this lemma, it holds for the S_{1} and S_{2} of (3.8) that

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

The next lemma leads then to a polynomial time algorithm for our problem.

Lemma 2. Let Σ_{1} and Σ_{2} be Horn theories, and let S_{1} as in (3.8). 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.

It is known [4] that given Q_{1}, Q_{2} ⊆ {0, 1}^{n}, deciding Cl_{∧}(Q_{1}) ∩ Cl_{∧}(Q_{2}) = ∅ is possible in O(n(|Q_{1}| + |Q_{1}|)) time. Since Σ_{2} = Cl_{∧}(C^{∗}(Σ_{2})), we thus obtain from Lemma 2, turned into a straightforward algorithm, the following result.

Theorem 2. Let Σ_{1}, Σ_{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.

4 Horn Cores

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 no Horn clause c is 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 v.

Denote for a formula ψ and a model w, by min_{≥w}(ψ) the set of minimal models u such that ψ(u) = 1 and u ≥ w. Then, it holds that any clause c ∈ HC(v) such that c(u) = 1 for some u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}) is appropriate for our purpose.

For models v, u with v ≤ u, let HC(v; u) be the set of Horn clauses c ∈ HC(v) whose positive literal x_{j} satisfies u_{j} = 1. E.g., 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, based on a model u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}), we update ϕ_{1} and ϕ_{2} respectively by

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

Thus, we have the following algorithm.

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

Steps 0.–2. as in CHECK-HORN

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. □

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

v^{(k)} < v^{(k+1)},  for k = 1, 2, . . ..  (4.11)

This implies that the number of iterations is at most n + 1. The only nonobvious polynomial operation in HORN-CORE1 is finding some u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}) in Step 3. The models {w ≥ v | (ϕ_{1} \ ϕ_{2})(w) = 1} can be described by a disjunction of m Horn CNFs ψ_{1}, …, ψ_{m}, where m is the number of clauses in ϕ_{2}. Consequently, the models in min_{≥v}(ϕ_{1}\ϕ_{2}) are the minimal models among the least models of ψ_{1}, …, ψ_{m}. Each ψ_{i} results by fixing the value of some literals in ϕ_{1}, and its least model can be computed in O(|ϕ_{1}| + n) time exploiting [3]. Looking at the number of 1-bits in each model, we can thus find some u ∈ min_{≥v}(ϕ_{1} \ ϕ_{2}) in O(m(|ϕ_{1}| + n) + mn) = O(m(|ϕ_{1}| + n)) time. An analysis of the time complexity gives us then the following result.

Theorem 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.

As regards computing all Horn cores of φ_{1} \ φ_{2}, we note that this problem is provably not solvable in polynomial time, since in general, an exponential number of Horn cores might exist [6]. However, we have a polynomial total time algorithm (called output-polynomial in [8]), i.e., it runs in polynomial time in the combined size of the input and the output. In fact, it enumerates all Horn cores with polynomial delay [8].

Note 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}). We can also show 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.

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}.

Steps 0.–2. as in HORN-CORE1 and CHECK-HORN.

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}. □

An analysis of the time complexity leads us to the following result.

Theorem 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}|).

4.2 Model-based representation

In Subsection 3.2, we have seen that S_{1} of (3.8) 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}.

Theorem 5. Let Σ_{1}, Σ_{2} be Horn theories and let S as in (3.7). Then, Π is a Horn core of Σ_{1} \ Σ_{2} iff Π = Cl_{∧}(Q) for some maximal Q ⊆ S such that Cl_{∧}(Q) ∩ Σ_{2} = ∅. □

Based on Theorem 5, we obtain the following polynomial time algorithm.

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.7); 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. □

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

Is also possible to decide whether a given theory Π is a Horn core of the difference Σ_{1} \ Σ_{2} in polynomial time. A suitable algorithm is straightforward by proper modification of algorithm HORN-CORE2. We omit the details (see [6]).

As for the efficient computation of all Horn cores, we have a negative result. There is no polynomial total time algorithm for generating all Horn cores, unless P = NP.

Theorem 7. There is no algorithm which, given 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.

5 Conclusion and Further Work

The results of the present and companion papers [4, 5] 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.

Several issues remain for our ongoing work. One 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 cases 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. Therefore, parallelization of these problems is most likely not possible. Another interesting issue is a study of the effect of Horn renamings (cf. [1]).

Acknowledgments. The authors appreciate the comments of the anonymous reviewers.

References

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

2. M. Cadoli. Semantical and Computational Aspects of Horn Approximations. In Proc. IJCAI-93, pp. 39–44, 1993.

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

4. T. Eiter, T. Ibaraki, and K. Makino. Computing Intersections of Horn Theories for Reasoning with Models. In: Proc. AAAI ’98, pp. 292–297, 1998.

5. T. Eiter, T. Ibaraki, and K. Makino. Disjunctions of Horn Theories and their Cores. In Proc. 9th Int’l Symp. on Algorithms and Computation (ISAAC ’98), Dec. 1998.

6. T. Eiter, T. Ibaraki, and K. Makino. On the Difference of Horn Theories. RUTCOR Research Report RRR 25-98, Rutgers University 1998.

7. G. Gogic, C. Papadimitriou, and M. Sideri. Incremental Recompilation of Knowledge. J. Artificial Intelligence Research, 8:23–37, 1998.

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

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

10. H. Kautz, M. Kearns, and B. Selman. Reasoning With Characteristic Models. In Proc. AAAI ’93, 1993.

11. H. Kautz and B. Selman. Knowledge Compilation and Theory Approximation. JACM, 43(2):193–224, 1996.

12. D. Kavvadias, C. Papadimitriou, and M. Sideri. On Horn Envelopes and Hypergraph Transversals. In Proc. ISAAC ’93, LNCS 762, pp. 399–405, 1993.

13. R. Khardon and D. Roth. Reasoning with Models. Art. Intelligence, 87(1/2):187–213, 1996.