The Size of a Revised Knowledge Base ^{∗}

Marco Cadoli Francesco M. Donini Paolo Liberatore Marco Schaerf

Dipartimento di Informatica e Sistemistica

Università di Roma “La Sapienza”

via Salaria 113, I-00198 Roma, Italy

                 email: <lastname>@dis.uniroma1.it

Abstract

In this paper we address a specific computational aspect of belief revision: The size of the propositional formula obtained by means of the revision of a formula with a new one. In particular, we focus on the size of the smallest formula which is logically equivalent to the revised knowledge base. The main result of this paper is that not all formalizations of belief revision are equal from this point of view. For some of them we show that the revised knowledge base can be represented by a polynomial-size formula (we call these results “compactability” results). On the other hand we are able to prove that for other ones the revised knowledge base does not always admit a polynomial-space representation, unless the polynomial hierarchy collapses at a sufficiently low level (“non-compactability” results). The time complexity of query answering for the revised knowledge base has definitely an impact on being able to represent the result of the revision compactly. Nevertheless formalisms with the same complexity may have different compactability properties. We also study compactability properties for a weaker form of equivalence called query equivalence which allows to introduce new propositional symbols, and for the special case in which the new formula has constant size. Moreover we extend our analysis to sequences of revisions (i.e., iterated belief revision). A complete analysis along these four coordinates is shown.

1 Introduction

In many areas of computer science, such as Databases and Artificial Intelligence (AI), we are faced with the problem of constructing and maintaining up-to-date large bodies of information. How can new facts be added to an existing database (or knowledge base)? Intuition might suggest that we simply conjoin the formula P, representing the new information, with our previous information T. However, this would destroy consistency when T and P contradict each other. Moreover, even when T and P are compatible, simply conjoining them might not lead to the desired result, as we illustrate below.

∗An extended abstract of this paper appeared as [CDLS95].

As remarked by Winslett in [Win90], the problem of finding general methodologies to update and revise data and knowledge bases has been studied in at least three research communities. In the AI community, the problem of revising a set of beliefs naturally arises when we want to construct an artificial agent that is able to operate in the real world. Since the real world undergoes frequent changes the agent must be able to revise and modify its beliefs accordingly to the new information acquired, without losing an overall consistency. In the Database community problems with updates arose when incompleteness started being introduced in a database via the use of null values and the update of views (see, e.g. [BS81]). Finally, philosophers have analyzed the meaning of belief revision from the time of Aristotle. Recently, Alchourrón, Gärdenfors and Makinson [AGM85, Gär88] have presented a general framework for belief revision where the basic properties of belief revision are introduced and discussed.

Revision of logical theories comes in two flavors, which are known in the literature as belief revision and knowledge base update. To see intuitively their similarities and differences, we consider the following temporal diagram, representing that 1) our knowledge at time t_{1} was T, and 2) at time t_{2} we come to know that P is true.

t t^{2} t^{1}  P T  ^{}

After t_{2} there is no doubt we have to assume that P is true, because it represents the most recent observation. As far as T is concerned, things are not so obvious, since T ∧ P might be unsatisfiable. Anyway, a general principle seems to be that we should retain some of the information of T, if possible.

The main assumption in belief revision is that T was (at least partially) wrong at time t_{1}, because it came from non-valid observations. On the other hand in update we assume that T was true at time t_{1}, but the world of interest has changed between t_{1} and t_{2}, so T is no longer true after t_{2}. The following example clarifies the two approaches.

Example. George and Bill share an office near yours, and you wonder whether they are in the office or not. In what follows, propositional letters g and b denote that George is in the office and Bill is in the office, respectively.

Revision. Walking in the corridor, you hear someone talking in the office but you don’t recognize his voice. Thus, you suppose that either George or his colleague is in the office, and your knowledge is T = g ∨ b. Just beyond the corner you see George chatting with someone. This can be formalized as P = ¬g, so your conclusion is that the voice you heard was Bill’s one (because T ∧ P ≡ ¬g ∧ b). A fundamental property of revision is that if T ∧ P is not contradictory then the result of revising T with P is simply T ∧ P.

Update. Similarly to the previous case, in the morning you are walking in the corridor and hear a voice from the office. Then, you leave the building, come back later in the afternoon, and meet George in the corridor. T and P are exactly the same as in the previous case. Nevertheless, you do not conclude that Bill was in his office in the morning, because there is no evidence supporting this conclusion. It is possible that you heard George’s voice, and he left his office while you were outside the building. The only fact you know for sure is P. An interesting property of update is therefore that even if T ∧ P is consistent the update of T with P is not necessarily equal to the conjunction of the two formulas.

More details on the difference between revising a knowledge base and updating it can be found in [KM91]. From now on, unless when explicitly stated, we will generically talk about revision of knowledge. In symbols, we denote with T ∗ P the result of the revision of T with P. Both T and P are propositional formulae.

Proposed formalizations of belief revision are very different in spirit, but, following Eiter and Gottlob’s [EG92] presentation, they can be classified according to three orthogonal criteria.

• Irrelevance of syntax. Some of the approaches perform the revision by adding to T the update formula P and retracting some sub-formula of T, in order to preserve consistency. Such methods (e.g. [FUV83, Gin86, Neb91]) are known as formulabased approaches. On the other hand, most approaches deal with the models of T, thus not taking into account the syntactic presentation of the knowledge bases. Such methods (e.g. [Bor85, Dal88, For89, Sat88, Web86, Win90]) are known as model-based approaches.

• Measure of closeness. In model-based approaches the underlying idea is that the models of T ∗ P are the models of P plus some of the models of T. Only the models of T which are closest to the models of P are added. Each formalism has its own definition of what being closer means.

• Revision versus update which we explained intuitively above.

Other researchers [EG92, Neb91, Win90, LS96] focused on computational properties of belief revision. As an example, they addressed questions such as: Given formulae T, P, Q and a suitable semantics for the revision operator ∗, what is the time complexity of deciding T ∗ P ⊧ Q? In which cases polynomial algorithms exist? Same questions have been asked for the problem of deciding M ⊧ T ∗ P, where M is an interpretation.

Both aspects of belief revision (semantic and computational) are important from the theoretical as well as the practical point of view.

In this paper we address a new specific computational aspect of belief revision: The size of the revised theory T ∗ P. An informal description of our work follows. We insist that T ∗ P is represented as a propositional theory, i.e., we want a propositional theory T′ such that

{Q | T′ ⊧ Q} = {Q | T ∗ P ⊧ Q},  (1)

Q being any formula where only symbols of T or P occur. We call this property query equivalence, and we say that a T′ satisfying the above criterion is query equivalent to T ∗ P.

The reason why we insist on T ∗ P being a propositional theory is twofold. From the epistemological point of view, it seems reasonable that our set of beliefs does not change the format of its representation after being revised. From the computational point of view, it would be nice to split the task of deciding T ∗P ⊧ Q into two subtasks:

1. compute T′ such that (1) holds;

2. decide T′ ⊧ Q.

There are two positive aspects in such a computational approach: The first subtask can be done off-line, i.e., not necessarily when the query Q arrives. Moreover we could use the same set of algorithms and heuristics both for subtask 2 and for regular query answering.

A question now naturally arises: What is the size of such a T′? If the size of the smallest T′ is super-polynomial in the size of T plus the size of P, then the above mentioned approach to query answering is clearly not practical. Moreover the cognitive plausibility of belief revision as a model of evolution of the mind of an agent is questionable: An agent would either need an unreasonable amount of storing space, or change the format it uses to represent knowledge. The main result of this paper is that not all formalizations of belief revision are equal from this point of view. For some of them (e.g., Dalal’s [Dal88]) we show that T′ admits a polynomial-space representation (we call these results “compactability” results). On the other hand we are able to prove that for other ones (e.g., Ginsberg-Fagin-Ullman-Vardi’s [Gin86, FUV83] and Forbus’ [For89]) T′ does not always admit a polynomial-space representation, unless the polynomial hierarchy collapses at a sufficiently low level (“non-compactability” results). The time complexity of answering T ∗ P ⊧ Q on-line (T, P and Q being the input) has definitely an impact on being able to represent T′ compactly, although formalisms with the same time complexity may have different compactability properties.

Winslett addresses this problem in [Win90] for the specific case where the size of P is bounded by a constant, showing several compactability results. We give a complete analysis, proving that some formalisms (e.g., Ginsberg-Fagin-Ullman-Vardi’s) are not compactable even in such a restricted case, while other ones (e.g., Forbus’) are compactable.

A further aspect we address is the representation of a revised knowledge base using a form of equivalence characterized by the following requirement

T′ ≡ T ∗ P  (2)

We call this property logical equivalence, and we say that a T′ satisfying the above criterion is logically equivalent to T ∗ P. Notice that a T′ satisfying logical equivalence (2) satisfies query equivalence (1) as well, but not the other way around. Basically, query equivalence (1) gives the possibility of introducing new propositional letters, hence it yields formulae T′ with less information (e.g., model checking wrt T′ gives different results in the two cases). This has definitely an impact on compactability: As an example, Dalal’s formalization admits compact representations only according to criterion (1).

As further information arrives continuously, it may happen that a revised knowledge base needs to be revised once again. In general, we talk about iterated belief revision when an unbounded number of revisions occur. As far as the size is concerned, if a formula is compactable after a single revision then it is not guaranteed that it is compactable after several revisions. As an example, we show that Forbus’ operator —which admits compact representations for the bounded revision/logical equivalence case— admits polynomially-sized iteratively revised formulae only according to the query equivalence criterion, but not for the logical equivalence criterion.

Summing up, we provide a complete characterization of the compactability properties for belief revision operators along four coordinates:

1. the formalism;

2. bounded vs. unbounded size of the new formula P;

3. logical equivalence vs. query equivalence;

4. single revision vs. iterated revision.

For what concerns non-compactability results, we use concepts such as Turing machines with advice and non-uniform complexity classes, as well as results relating uniform and non-uniform complexity classes. In fact, our results not only show unlikeliness of propositional representations of revised theories, but are valid for a generic (in the sense of Section 7) data structure. As for compactability results, we show effective procedures for obtaining compact representations.

The structure of the paper is as follows: Section 2 contains definitions about theories of belief revision and non-uniform complexity classes. Section 3 contains the analysis for the unbounded-size case; we prove compactability as well as non-compactability results. Section 4 contains the analysis for the bounded-size case, while Sections 5 and 6 deal with iterated belief revision, in the unbounded-size and bounded-size case, respectively. Section 7 presents results for generic data structures and Section 8 contains some conclusions.

2 Preliminaries

The alphabet of a propositional formula is the set of all propositional letters occurring in it. The special letter ⊥ denotes falsity. We use x ≢ y as a shorthand for (x ∨ y) ∧ (¬x ∨ ¬y), and x ≡ y for (x ∧ y) ∨ (¬x ∧ ¬y). Another shorthand we use is x → y for ¬x ∨ y. An interpretation of a formula is a truth assignment to the letters of its alphabet. A theory T is a set of propositional formulae. We denote with ⋀ T the formula representing the logical “and” of all elements of T. When no confusion arises, we simply write T for ⋀ T. A model M of a formula P (theory T) is an interpretation that satisfies P (all formulae in T). This is written M ⊧ P (M ⊧ T). Interpretations and models of propositional formulae will be denoted as sets of letters (those which are mapped into true). ⊥ is always mapped into falseand ⊤ is always mapped into true. Given a propositional theory T, we denote with M(T) the set of its models. The expression |s| denotes the size of s.

Several notational convention help presenting the revision operators. In particular, the expression card(S) denotes the cardinality of a set S, and symmetric difference between two sets S_{1}, S_{2} is denoted by S_{1}ΔS_{2}. Recall that Δ is an associative and commutative operator, with ∅ as its neutral element.

If S is a set of sets, ∩S denotes the set formed intersecting all sets of S, and analogously ∪S for union; min_{⊆}S denotes the subset of S containing only the minimal (wrt set inclusion) sets in S; max_{⊆}S denotes the subset of S containing only the maximal (wrt set inclusion) sets in S.

Given a propositional theory T we denote with V (T) the letters appearing in T. In the paper we frequently use the notion of substitution of letters in a formula. The notation P [x/y] denotes the formula P where every occurrence of the letter x is replaced by the formula y. This notation is generalized to ordered sets: P [X/Y] denotes the formula P where all occurrences of letters in the set X are simultaneously replaced by the corresponding elements in Y, where X is an ordered set of letters (in general, X ⊆ V (P)) and Y is an ordered set of formulae with the same cardinality. For example, let Q be the formula x_{1} ∧ (x_{2} ∨ ¬x_{3}). Let X = {x_{1}, x_{3}} and Y = {y_{1}, ¬y_{3}}. Then, Q[X/Y] is the formula y_{1} ∧ (x_{2} ∨ ¬¬y_{3}).

2.1 Non-uniform complexity classes

As already pointed out, our proofs use the notion of non-uniform computation. We assume the reader is familiar with (uniform) classes of the polynomial hierarchy (P, NP, Σ_{2}^{p}, … and their complements), and we just briefly introduce non-uniform classes, following Johnson [Joh90].

Definition 2.1 An advice-taking Turing machine is a Turing machine that has associated with it a special “advice oracle” A, which can be any function (not necessarily a recursive one). On input s, a special “advice tape” is automatically loaded with A(|s|) and from then on the computation proceeds as normal, based on the two inputs, x and A(|s|).

Note that the advice is only function of the size of the input, not of the input itself.

Definition 2.2 An advice-taking Turing machine uses polynomial advice if its advice oracle A satisfies |A(n)| ≤ p(n) for some fixed polynomial p and all nonnegative integers n.

Definition 2.3 If C is a class of languages defined in terms of resource-bounded Turing machines, then C/poly is the class of languages defined by Turing machines with the same resource bounds but augmented by polynomial advice.

Any class C/poly is also known as non-uniform C, where non-uniformity is due to the presence of the advice. Non-uniform and uniform complexity classes are related in [KL80, Yap83]. In particular, Karp and Lipton proved in [KL80] that if NP ⊆ P/poly then Π_{2}^{p} = Σ_{2}^{p} = PH, i.e. the polynomial hierarchy collapses at the second level, while Yap in [Yap83, pg. 292 and Theorem 2] generalized their results showing that if NP ⊆ coNP/poly then Π_{3}^{p} = Σ_{3}^{p} = PH, i.e. the polynomial hierarchy collapses at the third level. Such a collapse is considered very unlikely by most researchers in structural complexity.

2.2 Revision operators

We now recall the different approaches to revision and update, classifying them into formula-based and model-based ones. A more extensive exposition can be found in [EG92]. The boldface name prefixed to each approach will be used for further reference.

2.2.1 Formula-based approaches

Formula-based revisions operate on the formulae syntactically appearing in the theory T. Let W (T, P) be the set of maximal subsets of T which are consistent with the revising formula P:

W (T, P) = max_{⊆}{T′ ⊆ T | T′ ∪ {P } |̸= ⊥}

GFUV. In [FUV83] and in [Gin86], the revised theory is defined as a set of theories: T ∗_{GF UV} P ≐ {T′∪{P } | T′ ∈ W (T, P)}. Each theory of this set has been called “world” by Ginsberg, with no reference to possible worlds in modal logics. Logical consequence in the revised theory is defined as logical consequence in each of the theories, i.e. T ∗_{GF UV} P ⊧ Q iff for all T′ ∈ W (T, P), T′ ∪ {P } ⊧ Q. If a theory T′ is also viewed as the conjunction of its formulae ∧T′, this consequence relation corresponds to consequence from the disjunction of all theories. Hence, as far as logical equivalence is concerned, we consider T ∗_{GF UV} P as being equivalent to (⋁_{T′∈W (T,P)}(∧T′)) ∧ P.

Nebel. The operator ∗_{N}, proposed in [Neb91], is an extension of Ginsberg-Fagin-Ullman-Vardi’s one, in which the new theories are built based on a prioritized partition of the formulae in T.

WIDTIO. Since there may be exponentially many new theories in T ∗_{GF UV} P, a simpler (but somewhat drastic) approach is the so-called WIDTIO (When In Doubt Throw It Out), which is defined as T ∗_{W id} P ≐ (∩W (T, P)) ∪ {P }.

Note that formula-based approaches are sensitive to the syntactic form of the theory. That is, the revision with the same formula P of two logically equivalent theories T_{1} and T_{2} may yield different results. We illustrate this fact through an example.

Example. Consider T_{1} = {a, b}, T_{2} = {a, a → b} and P = ¬b. Clearly, T_{1} is equivalent to T_{2}. The only maximal subset of T_{1} consistent with P is {a}, while there are two maximal consistent subsets of T_{2}, that are {a} and {a → b}.

Thus, T_{1} ∗_{GF UV} P = {a ∧ ¬b} while T_{2} ∗_{GF UV} P = {(a ∨ (a → b)) ∧ ¬b} = {¬b}. The WIDTIO revision gives the same results.

2.2.2 Model-based approaches

Model-based revisions obey the principle of “irrelevance of syntax” [Dal88]. They operate by selecting the models of P on the basis of some notion of proximity to the models of T. We distinguish between pointwise proximity and global proximity.

Approaches in which proximity between models of P and models of T is computed pointwise wrt each model of T were proposed as suitable for knowledge update [KM91]. Let M be a model of T; we define μ(M, P) as the set containing the minimal (wrt set inclusion) symmetric differences Δ between each model of P and the given M; more formally, μ(M, P) ≐ min_{⊆}{MΔN | N ∈ M(P)}.

Winslett. In [Win90], Winslett defines the models of the updated theory as M(T ∗_{W in} P) ≐ {N ∈ M(P) | ∃M ∈ M(T) : MΔN ∈ μ(M, P)}.

Borgida. Borgida’s operator ∗_{B} is the same as Winslett’s, except for the case when P is consistent with T, in which case Borgida’s revised theory is just T ∪ {P }.

Forbus. This approach [For89] takes into account cardinality: let k_{M,P} be the minimum cardinality of sets in μ(M, P). The models of Forbus’ updated theory are M(T ∗_{F} P) ≐ {N ∈ M(P) | ∃M ∈ M(T) : card(MΔN) = k_{M,P} }. Note that by means of cardinality, Forbus can compare (and discard) models which are incomparable in Winslett’s approach.

We now recall approaches where proximity between models of P and models of T is defined considering globally all models of T. Let δ(T, P) ≐ min_{⊆} ⋃_{M∈M(T)} μ(M, P).

Satoh. In [Sat88], the models of a revised theory are defined as M(T ∗_{S} P) ≐ {N ∈ M(P) | ∃M ∈ M(T) : NΔM ∈ δ(T, P)}.

M(T ∗_{F} P)  M(T ∗^{D} P)  M(T ∗_{S} P)  M(T ∗_{W eb} P) M(T ∗_{W in} P)

Figure 1: Containment between sets of models for the various operators.

Dalal. This approach is similar to Forbus’, but global. Let k_{T,P} be the minimum cardinality of sets in δ(T, P); in [Dal88], Dalal defines the models of a revised theory as M(T ∗_{D} P) ≐ {N ∈ M(P) | ∃M ∈ M(T) : card(NΔM) = k_{T,P} }.

Weber. Let Ω ≐ ∪δ(T, P), i.e. Ω contains every letter appearing in at least one minimal difference between a model of T and a model of P. Following [EG92, p. 238], the models of Weber’s revised theory [Web86] are defined as M(T ∗_{W eb} P) ≐ {N ∈ M(P) | ∃M ∈ M(T) : NΔM ⊆ Ω}.

From the definitions it follows that the set of models relative to the model-based approaches are related as described in Figure 1, where each arrow denotes set containment.

To illustrate the differences between different model-based approaches, consider the following example.

Example. Let T and P be two formulae on the alphabet {a, b, c, d} defined as:

T = a ∧ b ∧ c
P = (¬a ∧ ¬b ∧ ¬d) ∨ (¬c ∧ b ∧ (a ≢ d))

T has only two models, which are:

M_{1} = {a, b, c, d}
M_{2} = {a, b, c}

while P has four models:

N_{1} = {a, b}

N_{2} = {c}
N_{3} = {b, d}
N_{4} = ∅

The symmetric differences between each model of T and each model of P are:

\begin{matrix}Δ & N_{1} = \{a, b\} & N_{2} = \{c\} & N_{3} = \{b, d\} & N_{4} = ∅ \\ M_{1} = \{a, b, c, d\} & \{c, d\} & \{a, b, d\} & \{a, c\} & \{a, b, c, d\} \\ M_{2} = \{a, b, c\} & \{c\} & \{a, b\} & \{a, c, d\} & \{a, b, c\} \end{matrix}

Hence, the minimal differences between M_{1} and models of P are μ(M_{1}, P) = {{c, d}, {a, b, d}, {a, c}}; the minimal differences between M_{2} and models of P are μ(M_{2}, P) = {{c}, {a, b}}.

The cardinalities of set differences between each model of T and each model of P are:

\begin{matrix}|Δ| & N_{1} = \{a, b\} & N_{2} = \{c\} & N_{3} = \{b, d\} & N_{4} = ∅ \\ M_{1} = \{a, b, c, d\} & 2 & 3 & 2 & 4 \\ M_{2} = \{a, b, c\} & 1 & 2 & 3 & 3 \end{matrix}

Winslett. The minimal differences in μ(M_{1}, P) correspond to the models N_{1}, N_{2}, N_{3} of P, while those in μ(M_{2}, P) correspond to the models N_{1}, N_{2} of P. Therefore, the models of T ∗_{W in} P are N_{1}, N_{2}, N_{3}. The same result holds for Borgida’s revision, since T and P are inconsistent.

Forbus. From the table with cardinalities: the minimum cardinality of differences between M_{1} and each model of P is k_{M_{1},P} = 2, corresponding to models N_{1} and N_{3}; while k_{M_{2},P} = 1, corresponding to N_{1}. Therefore, T ∗_{F} P has models N_{1} and N_{3}.

We now turn to global proximity approaches, where also entries in different rows of the above tables are compared for minimality.

Satoh. The minimal differences between any model of T and any model of P are δ(T, P) = {{c}, {a, b}}. These minimal differences correspond to models N_{1} and N_{2} of P, which therefore are the models of T ∗_{S} P.

Dalal. The minimum cardinality of all set differences is k_{T,P} = 1, corresponding to N_{1}. As a result, T ∗_{D} P selects only the model N_{1}.

Weber. Consider the union of all minimal global differences, that is Ω = ∪δ(T, P) = {a, b, c}. In Weber’s revision, one selects the models of P for which there exists a model of T whose symmetric difference is included in Ω. Since all models of P have this property (cf. table with symmetric differences), they are all selected. Thus, the revision coincides with P in this case.

There is an important property of model-based revision operators that we frequently use in the sequel:

Proposition 2.1 Let M be a model of T and ∗ one of the revision operators {∗_{B}, ∗_{D}, ∗_{F} , ∗_{S}, ∗_{W eb}, ∗_{W in}}. Then, there exists a model N of T ∗ P such that MΔN ⊆ V (P).

This property states that for every model of T there exists a model of T ∗ P whose distance is bounded by the letters of P. This is sometimes crucial in showing the existence of compact representations since it allows to focus our attention only on the letters of P. This proposition is mentioned by Eiter and Gottlob in [EG92, proof of Lemma 6.1].

2.2.3 Iterated Revision

All the operators proposed in the literature aim at formalizing the process of revising a formula with a single update. Nevertheless, it is more realistic to formalize the result of applying a series of revisions or updates to an existing knowledge base. The iterated application of an update or revision operator is defined as follows: Given a theory T and a sequence of updates P^{1}, …, P^{m}, the m-times repeated application of ∗ is (⋯ (T ∗ P^{1}) ⋯ ∗ P^{m}). That is, the result of revising T with P^{1} is revised with P^{2} and so on. In order to simplify the notation, we assume that the revision operator ∗ is left associative. Thus, the result of revising the theory T with a series of updates P^{1}, …, P^{m} will be denoted as T ∗ P^{1} ∗ ⋯ ∗ P^{m}.

There are at least two possible computational approaches to deal with iterated revision. The first approach incorporates each revision one-by-one into the knowledge base, while the second approach stores the initial knowledge base and the sequence of update formulae and computes the result in a single step. As we show in Sections 5 and 6, the second approach leads to compact representations in a larger set of cases.

2.2.4 Complexity of Revision

As shown in the sequel, the existence of compact representations for the revised knowledge base is related to the complexity of model checking and inference for the various revision operators. The complexity of these decision problems have been analyzed in various papers. The complexity of deciding T ∗ P ⊧ Q (T, P and Q being the input) was studied in [EG92]. The results are that in Dalal’s approach the problem is Δ_{2}^{p}[log n]-complete, while in all other approaches it is Π_{2}^{p}-hard (in some cases, Π_{2}^{p}- complete).

The complexity of model checking, that is, the complexity of deciding whether M ⊧ T ∗ P (where M is an interpretation and M, T and P are the input) is analyzed in [LS96]. Noticeably, formalisms with the same complexity wrt inference have different complexity wrt model checking (e.g. Satoh’s and Ginsberg-Fagin-Ullman-Vardi’s operators).

The complexity of inference for iterated revision was analyzed by Eiter and Gottlob in [EG93].

2.3 Compact Representations

In this paper we investigate the possibility of compactly representing, with a propositional formula, the result of an update or revision. We point out that the result of all revision and update methods presented in Section 2.2 can be represented as a propositional formula. However, it is difficult to know what is the size of the shortest formula representing the result. Here we formally define which are the properties of the operators we presented before wrt such a problem.

We call an operator logically-compactable if there exists a propositional formula of polynomial size logically equivalent to the result of the revision. More precisely:

Definition 2.4 (logically-compactable operator) An update or revision operator ∗ is logically-compactable if and only if there exists a polynomial p such that for any pair of propositional formulae T and P there exists a propositional formula T′ with the following properties:

1. |T′| ≤ p(|T | + |P |);

2. T′ is logically equivalent (cf. (2)) to T ∗ P.

In order to prove that some belief revision operators are not logically-compactable we show that this would imply some very unlikely consequences on complexity classes. We now prove a general property that will be helpful in the proofs of the following sections.

A decision problem, seen as the infinite set of its instances, can be partitioned according to the size of the instances for a reasonable encoding (in the sense of [Joh90]) of the instances. In particular, we focus on the NP-complete problem 3-sat [GJ79, Problem LO2].

Definition 2.5 We partition the set of instances as 3-sat = ⋃_{n=1}^{∞} 3-sat_{n}, according to their size n. For each n, we know that the number of distinct propositional letters occurring in each instance of 3-sat_{n} is at most n. Without loss of generality, we assume that all formulae of 3-sat_{n} are built on the same set of atoms B_{n} = {b_{1}, …, b_{n}}. For each n, π_{n}^{max} is defined as the set of all the three-literal clauses on {b_{1}, …, b_{n}}.

Note that π_{n}^{max} has size polynomial in n; in particular it has Θ(n^{3}) clauses, and each literal can be represented with Θ(log n) bits. Moreover, each instance π ∈ 3-sat_{n}, considered as a set of clauses, is a subset of π_{n}^{max} ∈ 3-sat. In Theorems 2.2 and 2.3 of this section, and in Theorems 3.1, 3.3, 3.6, 6.3 and 6.6 of the following ones, we refer to such a partition of 3-sat, and the related notation.

Theorem 2.2 Let ∗ be a revision operator. Assume there exists a polynomial p such that, for each n > 0, there exists a pair of formulae T_{n}, P_{n} with the following properties:

1. |T_{n}| + |P_{n}| ≤ p(n);

2. for all π ∈ 3-sat_{n}, there exists an interpretation M_{π} of T_{n} ∗ P_{n} such that:

(a) M_{π} can be computed from π in polynomial time;

(b) M_{π} ⊧ T_{n} ∗ P_{n} iff π is satisfiable.

With the above hypothesis, if ∗ is logically-compactable, then NP ⊆ P/poly.

Proof. Assume there exists a polynomial p such that, for each n, there exists a pair of formulae T_{n}, P_{n} with the properties stated. Now, assume ∗ is logically-compactable. Hence, for each pair T_{n}, P_{n} there exists a T′_{n} with properties stated in Definition 2.4. Recall that checking whether M ⊧ T′_{n} (the input being M, T′_{n}) is a polynomial-time problem. Then we can define an advice-taking Turing machine in the following way.

First, we define the advice oracle as A(n) = T′_{n}. Observe that |A(n)| = |T′_{n}| ≤ p_{1}(|T_{n}| + |P_{n}|) ≤ p_{1}(p(n)), where p is the polynomial mentioned in the hypothesis 1 of the theorem, and p_{1} is the polynomial mentioned in point 1 of Definition 2.4. Hence, the size of the advice is bounded by a polynomial which is the composition of p_{1} and p.

Secondly, the machine operates as follows: given an instance π of 3-sat, with |π| = n, the machine loads A(|π|) = A(n) = T′_{n}, then computes M_{π} from π in time polynomial wrt |π|, then decides whether M_{π} ⊧ T_{n} ∗P_{n} by checking whether M_{π} ⊧ T′_{n}. If ∗ is logically-compactable the last decision can be made in time less than or equal to p_{1}(|T_{n}| + |P_{n}|) + |M_{π}|. Therefore, the advice-taking Turing machine would globally work in time polynomial in |π|. Since 3-sat is an NP-complete problem, this would imply NP ⊆ P/poly.

Compactability wrt query equivalence is a property of belief revision operators weaker than logical compactability.

Definition 2.6 (query-compactable operator) An update or revision operator ∗ is query-compactable if and only if there exists a polynomial p such that for any pair of propositional formulae T and P there exists a propositional formula T′ with the following properties:

1. |T′| ≤ p(|T | + |P |);

2. T′ is query equivalent (cf. (1)) to T ∗ P.

Similarly to logical-compactability, in order to prove that some belief revision operator are not query-compactable we show that this would imply some very unlikely consequences on complexity classes. We show a general property analogous to Theorem 2.2 that will be helpful in the proofs of the next sections.

Theorem 2.3 Let ∗ be a revision operator. Assume there exists a polynomial p such that, for each n > 0, there exists a pair of formulae T_{n}, P_{n} with the following properties:

1. |T_{n}| + |P_{n}| ≤ p(n);

2. for all π ∈ 3-sat_{n}, there exists a formula Q_{π} such that:

(a) Q_{π} can be computed from π in polynomial time;

(b) T_{n} ∗ P_{n} ⊧ Q_{π} iff π is satisfiable.

With the above hypothesis, if ∗ is query-compactable, then NP ⊆ coNP/poly.

Proof. Assume there exists a polynomial p such that, for each n, there exists a pair of formulae T_{n}, P_{n} with the properties stated. Now, assume ∗ is query-compactable. Hence, for each pair T_{n}, P_{n} there exists a T′_{n} with properties stated in Definition 2.6. Recall that the problem of deciding whether T′_{n} ⊧ Q_{π} (the input being T′_{n}, Q_{π}) is in coNP. Then we can define an advice-taking non-deterministic Turing machine in the following way.

First, we define the advice oracle as A(n) = T′_{n}. Observe that |A(n)| = |T′_{n}| ≤ p_{1}(|T_{n}| + |P_{n}|) ≤ p_{1}(p(n)), where p is the polynomial mentioned in the hypothesis 1 of the theorem, and p_{1} is the polynomial mentioned in point 1 of Definition 2.6. Hence, the size of the advice is bounded by a polynomial which is the composition of p_{1} and p.

Secondly, the machine operates as follows: given an instance π of 3-sat, with |π| = n, the machine loads A(|π|) = A(n) = T′_{n}, then computes Q_{π} from π in time polynomial wrt |π|, then decides whether T_{n} ∗ P_{n} ⊧ Q_{π} by checking whether T′_{n} ⊧ Q_{π}. If ∗ is query-compactable the last problem is in coNP (the input being T′_{n} and Q_{π}). Therefore, the problem “is π unsatisfiable?” can be solved by an advice-taking nondeterministic polynomial-time machine whose input has size polynomial in |π|. Since 3-sat is an NP-complete problem, and co(NP/poly) = coNP/poly, this would imply NP ⊆ coNP/poly.

Theorems 2.2 and 2.3 provide a general schema for the proofs of non-existence of compact representations that we present in the paper. All our proofs use the same technique, even though with major differences in the details.

3 Single unbounded revision

The purpose of this section is to show an analysis of logical- and query-compactability of revision operators. We consider revision operators mentioned in Section 2, and show both compactability and non-compactability results. There is no assumption on the size of the formula P; the bounded-size case will be addressed in the next section. Moreover, we consider only a single revision. Notice that WIDTIO semantics is logically compactable (hence query compactable) since it immediately follows from its definition that the size of T ∗_{W id} P is always less than or equal to |T | + |P |.

3.1 Query compactability

In this subsection we investigate query compactability, and begin our investigation focusing on Ginsberg-Fagin-Ullman-Vardi’s operator. Other researchers have already noticed that the explicit representation of the result of revising a knowledge base under Ginsberg-Fagin-Ullman-Vardi’s semantics might have exponential size.

We introduce this problem with an example presented by Nebel in [Neb94]. Let

T = {x_{1}, …, x_{m}, y_{1}, …, y_{m}}

P = ⋀_{i=1}^{m}(x_{i} ≢ y_{i})

Applying Ginsberg-Fagin-Ullman-Vardi’s revision method we have that W (T, P) contains 2^{m} distinct theories, each one containing, for each i(1 ≤ i ≤ m), exactly one of x_{i} and y_{i}. If we represent T ∗_{GF UV} P as the disjunction of all theories in W (T, P), conjoined with P, the size of this representation is exponential in |T | + |P |.

The problem of the explosion of the size of the revised knowledge base was also pointed out by Winslett in [Win90], where she shows another example:

T = { x_{1}, y_{1},  z_{1} ≡ (¬x_{1} ∨ ¬y_{1}),
⋮  ⋮  ⋮
x_{i}, y_{i},  z_{i} ≡ (z_{i−1} ∧ (¬x_{i} ∨ ¬y_{i})),
⋮  ⋮  ⋮
x_{m}, y_{m}, z_{m} ≡ (z_{m−1} ∧ (¬x_{m} ∨ ¬y_{m})) }
P = z_{m}

Again, the cardinality of the set W (T, P) is exponential in m (note that in this example the size of P does not depend on m). These two examples show that the “obvious” representation of T ∗_{GF UV} P might have size exponential in |T |+|P |. However, they do not rule out the existence of a different representation of polynomial size. As Winslett notes in [Win90, pg. 34] the exponential increase in the size is proven if we “assume a completely naive storage organization, where the theories are written out as we would write them down on paper”. Later on she also conjectures that “these bounds hold even for clever storage schemes”.

We now show that her conjecture on Ginsberg-Fagin-Ullman-Vardi’s revision is indeed true for the more general case of query equivalence. This result is later generalized to other revision operators mentioned in Section 2.2. We recall that the symbol B_{n} denotes the set of letters {b_{1}, …, b_{n}} used to build all formulae in 3-sat_{n}.

Theorem 3.1 Unless NP ⊆ coNP/poly, the revision operator ∗_{GF UV} is not querycompactable.

Proof. We apply the general schema of Theorem 2.3 and the notation of Definition 2.5, so we show that for any integer n, there exists a formula P_{n} and a set of atomic facts T_{n}, both depending only on n, of polynomial size wrt n, such that given any π ∈ 3-sat_{n}, there exists a query Q_{π} such that π is satisfiable if and only if T_{n} ∗_{GF UV} P_{n} ⊧ Q_{π}.

Let L be the alphabet B_{n} ∪ C ∪ D ∪ {r}, where C is a set of new atoms one-to-one with elements of π_{n}^{max}, i.e. C = {c_{i} | γ_{i} ∈ π_{n}^{max}}, D is a set of new atoms one-to-one with atoms in C and r is a new distinct atom.

We define T_{n} and P_{n} on the alphabet L according to the following rules:

T_{n} = ⋀(C ∪ D ∪ B_{n} ∪ {r})  (3)
P_{n} = [( ⋀_{i=1}^{n}{¬b_{i} | b_{i} ∈ B_{n}} ∧ ¬r) ∨ ⋀(c_{j} → γ_{j})] ∧ ⋀(c_{j} ≢ d_{j})  (4)

We define Q_{π} as follows:

Q_{π} = ⋀({c_{i} | γ_{i} ∈ π} ∪ {d_{i} | γ_{i} ∉ π}) → r  (5)

Given an interpretation η of the atoms of C, we can associate a theory W_{η} to it:

W_{η} = {c_{i} | c_{i} ∈ η} ∪ {d_{i} | c_{i} ∉ η}

Note that no c_{i} or d_{i} can be added consistently to W_{η} ∪ P_{n}, because P_{n} imposes that c_{i} ≢ d_{i}. Furthermore, the theory W_{η} ∪ P_{n} is consistent, because the interpretation η′, that extends η to L by making true all atoms d_{i} such that c_{i} ∉ η and false all the other atoms in L satisfies both W_{η} and P_{n}.

In order to find a world W_{1} of T_{n} ∗_{GF UV} P_{n} which does not satisfy Q_{π}, we must focus on the worlds satisfying ⋀({c_{i} | γ_{i} ∈ π} ∪ {d_{i} | γ_{i} ∉ π}). Hence, all worlds not satisfying Q_{π} must include W_{η}. Thus, W_{1} |̸= Q_{π} only if W_{η} ⊆ W_{1}.

Suppose π unsatisfiable. We show that W_{η} ∈ W (T_{n}, P_{n}) and W_{η} ∪ P_{n} |̸= Q_{π}. For each interpretation ϕ of the atoms of B_{n}, there exists a γ_{i} ∈ π such that ϕ |̸= γ_{i}. Let ψ = η ∪ ϕ be an interpretation on L: we have that ψ |̸= ⋀(c_{i} → γ_{i}). As a consequence, W_{η} ∪P_{n} ⊧ (⋀{¬b_{i} | b_{i} ∈ B_{n}})∧¬r ∧ ⋀(c_{i} ≢ d_{i}). Adding to W_{η} any other element of T_{n} would make W_{η} inconsistent with P_{n}, therefore, W_{η} ∈ W (T_{n}, P_{n}). Since W_{η} ∪P_{n} |̸= Q_{π}, then T_{n} ∗_{GF UV} P_{n} |̸= Q_{π}.

On the converse, suppose π satisfiable. We show that all theories in W (T_{n}, P_{n}) imply Q_{π}. Note that all theories not including W_{η} imply Q_{π}, hence we concentrate on those containing W_{η}. Since T is a conjunction of literals, these theories are uniquely characterized by their intersection with B_{n} ∪{r}. For any interpretation ϕ of the atoms in B_{n}, let W_{ϕ} be defined as follows:

W_{ϕ} = W_{η} ∪ {x_{i} | x_{i} ∈ ϕ} ∪ {r}

If ϕ does not satisfy π then W_{ϕ} is inconsistent with P_{n}, and therefore, W_{ϕ} ∉ W (T_{n}, P_{n}). On the other hand, if ϕ satisfies π, the interpretation ψ = η ∪ ϕ ∪ {r} of L satisfies W_{ϕ}, P_{n} and Q_{π}. Since there exists at least one interpretation ϕ satisfying π, the corresponding W_{ϕ} ∈ W (T_{n}, P_{n}), and therefore W_{η} ∉ W (T_{n}, P_{n}). As a consequence, for all elements W_{ϕ} of W (T_{n}, P_{n}) we have that W_{ϕ} ∪ P_{n} ⊧ Q_{π}.

We now consider the model-based revision operators. Even though their semantics is very different from Ginsberg-Fagin-Ullman-Vardi’s one, we obtain a similar result for most of them:

Theorem 3.2 Unless NP ⊆ coNP/poly, the revision operators ∗_{B}, ∗_{S} and ∗_{W in} are not query-compactable.

Proof. Eiter and Gottlob’s result [EG92, Lemma 6.1] implies that T ∗_{GF UV} P ⊧ Q iff T ∗_{B} P ⊧ Q iff T ∗_{S} P ⊧ Q iff T ∗_{W in} P ⊧ Q when T is a set of literals and V (Q) ⊆ V (T). Note that these conditions hold for the T_{n} defined in (3) and Q_{π} defined in (5).

Using a proof similar to the one of Theorem 3.1, we can show that the same result also holds for Forbus’ revision operator.

Theorem 3.3 Unless NP ⊆ coNP/poly, the revision operator ∗_{F} is not query-compactable.

Proof. The proof is similar to the one of Theorem 3.1, but we have now to consider closeness between models. We adopt the notation of Definition 2.5. Given an n, let C be an m × (n + 2) boolean matrix, where m is the number of clauses in π_{n}^{max}. Let

U_{n} = ⋀_{j=1}^{m} ⋀_{i=2}^{n+2}(c_{i}^{j} ≡ c_{1}^{j})

This formula forces all rows of the matrix C to be equal. Let T_{n} and P_{n} be defined as follows:

T_{n} = {U_{n}} ∪ B_{n} ∪ {r}
P_{n} = U_{n} ∧ [ ⋀_{j=1}^{m}(c_{1}^{j} → γ_{j}) ∨ (∧{¬b_{i} | b_{i} ∈ B_{n}} ∧ ¬r)]

Given π ∈ 3-sat_{n}, we define:

Q_{π} = ⋁_{i=1}^{n+2}{c_{i}^{j} | γ_{j} ∉ π} ∨ ⋁_{i=1}^{n+2}{¬c_{i}^{j} | γ_{j} ∈ π} ∨ ⋁ B_{n} ∨ r

We show that T_{n} ∗_{F} P_{n} ⊧ Q_{π} if and only if π is satisfiable. Note that every interpretation, but M_{π} = ⋃_{i=1}^{n+2}{c_{i}^{j} | γ_{j} ∈ π}, satisfies Q_{π}. Thus, we only need to show that M_{π} ⊧ T_{n} ∗_{F} P_{n} if and only if π is unsatisfiable.

First of all, note that T_{n} has a model for each π ⊆ π_{n}^{max}. We denote I_{π} = ⋃_{i=1}^{n+2}{c_{i}^{j} | γ_{j} ∈ π} ∪ B_{n} ∪ {r} that model.

Observe that the distance between M_{π} and I_{π} is exactly n + 1, while the distance from I_{π} of any other N ∈ M(P_{n}), with a different valuation of atoms in C, is at least n + 2. Hence, the models of P that are closest to I_{π} must have the same valuation of atoms in C.

Suppose π unsatisfiable. The closest model of I_{π} is now M_{π}, since there is no other model of P_{n} with the same valuation of C. Hence M_{π} ⊧ T_{n} ∗_{F} P_{n}.

On the converse, suppose π satisfiable. Let ϕ be the interpretation of the atoms in B_{n} satisfying π. The model N_{π} = ⋃_{i=1}^{n+2}{c_{i}^{j} | γ_{j} ∈ π} ∪ {x_{i} | x_{i} ∈ ϕ} ∪ {r} is now in M(P_{n}), and its distance from I_{π} is at most n letters. Hence, M_{π} is not a model of T_{n} ∗_{F} P_{n}.

We now turn our attention to operators that are query-compactable. In particular, we focus on Dalal’s and Weber’s operators.

Let V (T) = {x_{1}, …, x_{n}} be the alphabet of the initial knowledge base T, and Y = {y_{1}, …, y_{n}} be another set of (distinct) letters, one-to-one with V (T). Let EXA(k, V (T), Y, W) denote a formula containing letters of V (T) and Y, and possibly other letters W, which is true iff the Hamming distance between the values assigned to V (T) and Y is exactly k. The revised theory T ∗_{D} P can be expressed as T [V (T)/Y] ∧ P ∧ EXA(k, V (T), Y, W), where k is the minimum distance between the models of P and T, denoted as k_{T,P} in the definition of Dalal’s revision.

Formula EXA(k, V (T), Y, W) can be constructed in several ways. For example, first compute the number of true exclusive-or’s between each x_{i} and y_{i}. The binary representation of this number can be computed with a suitable adding circuit, that requires O(n^{2}) half adders. This circuit can be expressed as a formula using O(n^{2}) new

y HA x ∧ y x x ≢ y

Figure 2: Half adder.

w^{15}  w^{13}  w^{11}  w_{3} w_{4} w_{8} w_{6} w_{12} w_{10} w_{14} w_{9}  w_{5} w_{7}  w_{2} w_{1} HA1 HA2 HA4 HA3 HA5 HA6

Figure 3: Adding circuit for EXA(k, {x_{1}, x_{2}, x_{3}, x_{4}}, {y_{1}, y_{2}, y_{3}, y_{4}}, {w_{1}, …, w_{15}}) . letters. Secondly, write the formula that equals the bits of this number with those of the binary representation of k.

The circuit for a single half adder is reported in Figure 2. The half adder is used as a building block in Figure 3 for constructing a circuit for EXA(k, {x_{1}, x_{2}, x_{3}, x_{4}}, {y_{1}, y_{2}, y_{3}, y_{4}}, W) (i.e. n = 4). As it is evident from the figure, the set W is {w_{1}, …, w_{15}}, i.e. the set of fifteen new variables that are used. Such variables are characterized by the conjunction of the following formulae:

w_{1} ≡ (x_{1} ≢ y_{1})
w_{2} ≡ (x_{2} ≢ y_{2})
w_{3} ≡ (x_{3} ≢ y_{3})
w_{4} ≡ (x_{4} ≢ y_{4})
w_{5} ≡ (w_{1} ≢ w_{2})
w_{6} ≡ (w_{1} ∧ w_{2})
w_{7} ≡ (w_{5} ≢ w_{3})
w_{8} ≡ (w_{5} ∧ w_{3})
w_{9} ≡ (w_{6} ≢ w_{8})
w_{10} ≡ (w_{6} ∧ w_{8})
w_{11} ≡ (w_{4} ≢ w_{7})
w_{12} ≡ (w_{4} ∧ w_{7})
w_{13} ≡ (w_{12} ≢ w_{9})
w_{14} ≡ (w_{12} ∧ w_{9})
w_{15} ≡ (w_{14} ≢ w_{10})

Now, if k is 3, it is necessary to make sure that the output of the adding circuit (i.e. bits w_{15}, w_{13}, w_{11} – w_{15} being the most significant bit) equals the binary representation of k (i.e. 011). This can be done adding the conjunction of the following formula:

w_{11} ∧ w_{13} ∧ ¬w_{15}

Theorem 3.4 Let k be the minimum distance between models of T and models of P, i.e. k = k_{T,P}. Then T [V (T)/Y] ∧ P ∧ EXA(k, V (T), Y, W) is query equivalent (1) to T ∗_{D} P.

Proof. Let Q be a query on the alphabet V (T) ∪ V (P) and k be the minimal distance between the models of P and T. We prove the theorem by showing that T [V (T)/Y] ∧ P ∧ EXA(k, V (T), Y, W) ⊧ Q iff T ∗_{D} P ⊧ Q.

If. We show that T [V (T)/Y] ∧ P ∧ EXA(k, V (T), Y, W) |̸= Q implies T ∗_{D} P |̸= Q. Let M be a model of T [V (T)/Y] ∧ P ∧ EXA(k, V (T), Y, W) such that M |̸= Q. Thus, M ∩ V (T) satisfies P, and, since M satisfies EXA(k, V (T), Y, W), M ∩ V (T) has a distance k from M ∩ Y, and M ∩ Y satisfies T [V (T)/Y]. Since k is by definition the minimal distance between a model of T and a model of P, M ∩ V (T) is also a model of T ∗_{D} P. Therefore, T ∗_{D} P |̸= Q.

Only If. We show that T ∗_{D}P |̸= Q implies T [V (T)/Y]∧P ∧EXA(k, V (T), Y, W) |̸= Q. Let M be a model of T ∗_{D} P such that M |̸= Q. This model satisfies P. Let MT be a model of T having distance k from M. Define M′ as M ∪ {y_{i}|x_{i} ∈ MT }. Obviously, M′ satisfies both P and T [V (T)/Y], and by definition of MT it can be extended to an assignment to W so that it also satisfies EXA(k, V (T), Y, W). Therefore, T [V (T)/Y]∧ P ∧ EXA(k, V (T), Y, W) |̸= Q.

Now we show how Weber’s revision can be compactly represented. Winslett, in [Win90] gives a similar proof, but only if the new formula has a size bounded by a constant. Our result, instead, does not need such a restriction. Let Ω = {ω_{1}, …, ω_{k}} be the set of letters in the definition of Weber’s revision operator, and Z = {z_{1}, …, z_{k}} be a new set of letters one-to-one with Ω.

Theorem 3.5 T [Ω/Z] ∧ P is query equivalent (1) to T ∗_{W eb} P.

Proof. Let Q be a formula on the alphabet V (T)∪V (P). We show that T ∗_{W eb} P ⊧ Q iff T [Ω/Z] ∧ P ⊧ Q.

If. Assume that T ∗_{W eb} P ⊧ Q and T [Ω/Z] ∧ P |̸= Q. As a consequence, for all models N of T ∗_{W eb} P we have that N ⊧ Q and there exists a model M of T [Ω/Z] ∧ P (on the alphabet V (T) ∪ V (P) ∪ Z) such that M |̸= Q. Since M ⊧ T [Ω/Z], we construct a model M′ on the alphabet V (T) ∪ V (P) as follows: for all letters l of (V (T) ∪ V (P)) − Ω, we have that l ∈ M′ iff l ∈ M. For all letters ω_{i} of Ω, ω_{i} ∈ M′ iff z_{i} ∈ M. Obviously, M′ |̸= Q, and, by construction, M′ ⊧ T. Since M ⊧ P, M′ ⊧ T and MΔM′ ⊆ Ω, it follows that M is a model of T ∗_{W eb} P that does not satisfy Q, hence contradiction arises.

Only If. Assume that T ∗_{W eb} P |̸= Q and T [Ω/Z] ∧ P ⊧ Q. As a consequence, for all models M of T [Ω/Z] ∧ P we have that M ⊧ Q and there exists a model N of T ∗_{W eb} P such that N |̸= Q. Since N ⊧ T ∗_{W eb} P, we construct a model N′ on the alphabet V (T) ∪ V (P) ∪ Z as follows: for all letters l of (V (T) ∪ V (P)), we have that l ∈ N′ iff l ∈ N. For all letters z_{i} ∈ Z, z_{i} ∈ N′ iff ω_{i} ∈ Ω. Obviously, N′ |̸= Q, N′ ⊧ P, and, by construction, N′ ⊧ T [Ω/Z]. Therefore, there exists a model of T [Ω/Z] ∧ P that does not satisfy Q, thus contradicting the hypothesis.

We note that this representation of T ∗_{W eb} P increases the size of T only by the length of P whereas the less “compact” representation of T ∗_{D} P requires a formula whose size is quadratic in the number of the letters.

3.2 Logical compactability

In this section we investigate logical compactability. In particular, we show that Dalal’s and Weber’s operators, which are query-compactable, are probably not logically-compact-able.

Theorem 3.6 Unless NP ⊆ P/poly, the revision operators ∗_{D} and ∗_{W eb} are not logicallycompactable.

Proof. We apply the general schema of Theorem 2.2 and the notation of Definition 2.5, so we show that for any integer n, there exists a formula P_{n} and a knowledge base T_{n}, both depending only on n, of polynomial size wrt n, such that given a π ∈ 3-sat_{n}, there exists an interpretation M_{π} such that π is satisfiable iff M_{π} is a model of T_{n} ∗_{D} P_{n} iff M_{π} is a model of T_{n} ∗_{W eb} P_{n}.

Let Y = {y_{1}, …, y_{n}} be a set of new letters in one-to-one correspondence with letters of B_{n}, and let C be a set of new letters one for each three-literals clause over B_{n}, i.e. C = {c_{i} | γ_{i} ∈ π_{n}^{max}}. Finally, let L be the set B_{n} ∪ Y ∪ C. Notice that card(L) ∈ O(n^{3}). We define T_{n} as the conjunction of two formulae:

T_{n} = Φ_{n} ∧ Γ_{n}

The 2CNF formula Φ_{n} states non-equivalence between atoms in B_{n} and their correspondent in Y:

Φ_{n} = ⋀_{b_{i}∈B_{n}}(b_{i} ≢ y_{i}).

Γ_{n} codes every possible set of clauses in π_{n}^{max}, using the atoms in C as “enabling gates”. The formula is defined as:

Γ_{n} = ⋀_{c_{i}∈C} γ_{i} ∨ ¬c_{i}.

Γ_{n} is a 4CNF formula and it contains O(n^{3}) clauses.

We define P_{n} as:

P_{n} = ⋀_{i=1}^{n}(¬b_{i} ∧ ¬y_{i})

Note that the size of T_{n} and P_{n} is O(n^{3}). Moreover, T_{n} and P_{n} depend only on the size n.

We define C_{π} = {c_{i} ∈ C | γ_{i} is a clause of π}. We first show that π is satisfiable implies that C_{π} is a model of T_{n} ∗_{D} P_{n}, then we show that π is unsatisfiable implies that C_{π} is not a model of T_{n} ∗_{W eb} P_{n}. Combining these results with the fact that all models of Dalal’s revision are also models of Weber’s revision (cf. Figure 1), we obtain that π is satisfiable iff C_{π} is a model of T_{n} ∗_{D} P_{n} iff C_{π} is a model of T_{n} ∗_{W eb} P_{n}.

We observe that in every model of T_{n} exactly n atoms from B_{n}∪Y are true, while in every model of T_{n} ∗_{D} P_{n} all atoms from B_{n} ∪Y are false. Hence, recalling the definition of Dalal’s revision, k_{T_{n},P_{n}} ≥ n. Moreover, k_{T_{n},P_{n}} = n since B_{n} is a model of T_{n} and ∅ is a model of P_{n}, and the cardinality of their difference is n. Now C_{π} is a model of P_{n}, hence it is also a model of T_{n} ∗_{D} P_{n} iff there exists a model of T_{n} such that card(C_{π}ΔM) = k_{T_{n},P_{n}} = n.

Assume π is satisfiable. Let B_{π} be a model of π, \overline{Y_{π}} = \{y_{i} | b_{i} ∉ B_{π}\} and M = C_{π} ∪B_{π} ∪\overline{Y_{π}}. We show that M is a model of T_{n}. In fact, M satisfies Φ_{n} by construction of \overline{Y_{π}}, and also M satisfies Γ_{n}, because for each clause γ_{i} ∨ ¬c_{i} of Γ_{n}, either c_{i} ∉ C_{π} or γ_{i} is satisfied by B_{π}. Now observe that card(C_{π}ΔM) = card(B_{π} ∪ \overline{Y_{π}}) = n. Hence, C_{π} is a model of T_{n} ∗_{D} P_{n}. Since the models of Dalal’s revision are also models of Weber’s revision, we also have that C_{π} is a model of T_{n} ∗_{W eb} P_{n}.

Now, observe that M(P_{n}) = 2^{C}, i.e. every subset of C is a model of P_{n}. Since B_{n} and Y are models of T_{n}, μ(B_{n}, P_{n}) = B_{n}, μ(Y, P_{n}) = Y. This implies that both B_{n} and Y are in δ(T_{n}, P_{n}) ≐ ⋃_{M∈M(T_{n})} μ(M, P_{n}). Recall that Ω ≐ ∪δ(T, P). Hence, B_{n} ∪ Y ⊆ Ω. Moreover, since V (P_{n}) ∩ C = ∅, by Proposition 2.1 Ω = B_{n} ∪ Y. From the definition of Weber’s revision, C_{π} is a model of T_{n} ∗_{W eb} P_{n} iff there exists a model M of T_{n} such that M − Ω = C_{π} − Ω. Since Ω = B_{n} ∪ Y, the last condition is equivalent to M ∩ C = C_{π}.

Assume π is unsatisfiable and C_{π} is a model of T_{n} ∗_{W eb} P_{n}. Then there exists a model M of T_{n} such that M ∩ C = C_{π}. We claim that M ∩ B_{n} is a model of π. In fact, as for Dalal’s revision, M satisfies Γ_{n} = ⋀_{c_{i}∈C} γ_{i} ∨ ¬c_{i}. Simplifying Γ_{n} with truth values of M ∩ C = C_{π}, we conclude that M satisfies ⋀_{c_{i}∈C_{π}} γ_{i}, which is exactly formula π. Since the formula contains only atoms from B_{n}, M ∩ B_{n} satisfies π, hence π is satisfiable and contradiction arises. Thus, C_{π} is not a model of T_{n} ∗_{W eb} P_{n}. Since the set of models of T_{n} ∗_{W eb} P_{n} is a superset of the models of T_{n} ∗_{D} P_{n}, it follows that C_{π} is not a model of T_{n} ∗_{D} P_{n}.

We conclude the section by generalizing the negative results about query compactability to logical compactability.

Theorem 3.7 Unless NP ⊆ coNP/poly, the revision operators ∗_{B}, ∗_{F} , ∗_{GF UV} , ∗_{N}, ∗_{S}, and ∗_{W in} are not logically-compactable.

Proof. The claim follows from Theorems 3.1, 3.2 and the fact that the non-existence of a representation satisfying criterion (1) implies the non-existence of a representation satisfying criterion (2).

4 Single bounded revision

In the previous section we investigated the issue of the existence of compact representations of revised knowledge bases. As it turned out, for most of the operators a compact explicit representation of the result of revising a knowledge base with a new formula does not exist. From an analysis of the proofs, it turns out that this behavior depends on the new formula P being very complex. However, in database applications it is reasonable to assume that the size of the new formula is very small wrt the size of the knowledge base. In this section we investigate which impact this assumption has on the existence of compact representations. In particular, throughout this section we assume that the size of the new formula P is bounded by a constant (k in the sequel).

We first show that Ginsberg-Fagin-Ullman-Vardi’s revision remains non compactable even under the above assumption.

Theorem 4.1 Unless NP ⊆ coNP/poly, the revision operator ∗_{GF UV} is not query compactable, even if |P | ≤ k.

Proof. Let s be a new propositional variable. We define T′_{n}, P′_{n} from T_{n}, P_{n} in (3) and (4) by T′_{n} = {f ∧ (¬s ∨ P_{n})|f ∈ T_{n}} ∪ {¬s}, P′_{n} = s. It immediately follows that, for all formulae Q on the alphabet V (T_{n}) ∪ V (P_{n}), we have that T′_{n} ∗_{GF UV} P′_{n} ⊧ Q iff T_{n} ∗_{GF UV} P_{n} ⊧ Q. Assume that ∗_{GF UV} is query compactable when |P | ≤ k. By the above reduction we have that ∗_{GF UV} is query compactable even when there is no bound on the size of P. By Theorem 3.1 it follows that NP ⊆ coNP/poly.

The situation for model-based revision operators is more complex. As it turns out all of them admit a compact representation, wrt both query and logical equivalence, when the size of P is bounded.

Without loss of generality, since the size of P is bounded we assume that the alphabet V (P) of P is included in the alphabet V (T) of T (e.g. we can add to T the formula ⋀_{p∈V (P)}(p ∨ ¬p)). Because of the assumption of |P | being bounded by k, it follows that card(V (P)) ≤ k. Without loss of generality, we assume card(V (P)) = k, and denote letters in V (P) as {v_{1}, …, v_{k}}.

We use the following notation: for every set of letters H, we denote with Ĥ the set {¬x|x ∈ H}. The formula F [H/Ĥ], where H ⊆ V (F), is F with each letter in H replaced by the corresponding letter in Ĥ (that is, its negation).

A useful property that we shall use in the sequel is the following:

Proposition 4.2 For each interpretation M of the letters in V (F) and set H ⊆ V (F), M ⊧ F if and only if MΔH ⊧ F [H/Ĥ].

In other words, if an interpretation M satisfies a formula F then, for any given set of letters H, the model MΔH, that agrees with M on all letters in V (F)−H and disagrees on all letters in H, satisfies the formula F [H/Ĥ], where all letters in H are replaced by their negation. For example, let F = x_{1} ∧ (x_{2} ∨ ¬x_{3}), M = {x_{1}} and H = {x_{2}, x_{3}}. Note that M ⊧ F. Applying the definitions, we obtain that MΔH = {x_{1}, x_{2}, x_{3}} and F [H/Ĥ] = x_{1} ∧ (¬x_{2} ∨ ¬¬x_{3}). It follows that {x_{1}, x_{2}, x_{3}} ⊧ x_{1} ∧ (¬x_{2} ∨ ¬¬x_{3}).

4.1 Compactability of “pointwise” operators

We exhibit a compact representation of T ∗_{W in} P which uses exactly the same alphabet of T and P. Basically, we exploit the fact that we can explicitly represent all assignments to V (P) in constant space, since card(V (P)) = k.

Let S be an arbitrary set of letters such that S ⊆ V (P). The formula

P ∧ ⋁_{S⊆V (P)} (T [S/Ŝ] ∧ R)

where ⋁_{S⊆V (P)} means a disjunction for all possible subsets S of V (P), is satisfied by a model N of P iff there is a model M of T (whose distance from N is given by the set S), satisfying formula R.

S represents the distance between N and M. Formula R specifies that there is no other model in P whose distance from M is less than S.

R = ¬ ⋁_{C⊆V (P) , CΔS⊂S} P [C/Ĉ]

where ⋁_{C⊆V (P) , CΔS⊂S} means a disjunction for all possible subsets C of V (P), satisfying condition CΔS ⊂ S (an equivalent condition is C ≠ ∅, C ⊆ S). This formula imposes a condition over the distance C between two models of P. Namely, it forbids that C is between M and N.

The whole formula is

P ∧ ⋁_{S⊆V (P)} (T [S/Ŝ] ∧ ¬ ⋁_{C⊆V (P) , CΔS⊂S} P [C/Ĉ])  (6)

Theorem 4.3 Formula (6) has size linear in |T | and is logically equivalent to T ∗_{W in}P.

Proof. The formula uses only letters of V (T), and has size linear in |T |, but exponential in |P | (i.e. O(|T | · 2^{|P |} + 2^{2|P |})). As for the logical equivalence, we split the proof in two parts.

(1st part) Let N be a model of T ∗_{W in} P, i.e. N ∈ M(P) and ∃M ∈ M(T) : MΔN ∈ μ(M, P). We prove that N is also a model of formula (6). Let S be MΔN; the following propositions are equivalent:

1. M ⊧ T

2. (MΔS) ⊧ T [S/Ŝ]

3. N ⊧ T [S/Ŝ]

(1 equivalent to 2 by Proposition 4.2; 2 equivalent to 3 by associativity of Δ). We prove now that S ⊆ V (P), by assuming that there is a letter l such that l ∈ S, l ∉ V (P), and showing that a contradiction arises. Since S is MΔN, there are only two possibilities:

1. l ∈ N, l ∉ M. Define N′ as N \ {l}. Since l ∉ V (P), N′ ⊧ P. Since l ∉ M, N′ΔM ⊂ S, contradicting the hypothesis that S belongs to μ(M, P).

2. l ∉ N, l ∈ M. Define N′ as N ∪ {l}. Since l ∉ V (P), N′ ⊧ P. Since l ∈ M, N′ΔM ⊂ S, contradicting the hypothesis that S belongs to μ(M, P).

We now prove that N is a model of the remaining part of formula (6), i.e. that N ⊧ ¬ ⋁_{C⊆V (P) , CΔS⊂S} P [C/Ĉ]. We do so by assuming that there is a set C such that C ⊆ V (P), CΔS ⊂ S and N |̸= ¬P [C/Ĉ], and showing that a contradiction arises. N |̸= ¬P [C/Ĉ] is equivalent to N ⊧ P [C/Ĉ], which, by Proposition 4.2, is equivalent to (NΔC) ⊧ P. Now, MΔ(NΔC) = (MΔN)ΔC = SΔC. The last set is, by assumption, strictly contained in S. This leads to a contradiction: remind that by assumption N is a model of T ∗_{W in} P; this means that MΔN ∈ μ(M, P), i.e. S ∈ μ(M, P); but we found a model (NΔC) of P such that MΔ(NΔC) ⊂ S, hence S cannot belong to μ(M, P).

(2nd part) Let N be a model of formula (6). We prove that N is also a model of T ∗_{W in} P, i.e. N ∈ M(P) and ∃M ∈ M(T) : MΔN ∈ μ(M, P).

First of all, N ⊧ P. Secondly, we know there is a set S ⊆ V (P) such that N ⊧ T [S/Ŝ] ∧ ¬ ⋁_{C⊆V (P) , CΔS⊂S} P [C/Ĉ]. By Proposition 4.2, this is equivalent to (NΔS) ⊧ T ∧ ¬(⋁_{C⊆V (P) , CΔS⊂S} P [C/Ĉ])[S/Ŝ]. Define M as NΔS (which implies S = MΔN). We have to prove that S ∈ μ(M, P). We assume that this is not true, and prove that a contradiction follows. If S ∉ μ(M, P), it follows that there must be a model Q of P which is closer to M than N, i.e. MΔQ ∈ μ(M, P) (this implies MΔQ ⊂ S). Define C as NΔQ, i.e. Q = NΔC. The following conditions are equivalent:

1. Q ⊧ P

2. NΔC ⊧ P

3. N ⊧ P [C/Ĉ]

Next step is to note the following chain of equalities: CΔS = NΔQΔS = NΔQΔMΔN = QΔM. Using the fact that MΔQ ⊂ S, we have that CΔS ⊂ S. This implies C ⊂ S, which in turn implies C ⊂ V (P). Contradiction follows by noticing that we found a set C such that C ⊆ V (P), CΔS ⊂ S and N ⊧ P [C/Ĉ].

Using Theorem 4.3 and the fact that T ∗_{B} P is T ∧ P if consistent and T ∗_{W in} P otherwise, we obtain:

Corollary 4.4 There exists a formula of size linear in |T | that is logically equivalent to T ∗_{B} P.

We now exhibit a compact representation of T ∗_{F} P which uses exactly the same alphabet of T and P. The main difference between Forbus’ operator and Winslett’s one relies on the fact that the notion of distance between models for the former one is based on set cardinality, while for the latter one on set containment. As a consequence, we obtain a formula very similar to the one obtained for Winslett’s operator. In fact, the formula representing T ∗_{F} P is the following:

P ∧ ⋁_{S⊆V (P)} (T [S/Ŝ] ∧ ¬ ⋁_{C⊆V (P) , |CΔS|<|S|} P [C/Ĉ])  (7)

(cf. formula (6) and note that here cardinality of sets is considered in the subscript of the last disjunction).

Theorem 4.5 Formula (7) has size linear in |T | and is logically equivalent to T ∗_{F} P.

Proof. The formula uses only letters of V (T), and has size linear in |T |, but exponential in |P | (i.e. O(2^{2|P |})). As for the other statement, we split the proof in two parts.

(1st part) Let N be a model of T ∗_{F} P, i.e. N ∈ M(P) and ∃M ∈ M(T) : |MΔN| = k_{M,P}. We have to prove that N is also a model of formula (7).

The proof is omitted, as it can be obtained using a schema similar to the one used for the corresponding part of Theorem 4.3 (the only differences being the usage of set cardinality, of ≤ instead of ⊆, and k_{M,P} instead of μ(M, P)).

(2nd part) Let N be a model of formula (7). We prove that N is also a model of T ∗_{F} P, i.e. N ∈ M(P) and ∃M ∈ M(T) : |MΔN| = k_{M,P}.

First of all, N ⊧ P. Then we know there is a set S ⊆ V (P) such that N ⊧ T [S/Ŝ]∧ ¬ ⋁_{C⊆V (P) , |CΔS|<|S|} P [C/Ĉ]. By Proposition 4.2, this is equivalent to (NΔS) ⊧ T ∧ ¬(⋁_{C⊆V (P) , |CΔS|<|S|} P [C/Ĉ])[S/Ŝ]. Define M as NΔS (which implies S = MΔN). We have to prove that |S| = k_{M,P}. We assume that this is not true, and prove that a contradiction follows. If |S| > k_{M,P}, it follows that there must be a model Q of P which is closer to M than N, i.e. |MΔQ| = k_{M,P} < |S|. Define C as NΔQ, i.e. Q = NΔC. The following conditions are equivalent:

1. Q ⊧ P

2. NΔC ⊧ P

3. N ⊧ P [C/Ĉ]

Next step is to note the following chain of equalities: CΔS = NΔQΔS = NΔQΔMΔN = QΔM. Using the fact that |MΔQ| < |S|, we have that |CΔS| < |S|.

The last step that is still missing is to prove that C ⊆ V (P) (note: this step is not necessary in the proof of Theorem 4.3). We assume the contrary, and show that this leads to a contradiction. If C ⊈ V (P), then there is a letter l ∈ C such that l ∉ V (P). Since C = NΔQ, there are only two possibilities:

1. l ∈ N, l ∉ Q. Define Q′ as Q ∪ {l}. Since l ∉ V (P), Q′ ⊧ P. Since l ∉ V (P), l ∉ S, hence l ∉ NΔM, hence l ∈ M, which implies MΔQ′ ⊂ MΔQ, contradicting the above hypothesis.

2. l ∉ N, l ∈ Q. Define Q′ as Q \ {l}. Since l ∉ V (P), Q′ ⊧ P. Since l ∉ V (P), l ∉ S, hence l ∉ NΔM, hence l ∉ M, which implies MΔQ′ ⊂ MΔQ, contradicting the above hypothesis.

Contradiction follows by noticing that we found a set C such that C ⊆ V (P), |CΔS| < |S| and N ⊧ P [C/Ĉ].

We conclude this section by showing an example of the formulae obtained by applying formula (7).

Example. Let T and P be defined as:

T = a ∧ b ∧ c ∧ d ∧ e
P = ¬a ∨ ¬b

T has just one model (call it M), while P has 3×2^{3} models (each combination of the models of ¬a ∨ ¬b with 2^{{c,d,e}}). T ∧ P has no models. The minimum cardinality of differences between M and each model of P is k_{M,P} = 1, corresponding to models {a, c, d, e} and {b, c, d, e} of P. These are the models of T ∗_{F} P.

V (P) is {a, b}. Applying (7), we get for T ∗_{F} P

P ∧ ⋁_{S={},{a},{b},{a,b}} (T [S/Ŝ] ∧ ¬ ⋁_{C⊆V (P) , |CΔS|<|S|} P [C/Ĉ])

i.e.

P ∧ ( (a ∧ b ∧ c ∧ d ∧ e)
∨ ((¬a ∧ b ∧ c ∧ d ∧ e) ∧ ¬ ⋁_{C={a}} P [C/Ĉ])
∨ ((a ∧ ¬b ∧ c ∧ d ∧ e) ∧ ¬ ⋁_{C={b}} P [C/Ĉ])
∨ ((¬a ∧ ¬b ∧ c ∧ d ∧ e) ∧ ¬ ⋁_{C={a},{b},{a,b}} P [C/Ĉ]) )

i.e.

(¬a ∨ ¬b) ∧ ( (a ∧ b ∧ c ∧ d ∧ e)
∨ ((¬a ∧ b ∧ c ∧ d ∧ e) ∧ ¬(a ∨ ¬b))
∨ ((a ∧ ¬b ∧ c ∧ d ∧ e) ∧ ¬(¬a ∨ b))
∨ ((¬a ∧ ¬b ∧ c ∧ d ∧ e) ∧ ¬((a ∨ ¬b) ∨ (¬a ∨ b) ∨ (a ∨ b))) )

It is easy to verify that this formula has exactly two models: {b, c, d, e} (i.e. the unique model of the subformula on the second line), and {a, c, d, e} (i.e. the unique model of the subformula on the third line).

4.2 Compactability of “global” operators

For Satoh’s operator, the representation stems directly from the definition. We first compute off-line the set δ(T, P) of minimal global differences between models of T and models of P. Then we represent Satoh’s revision as:

P ∧ ⋁_{S∈δ(T,P)} T [S/Ŝ]  (8)

Theorem 4.6 Formula (8) has size linear in |T | and is logically equivalent to T ∗_{W eb}P.

Proof. The size of the formula is O(|P | + |T |^{card(δ(T,P))}). Observe that, by Proposition 2.1, each set in δ(T, P) is contained in V (P) hence δ(T, P) is a subset of the powerset of V (P), hence card(δ(T, P)) is bounded by 2^{c}k, for some constant c. Therefore, the size of Formula (8) is linear in |T | and doubly exponential in k.

As for the logical equivalence, we split the proof in two parts.

(1st part) Let N be a model of T ∗_{S} P. By definition, N ∈ M(P) and there exists M ∈ M(T) such that NΔM ∈ δ(T, P). Let S ≐ NΔM; then S ∈ δ(T, P), and N = MΔS. From Proposition 4.2, M ∈ M(T) iff MΔS ⊧ T [S/Ŝ], that is, N ⊧ T [S/Ŝ]. Hence N is a model of Formula (8).

(2nd part) Let N be a model of Formula (8). Then N ⊧ P and there is an S ∈ δ(T, P) such that N ⊧ T [S/Ŝ]. From Proposition 4.2, this implies NΔS ⊧ T. Let M ≐ NΔS. Then M is a model of T and MΔN ∈ δ(T, P). Hence N is a model of T ∗_{S} P.

Also for Dalal’s operator, the representation stems directly from the definition of revision, once k_{T,P} (the minimum cardinality of sets in δ(T, P)) is computed off-line. Dalal’s revision can be represented as:

P ∧ ⋁_{card(S)=k_{T,P}} T [S/Ŝ]  (9)

Theorem 4.7 Formula (9) has size linear in |T | and is logically equivalent to T ∗_{D} P.

Proof. The size of the formula is O(|P | + |T |^{b}), where b is the binomial coefficient

( \begin{matrix}k \\ k_{T,P} \end{matrix} ) Since, by Proposition 2.1, sets in δ(T, P) are subsets of P, k_{T,P} ≤ k = |P |,

hence the above binomial is less than 2^{k}. Therefore, the size of Formula (9) is linear in |T | and, at most, doubly exponential in k.

As for the other statement, the proof is similar to the one for the representation of Satoh’s revision.

(1st part) Let N be a model of T ∗_{D} P. By definition, N ∈ M(P) and there exists M ∈ M(T) such that card(NΔM) = k_{T,P}. Let S ≐ NΔM; then card(S) = k_{T,P}, and N = MΔS. From Proposition 4.2, M ∈ M(T) iff MΔS ⊧ T [S/Ŝ], that is, N ⊧ T [S/Ŝ]. Hence N is a model of Formula (9).

(2nd part) Let N be a model of Formula (8). Then N ⊧ P and there is an S such that card(S) = k_{T,P} and N ⊧ T [S/Ŝ]. From Proposition 4.2, this implies NΔS ⊧ T. Let M ≐ NΔS. Then M is a model of T and card(MΔN) = k_{T,P}. Hence N is a model of T ∗_{D} P.

A similar representation can be found for Weber’s operator. Computed off-line the set Ω, the explicit representation of T ∗_{W eb} P is

P ∧ ⋁_{S⊆Ω} T [S/Ŝ]  (10)

Theorem 4.8 Formula (10) has size linear in |T | and is logically equivalent to T ∗_{W eb} P.

Proof. The size of the formula is O(|P | + |T |^{card(Ω)}), hence it is linear in |T | and exponential in card(Ω). Observe that, by Proposition 2.1, card(Ω) is bounded by card(V (P)) = k. As for the other statement, the proof is identical to the one for the representation of Satoh’s revision, substituting δ(T, P) with Ω.

Note that all representations can be simplified by omitting in the disjunction all T [S/Ŝ] which are inconsistent with P.

Summing up, we have presented several results about the size of a propositional theory T′ representing the revision of a knowledge base and satisfying either criterion (1) or (2). We proved that some formalizations of belief revision (e.g., Forbus’ and Ginsberg-Fagin-Ullman-Vardi’s) lead to propositional theories T′ which are intrinsically not representable in polynomial space (unless there is a collapse in the polynomial hierarchy). Dalal’s and Weber’s formalizations have an interesting behavior: T′ has no polynomial-size representation if we insist on logical equivalence (2), but such a representation does exist if we ask only query equivalence (1). Restricting our attention to the bounded-size case also lead to interesting results. Some formalizations retain their non-compactability, while others admit a compact representation. In this case no differences arise when we choose a different equivalence criterion. Results are summarized in Table 1, where YES stands for compactable, while NO stands for not compactable.

We close this first part with an example:

Example. We continue the previous example. Recall that T and P are defined as:

T = a ∧ b ∧ c ∧ d ∧ e
P = ¬a ∨ ¬b

T has just one model (call it M), while P has 3×2^{3} models (each combination of the models of ¬a ∨ ¬b with 2^{{c,d,e}}). T ∧ P has no models. The set of minimal differences

General case  Bounded case
Formalism Logical equiv. (2) Query equiv. (1) Logical equiv. (2)  Query equiv. (1)
GFUV,  NO  NO  NO  NO
Nebel  th. 3.7  th. 3.1  th. 4.1  th. 4.1
Winslett  NO  NO  YES  YES
th. 3.7  th. 3.2  th. 4.3  th. 4.3, [Win90]
Borgida  NO  NO  YES  YES
th. 3.7  th. 3.2  co. 4.4  co. 4.4, [Win90]
Forbus  NO  NO  YES  YES
th. 3.7  th. 3.3  th. 4.5  th. 4.5
Satoh  NO  NO  YES  YES
th. 3.7  th. 3.2  th. 4.6  th. 4.6
Dalal  NO  YES  YES  YES
th. 3.6  th. 3.4  th. 4.7  th. 3.4, th. 4.7
Weber  NO  YES  YES  YES
th. 3.6  th. 3.5  th. 4.8  th. 3.5, th. 4.8, [Win90]
WIDTIO  YES  YES  YES  YES
–  –  –  –

Table 1: Is the revised knowledge base compactable? between models of T and models of P is δ(T, P) = {{a}, {b}}, corresponding to models {a, c, d, e} and {b, c, d, e} of P. These are the models of T ∗_{S} P. Since both differences have the minimum cardinality, k_{T,P} = 1, these two models are also models for T ∗_{D} P. Moreover, since Ω = {a, b} = V (P), T ∗_{W eb} P has also the third model {b, c, e}.

Applying either Formula (8) or Formula (9), we get for T ∗_{S} P = T ∗_{D} P

P ∧ ( ⋁_{S={a},{b}} T [S/Ŝ])

i.e.

(¬a ∨ ¬b) ∧ ( (¬a ∧ b ∧ c ∧ d ∧ e)
∨ (a ∧ ¬b ∧ c ∧ d ∧ e) )

This formula admits indeed the two models {b, c, d, e}, and {a, c, d, e}. Although it has exactly the same two models as T ∗_{F} P, it is syntactically much simpler.

As for T ∗_{W eb} P, Formula (10) yields

P ∧ (  ⋁_{S={a},{b},{a,b}} T [S/Ŝ])

i.e.

(¬a ∨ ¬b) ∧ ( (¬a ∧ b ∧ c ∧ d ∧ e)
∨ (a ∧ ¬b ∧ c ∧ d ∧ e)
∨ (¬a ∧ ¬b ∧ c ∧ d ∧ e) )

which admits also the model {c, d, e}.

5 Iterated unbounded revision

In the previous sections we have analyzed the size of the smallest propositional representation of the result of a single revision or update. We now turn our attention to the size of the result of a series of revisions or updates. Obviously, we only investigate operators that admit a compact representation after a single revision, since operators shown uncompactable for a single revision are also uncompactable for a series of revisions. In the style of Sections 3 and 4 we divide our analysis into two distinct cases: The general one (considered in this section), where no constraints are imposed on the sequence of m revising formulae {P^{1}, …, P^{m}}, and the bounded case (considered in the next section), where we assume that the size of each P^{i} is bounded by a constant.

In the general case, we only need to investigate the properties of Dalal’s and Weber’s operators under the query equivalence criterion. In particular, we show that Dalal’s and Weber’s operators retain their compactability properties even if the revision process is iterated m times, if we go for criterion (1), i.e. the initial language is extended.

For what concerns Dalal’s operator, note that the straightforward, m-times repeated, application of Theorem 3.4 yields a formula of size exponential in |T |+|P |+m. Therefore, we need to show a different formula.

Let EXA(r, S_{1}, S_{2}, S_{3}) denote the formula defined in Section 3.1 and containing letters of S_{1} and S_{2}, and possibly other letters S_{3}, which is true iff the Hamming distance between the values assigned to S_{1} and S_{2} is exactly r.

Now let P^{1}, …, P^{m} be the sequence of revising formulae. We denote with k_{1} the minimum distance between the models of P^{1} and T and with k_{i} the minimum distance between the models of P^{i} and T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{i−1}. Moreover, we define X = V (T) ∪ V (P^{1}) ∪ ⋯ ∪ V (P^{m}) and we use a family Y_{i} of sets of (distinct) letters, where each member Y_{i} of the family Y is one-to-one with X. Using this notation, the revised theory T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{m} can be expressed as:

T [X/Y_{1}]∧P^{1}[X/Y_{2}]∧…∧P^{m−1}[X/Y_{m−1}]∧P^{m}∧EXA(k_{1}, Y_{1}, Y_{2}, W_{1})∧…∧EXA(k_{m}, Y_{m}, X, W_{m})

(11)

Note that the formula contains m distinct instances of the formula EXA, each one comparing sets of cardinality at most n. Thus, we have:

Theorem 5.1 Formula (11) has size polynomial in |T |+|P^{1}|+⋯+|P^{m}| and is query equivalent to T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{m}.

Proof. Let Q be a query on the alphabet X. We prove the theorem by showing that T [X/Y_{1}]∧P^{1}[X/Y_{2}]∧…∧P^{m} ∧EXA(k_{1}, Y_{1}, Y_{2}, W_{1})∧…∧EXA(k_{m}, Y_{m}, X, W_{m}) ⊧ Q iff T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{m} ⊧ Q. The proof is by induction on m, and the base case is proven in Theorem 3.4.

If. We show that T [X/Y_{1}] ∧ P^{1}[X/Y_{2}] ∧ … ∧ P^{m} ∧ EXA(k_{1}, Y_{1}, Y_{2}, W_{1}) ∧ … ∧ EXA(k_{m}, Y_{m}, X, W_{m}) |̸= Q implies T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{m} |̸= Q. Let M be a model of T [X/Y_{1}] ∧ P^{1}[X/Y_{2}] ∧ … ∧ P^{m} ∧ EXA(k_{1}, Y_{1}, Y_{2}, W_{1}) ∧ … ∧ EXA(k_{m}, Y_{m}, X, W_{m}) such that M |̸= Q, and let N = M ∩ X. Since Q only uses letters of X, it holds N |̸= Q. Since M ⊧ EXA(k_{m}, Y_{m}, X, W_{m}), the distance between the two sets M ∩ X and M ∩ Y_{m} is exactly k_{m}. Let M′ = (MΔ(X ∪ Y_{m})) ∪ {x_{i}|y_{n}^{i} ∈ M}. Note that, by construction, M′ ⊧ T [X/Y_{1}] ∧ P^{1}[X/Y_{2}] ∧ … ∧ P^{m−1} ∧ EXA(k_{1}, Y_{1}, Y_{2}, W_{1}) ∧ … ∧ EXA(k_{m−1}, Y_{m−1}, X, W_{m−1}) and, by the inductive hypothesis, M′ ∩ X is a model of T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{m−1}. Therefore, M ∩ X has distance k_{m} from a model (M′ ∩ X) of T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{m−1} and, therefore, it is also a model of T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{m}.

Only If. We show that T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{m} |̸= Q implies T [X/Y_{1}] ∧ P^{1}[X/Y_{2}] ∧ … ∧ P^{m} ∧ EXA(k_{1}, Y_{1}, Y_{2}, W_{1}) ∧ … ∧ EXA(k_{m}, Y_{m}, X, W_{m}) |̸= Q. Let N_{n+1} be a model of T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{m} such that N_{n+1} |̸= Q. By definition, there exists a model N_{m} of T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{m−1} such that the distance between N_{n+1} and N_{m} is exactly k_{m}. Inductively, for any i, there exists a model M_{i} of T ∗_{D} P^{1} ∗_{D} ⋯ ∗_{D} P^{i−1} such that the distance between M_{i+1} and M_{i} is exactly k_{i}. Now, let M = {y_{1}^{i}|x_{i} ∈ N_{1}} ∪ {w_{1}^{i}|EXA(k_{1}, Y_{1}, Y_{2}, W_{1}) holds } ∪ ⋯ ∪ {y_{n}^{i}|x_{i} ∈ N_{m}} ∪ {w_{m}^{i}|EXA(k_{m}, Y_{m}, X, W_{m}) holds }∪N_{m}. Since Q only uses letters of X, and M agrees with N_{m} on X, we have that M |̸= Q. Moreover, by construction, M is a model of T [X/Y_{1}] ∧ P^{1}[X/Y_{2}] ∧ … ∧ P^{m} ∧ EXA(k_{1}, Y_{1}, Y_{2}, W_{1}) ∧ … ∧ EXA(k_{m}, Y_{m}, X, W_{m}).

Now we show how Weber’s revision can be compactly represented also for iterated revisions. By Theorem 3.5 we know that the propositional representation of T ∗_{W eb} P only increases the size of |T | + |P | by a linear factor. We denote with Ω_{i} the set associated to the i-th revision step (T ∗_{W eb} P^{1} ∗_{W eb} ⋯ ∗_{W eb} P^{i−1}) ∗_{W eb} P^{i}. To each Ω_{i} we associate a new set Z_{i}, one-to-one with Ω_{i}. Therefore, T ∗_{W eb} P^{1} ∗_{W eb} ⋯ ∗_{W eb} P^{m} can be represented by the formula:

T [Ω_{1}/Z_{1}; ⋯; Ω_{n}/Z_{m}]∧P^{1}[Ω_{2}/Z_{2}; ⋯; Ω_{n}/Z_{m}]∧…∧P^{i}[Ω_{i+1}/Z_{i+1}; ⋯; Ω_{n}/Z_{m}]∧…∧P^{m}

(12)

where the substitutions must be performed in left-to-right order. Thus, we obtain:

Corollary 5.2 Formula (12) has size linear in |T | + |P^{1}| + ⋯ + |P^{m}| and is query equivalent to T ∗_{W eb} P^{1} ∗_{W eb} ⋯ ∗_{W eb} P^{m}.

We close this section with an example of the application of Formula (12).

Example. We expand the example of the previous section. To highlight the one-to-one correspondence between sets of letters, we use {x_{1}, x_{2}, x_{3}, x_{4}, x_{5}} instead of {a, b, c, d, e}. We define T, P^{1} and P^{2} as:

T = x_{1} ∧ x_{2} ∧ x_{3} ∧ x_{4} ∧ x_{5}
P^{1} = ¬x_{1} ∨ ¬x_{2}
P^{2} = ¬x_{5}

T has just one model (call it M), while P^{1} has 3×2^{3} models and P^{2} has 2^{4} models. Recall that Ω_{1} = {x_{1}, x_{2}} = V (P^{1}) and, therefore, T ∗_{W eb}P^{1} has models {x_{1}, x_{3}, x_{4}, x_{5}}, {x_{2}, x_{3}, x_{4}, x_{5}} and {x_{3}, x_{4}, x_{5}}. Now, Ω_{2} = {x_{5}} = V (P^{2}). As a consequence, T ∗_{W eb} P^{1} ∗_{W eb} P^{2} has models {x_{1}, x_{3}, x_{4}}, {x_{2}, x_{3}, x_{4}} and {x_{3}, x_{4}}. We define two sets Z_{1} = {z_{1}^{1}, z_{1}^{2}} and Z_{2} = {z_{2}^{1}}.

Applying Formula (12) yields T [x_{1}/z_{1}^{1}, x_{2}/z_{1}^{2}, x_{5}/z_{2}^{1}] ∧ P^{1}[x_{5}/z_{2}^{1}] ∧ P^{2} i.e.

(z_{1}^{1} ∧ z_{1}^{2} ∧ x_{3} ∧ x_{4} ∧ z_{2}^{1}) ∧ (¬x_{1} ∨ ¬x_{2}) ∧ (¬x_{5})

which admits the three models {x_{1}, x_{3}, x_{4}, z_{1}^{1}, z_{1}^{2}, z_{2}^{1}}, {x_{2}, x_{3}, x_{4}, z_{1}^{1}, z_{1}^{2}, z_{2}^{1}} and {x_{3}, x_{4}, z_{1}^{1}, z_{1}^{2}, z_{2}^{1}} which – projecting out z_{1}^{1}, z_{1}^{2} and z_{2}^{1} – are exactly the models of T ∗_{W eb}P^{1}∗_{W eb} P^{2}.

6 Iterated bounded revision

In this section we assume that the size of all formulae {P^{1}, …, P^{m}} of the sequence of revisions is bounded by a constant. However, we assume that the number of revisions is arbitrary, therefore, in order to show the existence of compact representations, we must show formulae whose size is bounded by a polynomial in |T | + m.

We first focus on the query equivalence criterion. Note that the propositional formulae presented in Section 4.2 increase exponentially in m their size if the revision operator is iterated m times. As a consequence, we first find new formulae, that only preserve query equivalence, but that can be iterated without exploding the size. Since all the representations are very similar, we only show the representation for Winslett’s operator.

Without loss of generality, assume that the alphabet V (P) of P is included in the alphabet of T and let V (T) be the alphabet of T. Because of the assumption of |P | being bounded by k, it follows that card(V (P)) ≤ k. We assume card(V (P)) = k, and rearrange subscripts in such a way that V (P) = {x_{1}, …, x_{k}}. Let Y be a set of letters one-to-one with V (P). Since T ∧ P may be inconsistent, we replace in T the letters in V (P) with the new letters Y. This yields the formula

T [V (P)/Y] ∧ P  (13)

This formula is satisfiable – if both T and P are – but it is not query equivalent to T ∗_{W in} P, since any model of P can be suitably extended to a model of (13). Hence we want to impose further constraints to this formula.

Let M be a model of (13), i.e. an assignment to V (T) ∪ Y. Let \overline{V (P)} denote the set V (T) − V (P), i.e. letters of T not appearing in P. We partition M as M_{|V (P)} ∪ M_{|\overline{V (P)}} ∪ M_{|Y}, with M_{|V (P)} = M ∩ V (P), M_{|\overline{V (P)}} = M ∩ (\overline{V (P)}) and M_{|Y} = M ∩ Y. Let M′ = {x_{i} ∈ V (P) | y_{i} ∈ M_{|Y} }, i.e. M′ = M_{|Y} [Y/V (P)]. Observe that M is a model of (13) if and only if M is a model of P, and M′ ∪ M_{|\overline{V (P)}} is a model of T.

By Proposition 2.1, it follows that the models of P which are closest to a model M of T – i.e. having minimal set difference with M – agree with M on letters in \overline{V (P)}.

Therefore, a model M = M_{|V (P)} ∪ M_{|\overline{V (P)}} ∪ M_{|Y} of (13) should be discarded if there exists another model of P which is closer to the model M′ ∪ M_{|\overline{V (P)}} of T. Let Z be a set of letters one-to-one with V (P). In order to make the notation more compact, we introduce three formula schemata:

F_{P} (S) = P [V (P)/S]
F_{⊆}(S_{1}, S_{2}, S_{3}, S_{4}) = ⋀_{j=1}^{k}((s_{1}^{j} ≢ s_{2}^{j}) → (s_{3}^{j} ≢ s_{4}^{j}))

F_{⊉}(S_{1}, S_{2}, S_{3}, S_{4}) = ⋁_{j=1}^{k}((s_{1}^{j} = s_{2}^{j}) ∧ (s_{3}^{j} ≢ s_{4}^{j}))

where the sets S, S_{1}, S_{2}, S_{3} and S_{4} contain k letters each. The first schema F_{P} insures that the assignment to S is a model of P, the second one F_{⊆} that the differences between the assignments to S_{1} and S_{2} are less than the differences between the assignments to S_{3} and S_{4} (i.e. (S_{1}ΔS_{2})⊆(S_{3}ΔS_{4})). While the last schemata F_{⊉} enforces that the differences between the assignments to S_{1} and S_{2} are not more than or equal to the differences between the assignments to S_{3} and S_{4} (i.e. (S_{1}ΔS_{2})⊉(S_{3}ΔS_{4})).

Using this notation, we impose that an assignment to Z is a model of P with the formula F_{P} (Z). The assignment M_{|Z} on Z defines an assignment M′′ on V (P) as M′′ = {x_{i} ∈ V (P) | z_{i} ∈ M_{|Z}}, i.e. M′′ = M_{|Z}[Z/V (P)]. This assignment is closer to M′ than the assignment M_{|V (P)} iff (M′′ΔM′) ⊂ (M_{|V (P)}ΔM′), i.e. iff the two formulae F_{⊆}(Z, Y, Y, V (P)) and F_{⊉}(Z, Y, Y, V (P)) are both satisfied. In fact, the first one enforces that the assignment on Z is closer to the assignment on Y than a model of P does, while the second one enforces that the assignment on Z is not equal or more far away to the assignment on Y than a model of P does.

Since a model of (13) must be considered only if there does not exist a closer model, the whole revision can be reformulated as the following quantified boolean formula:

T [V (P)/Y] ∧ P ∧ ¬∃Z.(F_{P} (Z) ∧ F_{⊆}(Z, Y, Y, V (P)) ∧ F_{⊉}(Z, Y, Y, V (P))  (14)

where ∃Z is a shorthand for ∃z_{1} ⋯ ∃z_{k}. This formula could be turned into an (unquantified) propositional formula by replacing the existential quantification with a disjunction over all assignments to Z, which are 2^{k} (a constant, since k = |P | is a constant). Hence the total size of T ∗_{W in} P is O(|T | + |P | + 2^{|P |}). Observe that the assignments to Z which are not models of P can be discarded (they do not satisfy F_{P} (Z)), and the simplified formula is linear in the number of models of P, hence it could be significantly smaller than 2^{|P |}. Note that this explicit representation introduces new letters, hence it does not preserve logical equivalence (2). A linear-size representation with new letters was also shown by Winslett herself in [Win90].

Example. As in the last example, T = x_{1} ∧ x_{2} ∧ x_{3} ∧ x_{4} ∧ x_{5} and M is its unique model. While P = ¬x_{1} ∨ ¬x_{2} and it has 3×2^{3} models (each combination of the models of ¬x_{1} ∨ ¬x_{2} with 2^{{x_{3},x_{4},x_{5}}}). T ∧ P has no models.

V (P) is {x_{1}, x_{2}}. Let Y = {y_{1}, y_{2}} and Z = {z_{1}, z_{2}} be two sets whose letters are one-one with V (P). Applying (14), we get for T ∗_{W in} P

(y_{1} ∧ y_{2} ∧ x_{3} ∧ x_{4} ∧ x_{5})

∧ (¬x_{1} ∨ ¬x_{2})

∧

¬∃z_{1}∃z_{2}. ( \begin{matrix}¬z_{1} ∨ ¬z_{2} \\ ∧ \\ (z_{1} ≢ y_{1}) → (y_{1} ≢ x_{1}) ∧ (z_{2} ≢ y_{2}) → (y_{2} ≢ x_{2}) \\ ∧ \\ (((z_{1} ≡ y_{1}) ∧ (y_{1} ≢ x_{1})) ∨ ((z_{2} ≡ y_{2}) ∧ (y_{2} ≢ x_{2}))) \end{matrix} )

Substituting the existential quantifications with a disjunction corresponding to the four possible assignments

( \begin{matrix}z_{1} ↦ true \\ z_{2} ↦ true \end{matrix} ) ( \begin{matrix}z_{1} ↦ true \\ z_{2} ↦ false \end{matrix} ) ( \begin{matrix}z_{1} ↦ false \\ z_{2} ↦ true \end{matrix} ) ( \begin{matrix}z_{1} ↦ false \\ z_{2} ↦ false \end{matrix} )

and considering that the first assignment does not satisfy F_{P} (Z), hence it can be discarded, one obtains

(y_{1} ∧ y_{2} ∧ x_{3} ∧ x_{4} ∧ x_{5})

∧ (¬x_{1} ∨ ¬x_{2})

∧ ¬(

( \begin{matrix}¬⊤ ∨ ¬⊥ \\ ∧ \\ (⊤ ≢ y_{1}) → (y_{1} ≢ x_{1}) ∧ (⊥ ≢ y_{2}) → (y_{2} ≢ x_{2}) \\ ∧ \\ (((⊤ ≡ y_{1}) ∧ (y_{1} ≢ x_{1})) ∨ ((⊥ ≡ y_{2}) ∧ (y_{2} ≢ x_{2}))) \end{matrix} )

∨

( \begin{matrix}¬⊥ ∨ ¬⊤ \\ ∧ \\ (⊥ ≢ y_{1}) → (y_{1} ≢ x_{1}) ∧ (⊤ ≢ y_{2}) → (y_{2} ≢ x_{2}) \\ ∧ \\ (((⊥ ≡ y_{1}) ∧ (y_{1} ≢ x_{1})) ∨ ((⊤ ≡ y_{2}) ∧ (y_{2} ≢ x_{2}))) \end{matrix} )

∨

( \begin{matrix}¬⊥ ∨ ¬⊥ \\ ∧ \\ (⊥ ≢ y_{1}) → (y_{1} ≢ x_{1}) ∧ (⊥ ≢ y_{2}) → (y_{2} ≢ x_{2}) \\ ∧ \\ (((⊥ ≡ y_{1}) ∧ (y_{1} ≢ x_{1})) ∨ ((⊥ ≡ y_{2}) ∧ (y_{2} ≢ x_{2}))) \end{matrix} )

)

Now the formula could be simplified and rearranged; anyway, observe that the two models satisfying it are {x_{1}, x_{3}, x_{4}, x_{5}, y_{1}, y_{2}} and {x_{2}, x_{3}, x_{4}, x_{5}, y_{1}, y_{2}} which – projecting out y_{1}, y_{2} – are exactly the models of T ∗_{W in} P.

Along the same lines, one could verify that Satoh’s revision T ∗_{S} P is queryequivalent to the quantified boolean formula

T [V (P)/Y]∧P ∧¬∃W ∃Z.(F_{P} (Z)∧T [V (P)/W]∧F_{⊆}(Z, W, Y, V (P))∧F_{⊉}(Z, W, Y, V (P))

(15)

Analogously, Forbus’ revision T ∗_{F} P is query-equivalent to the quantified boolean formula

T [V (P)/Y] ∧ P ∧ ¬∃Z.(F_{P} (Z) ∧ (DIST (Z, Y) < DIST (V (P), Y)))  (16)

where DIST (·, ·) is a formula (e.g. the circuit presented in Figure 3) that computes the Hamming distance between the assignments to the two sets of letters. Moreover, the < operator can be represented with a circuit that compares the binary representations of the two numbers DIST (Z, Y) and DIST (V (P), Y).

As far as Borgida’s revision is concerned, since it coincides with Winslett’s one if T ∧ P is unsatisfiable and it is T ∧ P otherwise, a query-equivalent formula can be directly obtained from formula (14).

Formulae (14), (15) and (16) only apply to the result of a single revision, but, differently from formulae (6), (8) and (7), they can be extended to hold for a series of revisions. We first focus on Winslett’s operator.

In order to make the final formula understandable we introduce some notation. Without loss of generality, assume that for each i the alphabet V (P^{i}) of P^{i} is included in the alphabet V (T) of T. We assume that for each P^{i} its size is bounded by k_{i}, it follows that for each i, card(V (P^{i})) ≤ k_{i}. We assume card(V (P^{i})) = k_{i}. For each P^{i}, let Y_{i} and Z_{i} be sets of letters one-to-one with V (P^{i}). Given a formula T and a series of revising formulae P^{1}, …, P^{m}, we use the notation:

W IN_{1} = T [V (P^{1})/Y_{1}]∧P^{1}∧¬∃Z_{1}.(F_{P^{1}}(Z_{1})∧F_{⊆}(Z_{1}, Y_{1}, Y_{1}, V (P^{1}))∧F_{⊉}(Z_{1}, Y_{1}, Y_{1}, V (P^{1}))

(17)

and, inductively, we define:

W IN_{i} = W IN_{i−1}[V (P^{i})/Y_{i}]∧P^{i}∧¬∃Z_{i}.(F_{P^{i}}(Z_{i})∧F_{⊆}(Z_{i}, Y_{i}, Y_{i}, V (P^{i}))∧F_{⊉}(Z_{i}, Y_{i}, Y_{i}, V (P^{i}))

(18)

Note that the size of W IN_{m} is at most quadratic in |T | + m. Thus, it follows that:

Theorem 6.1 Formula (18) has size polynomial in |T | + m and is query equivalent to T ∗_{W in} P^{1} ∗_{W in} ⋯ ∗_{W in} P^{m}.

Given the similarities with Borgida’s operator, the size of the above formula is also an upper bound for Borgida’s operator. A similar construction can also be applied to Satoh’s and Forbus’ revision operators. Furthermore, the existence of a compact representation for Dalal’s and Weber’s operator is guaranteed by Theorems 5.1 and 5.2. As a consequence, we have that:

Theorem 6.2 The iterated version of formula (15) has size polynomial in |T | + m and is query equivalent to T ∗_{S} P^{1} ∗_{S} ⋯ ∗_{S} P^{m}. Furthermore, the iterated version of formula (16) has size polynomial in |T |+m and is query equivalent to T ∗_{F} P^{1} ∗_{F} ⋯∗_{F} P^{m}.

6.1 Logical Equivalence

While compact representations still exist if we go for query equivalence, this is not the case for logical equivalence.

Theorem 6.3 Unless NP ⊆ P/poly, there is no formula of size polynomial in |T | + m that is logically equivalent to T ∗ P^{1} ∗ ⋯ ∗ P^{m}, where ∗ ∈ {∗_{D}, ∗_{S}, ∗_{W eb}}.

Proof. We apply an iterated version of the general schema of Theorem 2.2 and the notation of Definition 2.5, so we show that for any integer n, there exists a sequence of n formulae P_{n}^{1} … P_{n}^{n} and a knowledge base T_{n}, both depending only on n, of polynomial size wrt n, such that given any π ∈ 3-sat_{n}, there exists an interpretation M_{π} such that π is satisfiable iff M_{π} is a model of T_{n} ∗_{D} P_{n}^{1} ∗ ⋯ ∗ P_{n}^{n}.

Let Y = {y_{1}, …, y_{n}} be a set of new letters in one-to-one correspondence with letters of B_{n}, and C be a set of new letters one for each clause in π_{n}^{max}, i.e., C = {c_{i} | γ_{i} ∈ π_{n}^{max}}. Finally, let L be the set B_{n} ∪ Y ∪ C. Notice that card(L) ∈ O(n^{3}). We define T as the conjunction of two formulae:

T = Φ ∧ Γ

The 2CNF formula Φ states non-equivalence between atoms in B_{n} and their correspondent in Y:

Φ = ⋀_{b_{i}∈B_{n}}(b_{i} ≢ y_{i}).

We define the sequence of m formulae {P_{n}^{1} … P_{n}^{n}} as:

P_{n}^{i} = (¬b_{i} ∧ ¬y_{i})

Note that the size of T is O(n^{3}) and the size of each P_{n}^{i} is constant. Moreover, T and {P_{n}^{1} … P_{n}^{n}} do not depend on a specific 3CNF formula π, but only on its size n.

We denote C_{π} = {c_{i} ∈ C | γ_{i} is a clause of π}. We show that π is satisfiable iff C_{π} is a model of T ∗ P_{n}^{1} … ∗ P_{n}^{n}, where ∗ ∈ {∗_{D}, ∗_{S}, ∗_{W eb}}. The proof is divided in three parts, one for each operator.

Dalal’s revision

We observe that in every model of T for each i there is exactly one of b_{i} and y_{i} that is true, while in every model of T ∗_{D} P_{n}^{1} both b_{1} and y_{1} are false. Hence, k_{T,P_{n}^{1}} ≥ 1. Moreover, k_{T,P_{n}^{1}} = 1 since B_{n} is a model of T and B_{n} − {b_{1}} is a model of P_{n}^{1}, and the cardinality of their difference is 1. By repeating the same line of reasoning, it follows that for all i < m we have k_{T ∗_{D}P_{n}^{1}...∗_{D}P_{n}^{i},P_{n}^{i+1}} = 1. Now C_{π} is a model of P_{n}^{n}, hence it is also a model of T ∗_{D} P_{n}^{1} … ∗_{D} P_{n}^{n} iff there exists a sequence of m models {M_{0}, M_{1}, …, M_{m}} such that:

1. M_{0} ⊧ T;

2. M_{i} ⊧ T ∗_{D} P_{n}^{1} … ∗_{D} P_{n}^{i};

3. M_{m} = C_{π};

4. card(M_{i+1}ΔM_{i}) = 1.

If. Let π be satisfiable, B_{π} be a model of π and \overline{Y_{π}} = \{y_{i} | b_{i} ∉ B_{π}\}. We define the sequence of models as follows:

• M_{0} = C_{π} ∪ B_{π} ∪ \overline{Y_{π}};

• M_{i+1} = M_{i} − {b_{i}, y_{i}}.

Note that conditions (3) and (4) are trivially satisfied, while condition (1) is satisfied because M_{0} ⊧ T since M_{0} satisfies Φ_{n} by construction of \overline{Y_{π}}, and also it satisfies Γ_{n}, because for each clause γ_{i} ∨ ¬c_{i} of Γ_{n}, either c_{i} ∉ C_{π} or γ_{i} is satisfied by B_{π}. We show that also condition (2) is satisfied by induction on m. The base case is proven by condition (1); Assume that M_{i} ⊧ T ∗_{D} P_{n}^{1} … ∗_{D} P_{n}^{i}. Since M_{i+1} ⊧ P_{n}^{i+1} and card(M_{i+1}ΔM_{i}) = 1 it follows that M_{i+1} ⊧ T ∗_{D} P_{n}^{1} … ∗_{D} P_{n}^{i+1}.

Only if. Suppose C_{π} is a model of T ∗_{D} P_{n}^{1} … ∗_{D} P_{n}^{n}. Then there exists a sequence of models {M_{0}, M_{1}, …, M_{m}} such that

1. M_{0} ⊧ T;

2. M_{i} ⊧ T ∗_{D} P_{n}^{1} … ∗_{D} P_{n}^{i};

3. M_{m} = C_{π};

4. card(M_{i+1}ΔM_{i}) = 1.

Since card(M_{i+1}ΔM_{i}) = 1, the difference M_{i+1}ΔM_{i} contains exactly 1 atom from B_{n}∪Y. Hence, all M_{i} agree on the truth assignment to atoms of C, that is, M_{i}∩C = C_{π}. We claim that M_{0} ∩ B_{n} is a model of π. In fact, M_{0} satisfies Γ_{n} = ⋀_{c_{i}∈C} γ_{i} ∨ ¬c_{i}. Simplifying Γ_{n} with truth values of M_{0} ∩ C = C_{π}, we conclude that M_{0} satisfies ⋀_{c_{i}∈C_{π}} γ_{i}, which is exactly formula π. Since the formula contains only atoms from B_{n}, the interpretation M_{0} ∩ B_{n} satisfies π, hence π is satisfiable.

Satoh’s revision

We observe that in every model of T for each i there is exactly one of b_{i} and y_{i} that is true, while in every model of T ∗_{S} P_{n}^{1} both b_{1} and y_{1} are false. Hence, all elements in δ(T, P_{n}^{1}) must contain b_{1} or y_{1}. Moreover, δ(T, P_{n}^{1}) = {b_{1}} ∪ {y_{1}} since B_{n} is a model of T while B_{n} − {b_{1}} is a model of P_{n}^{1} and Y is a model of T while Y − {y_{1}} is a model of P_{n}^{1}. By repeating the same line of reasoning, it follows that for all i < m we have δ(T ∗_{S} P_{n}^{1} … ∗_{S} P_{n}^{i}, P_{n}^{i+1}) = {b_{i+1}} ∪ {y_{i+1}}. Now C_{π} is a model of P_{n}^{n}, hence it is also a model of T ∗_{S} P_{n}^{1} … ∗_{S} P_{n}^{n} iff there exists a sequence of m models {M_{0}, M_{1}, …, M_{m}} such that:

1. M_{0} ⊧ T;

2. M_{i} ⊧ T ∗_{S} P_{n}^{1} … ∗_{S} P_{n}^{i};

3. M_{m} = C_{π};

4. M_{i+1} = M_{i} − {b_{i}, y_{i}}.

If. Let π be satisfiable, B_{π} be a model of π and \overline{Y_{π}} = \{y_{i} | b_{i} ∉ B_{π}\}. We define the sequence of models as follows:

• M_{0} = C_{π} ∪ B_{π} ∪ \overline{Y_{π}};

• M_{i+1} = M_{i} − {b_{i}, y_{i}}.

Note that conditions (3) and (4) are trivially satisfied, while condition (1) is satisfied because M_{0} ⊧ T since M_{0} satisfies Φ_{n} by construction of \overline{Y_{π}}, and also it satisfies Γ_{n}, because for each clause γ_{i} ∨ ¬c_{i} of Γ_{n}, either c_{i} ∉ C_{π} or γ_{i} is satisfied by B_{π}. We show that also condition (2) is satisfied by induction on m. The base case is proven by condition (1); Assume that M_{i} ⊧ T ∗_{S} P_{n}^{1} … ∗_{S} P_{n}^{i}. Since M_{i+1} ⊧ P_{n}^{i+1} and M_{i+1} = M_{i} − {b_{i}, y_{i}} it follows that M_{i+1} ⊧ T ∗_{S} P_{n}^{1} … ∗_{S} P_{n}^{i+1}.

Only if. Suppose C_{π} is a model of T ∗_{S} P_{n}^{1} … ∗_{S} P_{n}^{n}. Then there exists a sequence of models {M_{0}, M_{1}, …, M_{m}} such that

1. M_{0} ⊧ T; 2. M_{i} ⊧ T ∗_{S} P_{n}^{1} … ∗_{S} P_{n}^{i};

3. M_{m} = C_{π};

4. M_{i+1} = M_{i} − {b_{i}, y_{i}}.

Since M_{i+1} = M_{i} − {b_{i}, y_{i}}, the difference M_{i+1}ΔM_{i} contains exactly 1 atom from B_{n}∪Y. Hence, all M_{i} agree on the truth assignment to atoms of C, that is, M_{i}∩C = C_{π}. We claim that M_{0} ∩ B_{n} is a model of π. In fact, M_{0} satisfies Γ_{n} = ⋀_{c_{i}∈C} γ_{i} ∨ ¬c_{i}. Simplifying Γ_{n} with truth values of M_{0} ∩ C = C_{π}, we conclude that M_{0} satisfies ⋀_{c_{i}∈C_{π}} γ_{i}, which is exactly formula π. Since the formula contains only atoms from B_{n}, the interpretation M_{0} ∩ B_{n} satisfies π, hence π is satisfiable.

Weber’s revision

First observe that each P_{n}^{i} do not impose any constraint on the value of C and on the value of the all letters b_{j} ∈ B_{n} and y_{j} ∈ Y where i ≠ j, i.e. for every subset of (C ∪ B_{n} ∪ Y)Δ({b_{i}, y_{i}} there is a model of P_{n}^{i}. We define Ω_{i} ≐ ∪δ(T ∗_{W eb} P_{n}^{1} … ∗_{W eb} P_{n}^{i−1}, P_{n}^{i}).

Note that B_{n} and Y are models of T, μ(B_{n}, P_{n}^{1}) = {b_{1}} and μ(Y, P_{n}^{1}) = {y_{1}}. This implies that both {b_{1}} and {y_{1}} are in δ(T, P_{n}^{1}) ≐ ⋃_{M∈M(T)} μ(M, P_{n}^{1}). Recall that Ω_{1} ≐ ∪δ(T, P_{n}^{1}). Hence, {b_{1}} ∪ {y_{1}} ⊆ Ω_{1}. Moreover, for every model M of T, μ(M, P_{n}^{1}) contains no atom from C because for every subset of C there is a model of P_{n}^{i}. Hence, Ω_{1} = {b_{1}} ∪ {y_{1}}.

By repeating the above analysis, we obtain that Ω_{i} = {b_{i}}∪{y_{i}}. From the definition of Weber’s revision, C_{π} is a model of T ∗_{W eb} P_{n}^{1} … ∗_{W eb} P_{n}^{n} iff there exists a sequence of models {M_{0}, M_{1}, …, M_{m}} such that

1. M_{0} ⊧ T;

2. M_{i} ⊧ T ∗_{W eb} P_{n}^{1} … ∗_{W eb} P_{n}^{i};

3. M_{m} = C_{π};

4. Ω_{i} = {b_{i}} ∪ {y_{i}}.

If. Let π be satisfiable, B_{π} be a model of π and \overline{Y_{π}} = \{y_{i} | b_{i} ∉ B_{π}\}. We define the sequence of models as follows:

• M_{0} = C_{π} ∪ B_{π} ∪ \overline{Y_{π}};

• M_{i+1} = M_{i} − {b_{i}, y_{i}}.

Note that conditions (3) and (4) are trivially satisfied, while condition (1) is satisfied because M_{0} ⊧ T since M_{0} satisfies Φ_{n} by construction of \overline{Y_{π}}, and also it satisfies Γ_{n}, because for each clause γ_{i} ∨ ¬c_{i} of Γ_{n}, either c_{i} ∉ C_{π} or γ_{i} is satisfied by B_{π}. We show that also condition (2) is satisfied by induction on m. The base case is proven by condition (1); Assume that M_{i} ⊧ T ∗_{W eb} P_{n}^{1} … ∗_{W eb} P_{n}^{i}. Since M_{i+1} ⊧ P_{n}^{i+1} and Ω_{i} = {b_{i}} ∪ {y_{i}} it follows that M_{i+1} ⊧ T ∗_{W eb} P_{n}^{1} … ∗_{W eb} P_{n}^{i+1}.

Only if. Suppose C_{π} is a model of T ∗_{W eb} P_{n}^{1} … ∗_{W eb} P_{n}^{n}. Then there exists a sequence of models {M_{0}, M_{1}, …, M_{m}} such that

1. M_{0} ⊧ T;

2. M_{i} ⊧ T ∗_{W eb} P_{n}^{1} … ∗_{W eb} P_{n}^{i};

3. M_{m} = C_{π};

4. Ω_{i} = {b_{i}} ∪ {y_{i}}.

We claim that M_{0} ∩ B_{n} is a model of π. In fact, as for Dalal’s revision, M_{0} satisfies Γ_{n} = ⋀_{c_{i}∈C} γ_{i} ∨ ¬c_{i}. Simplifying Γ_{n} with truth values of M_{0} ∩ C = C_{π}, we conclude that M_{0} satisfies ⋀_{c_{i}∈C_{π}} γ_{i}, which is exactly formula π. Since the formula contains only atoms from B_{n}, the interpretation M_{0} ∩ B_{n} satisfies π, hence π is satisfiable.

The same result also holds for the other model-based revision operators. We first consider Winslett’s revision. In order to show the result, we need a preliminary lemma that relates the effect of a single revision with the effects of a series of revisions.

Lemma 6.4 Let T, P^{1} and P^{2} be three formulae. If (V (P_{1}) ∪ V (P_{2})) ⊆ V (T) and V (P^{1}) ∩ V (P^{2}) = ∅ then T ∗_{W in} (P^{1} ∧ P^{2}) ≡ (T ∗_{W in} P^{1}) ∗_{W in} P^{2}.

Proof. By Winslett’s definition, a model J of P_{1} is a model of the updated knowledge base if and only if there exists a model I of T such that J is its closest model of P^{1}.

Now consider (T ∗_{W in} P^{1}) ∗_{W in} P^{2} and one of its models M. Using Winslett’s definition, we have that M ⊧ (T ∗_{W in} P^{1}) ∗_{W in} P^{2} if and only if there exists a model J of (T ∗_{W in} P^{1}) and a model I of T such that J is one of the closest model to I and M is one of the closest models to J. By Proposition 2.1 we have that I ∩ (V (T) − V (P_{1})) = J ∩ (V (T) − V (P_{1})) and J ∩ (V (T) − V (P_{2})) = M ∩ (V (T) − V (P_{2})). Since M and J agree on the letters of V (P_{1}) and J ⊧ P_{1}, it follows that M ⊧ P_{1}. Since M is a model of P_{1}, it follows that J = M, since M is the only model of P_{1} closest to M. As a consequence, M is also one of the models closest to I and, therefore, M is a model of T ∗_{W in} (P^{1} ∧ P^{2}).

Iterating the above lemma we can show that the following property holds:

Corollary 6.5 For any T, P^{1}, …, P^{m} we have that: If for any pair of formulae P^{i}, P^{j} we have that V (P^{i}) ∩ V (P^{j}) = ∅ then T ∗_{W in} (P^{1} ∧ ⋯ ∧ P^{m}) = T ∗_{W in} P^{1} ∗_{W in} ⋯ ∗_{W in} P^{m}

Using the above corollary we can prove uncompactability of Winslett’s operator.

Theorem 6.6 Unless NP ⊆ P/poly, there is no formula of size polynomial in |T | + m that is logically equivalent to T ∗ P^{1} ∗ ⋯ ∗ P^{m}, where ∗ ∈ {∗_{W in}, ∗_{B}}.

Proof. We rephrase a reduction presented in [Lib95] for the non-iterated case and generalize it using Corollary 6.5. We use the notation of Definition 2.5. We first apply the general schema of Theorem 2.2, so we show that for any integer n, there exists a formula P_{n} and a knowledge base T_{n}, both depending only on n, of polynomial size wrt n, such that given any π ∈ 3-sat_{n}, there exists an interpretation M_{π} such that π is satisfiable iff M_{π} is a model of T_{n} ∗_{D} P_{n}.

Let Y = {y_{1}, …, y_{n}} be a set of new letters in one-to-one correspondence with letters of B_{n}, C be a set of new letters one for each clause in π_{n}^{max}, i.e., C = {c_{i} | γ_{i} ∈ π_{n}^{max}} and D a new set of atoms, one-to-one with atoms in C. Finally, let L be the set B_{n} ∪ Y ∪ C ∪ D.

We define T_{n} and P_{n} over L according to the following rules:

T_{n} = ( ⋀_{i=1}^{n}(¬b_{i} ∨ ¬y_{i})) ∧ ⋀(c_{i} → γ_{i}^{neg})
P_{n} = ⋀_{i=1}^{n}(b_{i} ≡ y_{i})

where γ^{neg} is the clauses obtained from γ by replacing every positive occurrence of b_{j} with ¬y_{j}.

Moreover, we define M_{π} as

M_{π} = B_{n} ∪ Y ∪ {c_{i} | γ_{i} ∈ π} ∪ {d_{i} | γ_{i} ∉ π}

From [Lib95] it follows that M_{π} ⊧ T_{n} ∗_{W in} P_{n} if and only if the set of clauses π is satisfiable. Using Corollary 6.5 we rewrite P_{n} in a sequence of n revisions

P_{n}^{1} = (b_{1} ≡ y_{1}), …, P_{n}^{n} = (b_{n} ≡ y_{n})

and

T_{n} ∗_{W in} P_{n} = T_{n} ∗_{W in} P_{n}^{1} ⋯ ∗_{W in} P_{n}^{n}

The result for Winslett’s revision now follows. For Borgida’s revision we only need to ensure that all revisions always apply to mutually contradicting formulae. Then, just modify T_{n} and P_{n}^{i} as follows

T_{n} = ( ⋀_{i=1}^{n}(¬b_{i} ∨ ¬y_{i})) ∧ ⋀(c_{i} → γ_{i}^{neg}) ∧ ⋀_{i=1}^{n} ¬z_{i}
P_{n}^{i} = (b_{i} ≡ y_{i}) ∧ z_{i}

Hence, this result also applies to Borgida’s revision operator.

For Forbus’ operator we can give a similar proof (the preliminary lemma still holds, and the proof of non-compactability is the same of Winslett’s).

Theorem 6.7 Unless NP ⊆ P/poly, there is no formula of size polynomial in |T | + m that is logically equivalent to T ∗_{F} P^{1} ∗_{F} ⋯ ∗_{F} P^{m}.

Proof. The proof follows the same lines of the proof of Theorem 6.6.

Summing up the results presented on iterated belief revision, we proved that all formalizations of belief revision considered (exception made for WIDTIO) lead to logically equivalent propositional theories T′ which are intrinsically not representable in polynomial space (unless there is a collapse in the polynomial hierarchy). Restricting our attention to query equivalence, we found situations where compact representations exist. Results are summarized in Table 2, where YES stands for compactable, while NO stands for not compactable.

7 Generalization and strengthening of results

Our results can be easily generalized in several directions. First of all, we can withdraw the assumption that the result of a revision must be a propositional formula. Such an assumption, which we made in the introduction, is motivated from both an epistemological and a practical point of view. However, when the result of revision is a generic data structure which admits a polynomial-time algorithm for model checking, Definition 2.4 can be rephrased as follows:

Definition 7.1 (logically-compactable (data structure) operator) An update or revision operator ∗ is logically-compactable with a data structure if and only if there exist two polynomials p_{1} and p_{2} and an algorithm ASK such that for any pair of propositional formulae T and P there exists a data structure D with the following properties:

1. |D| ≤ p_{1}(|T | + |P |);

2. for all interpretations M of V (T) ∪ V (P) the call ASK(D, M) returns yes iff M ⊧ T ∗ P;

3. ASK(D, M) requires time ≤ p_{2}(|M| + |D|).

Iterated General case  Iterated Bounded case
Formalism Logical equiv. (2) Query equiv. (1) Logical equiv. (2) Query equiv. (1)
GFUV,  NO  NO  NO  NO
Nebel  th. 3.7  th. 3.1  th. 4.1  th. 4.1
Winslett,  NO  NO  NO  YES
Borgida  th. 3.7  th. 3.2  th. 6.6  th. 6.1
Forbus  NO  NO  NO  YES
th. 3.7  th. 3.3  th. 6.7  th. 6.2
Satoh  NO  NO  NO  YES
th. 3.7  th. 3.2  th. 6.3  th. 6.2
Dalal  NO  YES  NO  YES
th. 3.6  th. 5.1  th. 6.3  th. 5.1
Weber  NO  YES  NO  YES
th. 3.6  th. 5.2  th. 6.3  th. 5.2
WIDTIO  YES  YES  YES  YES
–  –  –  –

Table 2: Is the iteratively revised knowledge base compactable?

In the above definition the algorithm ASK plays the role of model checking when applied to a data structure and not to a propositional formula. If we consider this definition, Theorem 2.2 still holds, when rephrased as follows:

Theorem 7.1 Let ∗ be a revision operator. Assume there exists a polynomial p such that, for each n > 0, there exists a pair of formulae T_{n}, P_{n} with the following properties:

1. |T_{n}| + |P_{n}| ≤ p(n);

2. for all π ∈ 3-sat_{n}, there exists an interpretation M_{π} of T_{n} ∗ P_{n} such that:

(a) M_{π} can be computed from π in polynomial time;

(b) M_{π} ⊧ T_{n} ∗ P_{n} iff π is satisfiable.

With the above hypothesis, if ∗ is logically-compactable with a data structure, then NP ⊆ P/poly.

As a consequence, our negative results also apply to all representations where the equivalent of model checking can be decided in polynomial time.

A similar modification can also be applied to Definition 2.6 of query-compactability and to Theorem 2.3.

In the previous sections we focused on showing that, for many revision operators, it is very unlikely that the result can be expressed with a compact propositional formula. In fact, we have shown that the existence of these representations would imply a collapse in the polynomial hierarchy, which most researchers in computational complexity consider to be very unlikely. However, necessary and sufficient conditions for the existence of compact representations can be obtained quite easily by applying the technique used in [CDSS95, Proof of Theorems 6 and 7]. In fact, Theorems 2.2 and 2.3 can be, more precisely, formulated as follows:

Theorem 7.2 Let ∗ be a revision operator. Assume there exists a polynomial p such that, for each n > 0, there exists a pair of formulae T_{n}, P_{n} with the following properties:

1. |T_{n}| + |P_{n}| ≤ p(n);

2. for all π ∈ 3-sat_{n}, there exists an interpretation M_{π} of T_{n} ∗ P_{n} such that:

(a) M_{π} can be computed from π in polynomial time;

(b) M_{π} ⊧ T_{n} ∗ P_{n} iff π is satisfiable.

With the above hypothesis, ∗ is logically-compactable if and only if NP ⊆ NC^{1}/poly.

Theorem 7.3 Let ∗ be a revision operator. Assume there exists a polynomial p such that, for each n > 0, there exists a pair of formulae T_{n}, P_{n} with the following properties:

1. |T_{n}| + |P_{n}| ≤ p(n);

2. for all π ∈ 3-sat_{n}, there exists a formula Q_{π} such that:

(a) Q_{π} can be computed from π in polynomial time;

(b) T_{n} ∗ P_{n} ⊧ Q_{π} iff π is satisfiable.

With the above hypothesis, ∗ is query-compactable if and only if NP ⊆ coNP/poly.

We remind (cf. [Joh90]) that the class NC^{1} consists of all languages recognizable by log-space uniform families of Boolean circuits having polynomial size and depth O(log n). Since NC^{1} ⊆ NC^{1}/poly, NP ⊈ NC^{1}/poly implies NP≠ NC^{1}. Hence proving the unconditioned impossibility of logical compactability of a revision operator would be, by Theorem 7.2, at least as strong a result as proving NP≠ NC^{1}. For a similar reason, Theorem 7.3 implies that if we are able to prove that a revision operator is unconditionally non query-compactable, then NP≠ coNP.

8 Conclusions

When we are faced with the problem of representing and keeping up-to-date a large body of information, we must choose the most appropriate representation formalism and revision operator. Our analysis suggests that important aspects in the choice of a revision operator are its compactability properties. In fact, in this paper we presented several results about the size of a propositional theory T′ representing the revision T ∗P of a knowledge base and satisfying either the query-equivalence criterion (1) or the more restrictive logical equivalence criterion (2). In particolar, we proved that some formalizations of belief revision (e.g., Forbus’ and Ginsberg-Fagin-Ullman-Vardi’s) lead to propositional theories T′ which are intrinsically not representable in polynomial space. Dalal’s and Weber’s formalizations have an interesting behavior: T′ has no polynomial-sized representation if we insist on logical equivalence (2), but such a representation does exist if we ask only query equivalence (1).

Furthermore, we investigated the impact of bounding the size of the revising formula P. Several operators (e.g., Winslett’s and Satoh’s) are logically compactable only in such a restricted case (cf. Table 1). We made another analysis about the impact of iterating the revision process an unbounded number of times. The analysis showed that many revision operators (e.g., Winslett’s and Satoh’s) become not logically compactable, although they remain query compactable (cf. Table 2).

We proved non existence of polynomial-sized representations subject to non-collapse of the polynomial hierarchy at a sufficiently low level. Anyway proving unconditional non existence of such representations is equivalent to solving some long-standing questions in computational complexity (cf. Section 7). Our results can also be generalized to general data structures (not only propositional formulae).

There are several lessons to be learned from this analysis. First of all, from both an epistemological and a practical point of view, many belief revision operators have the undesired property that, in the worst case, it is not feasible to explicitly store the result of revising an existing knowledge base with a new formula. Secondly, compactability and computational complexity of inference are two different computational aspects, although somehow related. In fact, from Eiter and Gottlob’s work [EG92] it follows that the two computationally more difficult operators are ∗_{W eb} and ∗_{W id}, which admit compact representations in more cases than computationally simpler operators such as ∗_{S} and ∗_{GF UV}. Finally, compactability is also not directly related to the selectivity of the operators in choosing the resulting set of models. As a matter of fact, the two model-based operators that more often admit compact representations are ∗_{D} and ∗_{W eb}. As shown in Figure 1, ∗_{D} is the most selective operator while ∗_{W eb} is one of the least selective ones.

Acknowledgements

This work has been supported by ASI – Agenzia Spaziale Italiana.

References

[AGM85] C. E. Alchourrón, P. Gärdenfors, and D. Makinson. On the logic of theory change: Partial meet contraction and revision functions. Journal of Symbolic Logic, 50:510– 530, 1985.

[Bor85] A. Borgida. Language features for flexible handling of exceptions in information systems. ACM Transactions on Database Systems, 10:563–603, 1985.

[BS81] F. Bancilhon and N. Spyratos. Update semantics of relational views. ACM Transactions on Database Systems, 6(4):557–575, 1981.

[CDLS95] M. Cadoli, F. M. Donini, P. Liberatore, and M. Schaerf. The size of a revised knowledge base. In Proceedings of the Fourteenth ACM SIGACT SIGMOD SIGART Symposium on Principles of Database Systems (PODS-95), pages 151– 162, 1995.

[CDSS95] M. Cadoli, F. M. Donini, M. Schaerf, and R. Silvestri. On compact representations of propositional circumscription. Technical Report RAP.14.95, Dipartimento di Informatica e Sistemistica, Università di Roma “La Sapienza”, July 1995. To appear in Theoretical Computer Science. Short version appeared in Proceedings of the Twelfth Symposium on Theoretical Aspects of Computer Science (STACS-95), pages 205–216.

[Dal88] M. Dalal. Investigations into a theory of knowledge base revision: Preliminary report. In Proceedings of the Seventh National Conference on Artificial Intelligence (AAAI-88), pages 475–479, 1988.

[EG92] T. Eiter and G. Gottlob. On the complexity of propositional knowledge base revision, updates and counterfactuals. Artificial Intelligence Journal, 57:227–270, 1992.

[EG93] T. Eiter and G. Gottlob. The complexity of nested counterfactuals and iterated knowledge base revisions. In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI-93), pages 526–531, 1993.

[For89] K. D. Forbus. Introducing actions into qualitative simulation. In Proceedings of the Eleventh International Joint Conference on Artificial Intelligence (IJCAI-89), pages 1273–1278, 1989.

[FUV83] R. Fagin, J. D. Ullman, and M. Y. Vardi. On the semantics of updates in databases. In Proceedings of the Second ACM SIGACT SIGMOD Symposium on Principles of Database Systems (PODS-83), pages 352–365, 1983.

[Gär88] P. Gärdenfors. Knowledge in Flux: Modeling the Dynamics of Epistemic States. Bradford Books, MIT Press, Cambridge, MA, 1988.

[Gin86] M. L. Ginsberg. Conterfactuals. Artificial Intelligence Journal, 30:35–79, 1986.

[GJ79] M. R. Garey and D. S. Johnson. Computers and Intractability, A Guide to the Theory of NP-Completeness. W.H. Freeman and Company, San Francisco, Ca, 1979.

[Joh90] D. S. Johnson. A catalog of complexity classes. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume A, chapter 2. Elsevier Science Publishers (North-Holland), Amsterdam, 1990.

[KL80] R. M. Karp and R. J. Lipton. Some connections between non-uniform and uniform complexity classes. In Proceedings of the Twelfth ACM Symposium on Theory of Computing (STOC-80), pages 302–309, 1980.

[KM91] H. Katsuno and A. O. Mendelzon. On the difference between updating a knowledge base and revising it. In Proceedings of the Second International Conference on the Principles of Knowledge Representation and Reasoning (KR-91), pages 387–394, 1991.

[Lib95] P. Liberatore. Compact representation of revision of Horn clauses. In Proceedings of the Eighth Australian Joint Artificial Intelligence Conference, 1995.

[LS96] P. Liberatore and M. Schaerf. The complexity of model checking for belief revision and update. In Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI-96), pages 556–561, 1996.

[Neb91] B. Nebel. Belief revision and default reasoning: Syntax-based approaches. In Proceedings of the Second International Conference on the Principles of Knowledge Representation and Reasoning (KR-91), pages 417–428, 1991.

[Neb94] B. Nebel. Base revision operations and schemes: Semantics, representation and complexity. In Proceedings of the Eleventh European Conference on Artificial Intelligence (ECAI-94), pages 341–345, 1994.

[Sat88] K. Satoh. Nonmonotonic reasoning by minimal belief revision. In Proceedings of the International Conference on Fifth Generation Computer Systems (FGCS-88), pages 455–462, 1988.

[Web86] A. Weber. Updating propositional formulas. In Proc. of First Conf. on Expert Database Systems, pages 487–500, 1986.

[Win90] M. Winslett. Updating Logical Databases. Cambridge University Press, 1990.

[Yap83] C. K. Yap. Some consequences of non-uniform conditions on uniform classes. Theoretical Computer Science, 26:287–300, 1983.