On Computational Aspects of Iterated Belief Change

1 Introduction

Belief revision theory aims to study how to incorporate in the beliefs of an agent a new piece of information that (typically) contradicts them [Alchourr´on et al., 1985; G¨ardenfors, 1988; Hansson, 1999; Ferm´e and Hansson, 2011]. Whereas the standard belief revision literature has been focused on the single-step change process, considering the iterated case, i.e., to determine what happens when several successive revision steps occur, is an important issue, that gave rise to a significant amount of work where iterated change operators have been defined and investigated [Lehmann, 1995; Darwiche and Pearl, 1997; Nayak et al., 2003; Booth and Meyer, 2006; Rott, 2006; Jin and Thielscher, 2007; Konieczny and Pino P´erez, 2008; Konieczny et al., 2010].

Improvement operators have been proposed as a general class of iterated change operators [Konieczny and Pino P´erez, 2008; Konieczny et al., 2010]. In this paper, we will study two interesting subclasses of improvement operators from a computational perspective. The first one is the class of iterated revision operators, which require the change formula to be entailed in the revised set of beliefs of the agent [Darwiche and Pearl, 1997; Nayak et al., 2003; Booth and Meyer, 2006]. The second one is the class of soft improvement operators: in contrast to iterated revision operators, these operators aim to increase in a "minimal way" the plausibility of the change formula in the beliefs of the agent [Konieczny and Pino P´erez, 2008; Konieczny et al., 2010].

∗Contact Author

In iterated belief change, it is standard to assume that the current set of beliefs of an agent is given by an epistemic state, i.e., an abstract object Φ from which the actual beliefs of the agent, denoted by B(Φ), can be extracted. In this paper, the computational complexity of iterated belief change operators ⋆ is investigated when epistemic states are represented by compact world rankings (CWRs). This representation will be formally introduced later. For the moment let us just roughly describe a CWR as a special kind of stratified belief base (an ordered set of formulae) that encodes a total preorder over the interpretations. We focus on the (onestep) inference problem: given a CWR Φ = (ϕ1, . . . , ϕn) and two formulae µ, α, is it the case that B(Φ ⋆ µ) |= α? The computational complexity of this problem is identified for several families of iterated change operators ⋆, and shown as "mildly" hard (i.e., solvable using a constant number or a logarithmic number of calls to an NP oracle). More in detail, we show that:

1. for any iterated revision operator satisfying postulates (R*1)-(R*6) [Darwiche and Pearl, 1997] the inference problem is in Θp2 , i.e., only a logarithmic number of calls to an NP oracle is necessary in the general case to decide whether a formula is entailed by a revised epistemic state;
2. for the three soft improvement operators pointed out in the literature [Konieczny et al., 2010], the inference problem is shown to be in the Boolean Hierarchy BH [Wagner, 1987; Cai et al., 1988], i.e., only a bounded number of calls to an NP oracle is needed to solve the problem; the exact complexity of the problem within BH (completeness results) is reported for each of those three operators;
3. hardness results for the inference problem, that rely only on postulates and apply to all operators satisfying them, have been identified as well. Thus, for any iterated revision operator satisfying the postulates (R*1)-(R*6), the inference problem is shown Θp2 -hard (hence, given the re-

sults in 1., it is Θp2 -complete). For any soft improvement operator, it is shown coNP(3)-hard.

Given the performance of modern SAT solvers (that are NP oracles), these results suggest that the existence of inference algorithms for iterated belief change that prove efficient enough to tackle large-sized instances is not utopic. In order to verify it, we implemented SAT-based algorithms for the iterated belief change of CWRs (seven operators have been considered). More precisely, for each change operator under consideration, we implemented the change operation Φ ⋆ µ, i.e., we designed a procedure for deriving a CWR representing Φ ⋆ µ from a CWR representing Φ, and from µ. Interestingly, with epistemic states Φ represented as CWRs, the representation of Φ ⋆ µ does not exponentially blow up in terms of size: the number of strata in the corresponding CWR representation of Φ ⋆ µ is at most twice the one of Φ. As an interesting consequence, building the CWR Φ ⋆ µ can be done in polynomial time given an NP oracle. We evaluated our SAT-based algorithms for iterated belief change on many benchmarks. The empirical results we have obtained confirm the feasibility of iterated belief change from the practical side.

The proofs of propositions can be found on http://www. cril.fr/∼konieczny/SKLM-IJCAI20-long.pdf

2 Preliminaries on Iterated Belief Change

Let LP be a propositional language built up from a finite set of propositional variables P and the usual connectives. ⊥ (resp. ⊤) is the Boolean constant always false (resp. true). An interpretation (or world) is a mapping from P to {0, 1}. |= denotes logical entailment, ≡ logical equivalence, and [ϕ] denotes the set of models of the formula ϕ. In iterated change, it is standard to assume that the set of beliefs of an agent is represented by an epistemic state (ES for short) Φ, which represents (i) the actual beliefs of the agent, i.e., a propositional formula denoted by B(Φ), and (ii) some conditional information guiding the revision process.

For conventional purposes, in the rest of the paper the symbols ◦, · and ⋆ will respectively denote an iterated revision operator, a soft improvement operator, and any iterated belief change operator.

2.1 Iterated Revision

Let us start with Darwiche and Pearl's iterated revision:

Definition 1 (DP-AGM revision operator [Darwiche and Pearl, 1997]). A DP-AGM revision operator ◦ is an operator associating an ES Φ and a formula µ with a new ES Φ ◦ µ, such that for each ES Φ and all formulae µ, µ′ :

Darwiche and Pearl also provided a characterization of DPAGM operators in terms of total preorders over worlds:

Definition 2 (faithful assignment). A function Φ ↦→⪯Φ that maps each ES Φ to a total preorder 1 over worlds ⪯Φ is a faithful assignment iff for all worlds ω, ω′ :

Proposition 1 ([Darwiche and Pearl, 1997]). An operator ◦ is a DP-AGM operator iff there exists a faithful assignment Φ ↦→⪯Φ such that for each ES Φ and each formula µ, [B(Φ◦ µ)] = min([µ], ⪯Φ).

One can see from Prop. 1 that given an ES Φ and a formula µ, the set of models of B(Φ ◦ µ) can be characterized independently of the choice of the DP-AGM revision operator ◦. However, postulates (R*1-R*6) impose no restriction on the rest of the ordering ⪯Φ◦µ. Thus four additional "rigidity" postulates (CR1-CR4) have been introduced [Darwiche and Pearl, 1997]. In addition, postulate (PR) was also introduced to also require a strict increase of the plausibility of models of µ within ⪯Φ [Booth and Meyer, 2006; Jin and Thielscher, 2007]: 2

DP-AGM operators satisfying (CR1-CR2) and (PR) are called admissible operators [Booth and Meyer, 2006]. Noteworthy, these operators also satisfy (CR3-CR4).

Let us now introduce four well-known DP-AGM operators from the literature. For space reasons, each one of them is semantically characterized by additional postulates on their corresponding faithful assignment. This also allows one to see how the revised ES Φ ◦ µ is constructed in terms of total preorders (an illustrative example is given in Fig. 1).

Boutiler's natural revision. Denoted by ◦B, it is the DPAGM operator satisfying (CR1-CR4) and the following additional postulate [Boutilier, 1996]:

Nayak's lexicographic revision. Denoted by ◦N, it is the DP-AGM operator satisfying (CR1-CR4) and the following additional postulate [Nayak et al., 2003]:

This operator satisfies (PR).

1 For each preorder ⪯, ≃ denotes the corresponding indifference relation, and ≺ the corresponding strict ordering.

2 For space reasons, we only provide the semantic versions of the postulates, i.e., in terms of properties on faithful assignments.

Lehmann's ranked revision. Denoted by ◦L, it is the DPAGM operator characterized by a widening ranked model [Lehmann, 1995]. Although Lehmann initially characterized the operator in terms of functions mapping ordinals to nonempty subsets of worlds, it can equivalently be characterized in terms of a faithful assignment satisfying the following properties:

This operator satisfies (CR1), (CR3) and (CR4) but it does not satisfy (CR2) or (PR).

Booth and Meyer's restrained revision. Denoted by ◦BM, it is the DP-AGM operator satisfying (CR1-CR2), (PR), and the following additional postulate [Booth and Meyer, 2006]:

2.2 Soft Improvement

Soft improvement operators, unlike DP-AGM ones, do not satisfy the success postulate (R*1) [Konieczny et al., 2010]. Instead, they satisfy the following one:

Definition 3 (soft improvement operator). A soft improvement operator is an operator · associating an ES Φ and a formula µ with a new ES Φ · µ such that postulates 3 (I1-I10) from [Konieczny et al., 2010] are satisfied.

Konieczny et al. [2010] also provided the following representation theorem :

Definition 4 (soft gradual assignment). A strong faithful assignment is a faithful assignment such that for each n > 0, and each ES Φ, we have ⪯Φ·α1·...·αn =⪯Φ·β1·...·βn when all formulae αi, βi, i ∈ {1, . . . , n} are such that αi ≡ βi.

A soft gradual assignment is a strong faithful assignment satisfying (CR1), (CR2), (PR) and the following property:

Proposition 2 ([Konieczny et al., 2010]). An operator · is a soft improvement operator iff there exists a soft gradual assignment Φ ↦→⪯Φ such that for each ES Φ and each formula 4 µ, [B(Φ ◦· µ)] =min([µ],⪯Φ).

As opposite to DP-AGM operators, when performing a change Φ · µ soft improvement operators · require the plausibility of all models of µ w.r.t. ⪯Φ to be increased only to a "small" extent. This behavior is reflected by (S4).

Lastly, let us introduce the (semantic) characterization of the three soft improvement operators found in [Konieczny et al., 2010].

3 Postulates are not recalled here. For space reasons we will focus on the corresponding assignment properties. The reader is invited to check [Konieczny et al., 2010] for more details.

4Φ ◦· µ = Φ ·n µ where n is the smallest integer such that B(Φ ·n µ) |= µ.

One-improvement. Denoted by ·O, it is the soft improvement operator satisfying the following additional property. For all ω, ω′ , ω ≪ ω′ is a shortcut for (ω ≺ ω′ and ∄ω′′ , ω ≺ ω′′ ≺ ω′ ):

Half-improvement. Denoted by ·H, it is the soft improvement operator satisfying the following two additional properties:

Best-improvement. Denoted by ·B, it is the soft improvement operator satisfying the following two additional properties. A formula α is separated in ⪯ for a given total preorder ⪯ iff for all ω, ω′ , if ω |= α and ω′ ̸|= α then ω ̸≃ ω′ :

(SB1) If ω |= µ, ω′ ̸|= µ, ω′ ≪Φ ω and µ is separated in ⪯Φ, then ω ⪯Φ·µ ω′ ;

(SB2) If ω |= µ, ω′ ̸|= µ, ω′ ≺Φ ω and µ is not separated in ⪯Φ, then ω′ ≺Φ·µ ω.

3 Complexity Results

From now on, we assume that each change operator ⋆ is characterized in terms of a faithful assignment (cf. Def. 2 and 4), and each ES Φ is represented by a compact world ranking (CWR for short):

Definition 5 (compact world ranking). A compact world ranking (CWR) is a vector of consistent formulae (ϕ1, . . . , ϕn), n ≥ 1, such that for all i, j, i ̸= j ⇒ ϕi ∧ ϕj |= ⊥ and ∨ni=1 ϕi is valid.

Stated otherwise, a CWR is a total ordering over a set of consistent formulae whose sets of models are jointly exhaustive and pairwise disjoint (JEPD). To obtain the ES Φ (in terms of faithful assignment) corresponding to a given CWR (ϕ1, . . . , ϕn), one simply sets ω ⪯Φ ω′ iff ω |= ϕi and ω′ |= ϕj for some i, j s.t. i < j. Doing so, it is easy to see that B(Φ) = ϕ1. Abusing notations, in the following Φ

will denote both an ES and the CWR representing it. Lastly, in a CWR Φ = (ϕ1, . . . , ϕn), for each i ∈ {1, . . . , n}, the formula ϕi is also called the ith stratum of Φ, and Φ is said to have n strata.

A CWR can be seen as a special kind of stratified belief base (SBB), as considered in several papers about revision and inference (see e.g., [Rott, 2009]), but in a CWR each stratum must be a single formula and the JEPD condition must be satisfied. The aim is to compactly represent a total preorder over the interpretations.

We are interested in identifying the computational complexity of the following decision problem:

Definition 6 (|=⋆ ). Let ⋆ be a change operator. |=⋆ is the decision problem defined as follows:

• Input: A CWR Φ, formulae µ, α.
• Question: Does B(Φ ⋆ µ) |= α hold?

We assume that the reader is familiar with the complexity classes NP and coNP. We briefly recall below some complexity classes of interest in this paper, all at the first level of the polynomial hierarchy. The class ΘP2 = P NP [O(log n)] [Wagner, 1987; Eiter and Gottlob, 1997] is the class of languages that can be recognized in polynomial time by a deterministic Turing machine using a number of calls to an NP oracle bounded by a logarithmic function of the size of the input. The Boolean hierarchy BH is the Boolean closure of NP under Boolean operations (see [Cai et al., 1988] for the formal definition of BH). Roughly speaking, a problem belongs to the class NP(k) or coNP(k) only if solving it requires at most k calls to an NP oracle.

3.1 Iterated Revision

Prop. 3 below tells us that for any DP-AGM operator ◦, one can precisely characterize the computational complexity of deciding whether a formula is entailed by a revised CWR: it "only" requires a logarithmic number of calls to an NP oracle. This result highly relies on the following lemma:

Lemma 1. Let ◦ be a DP-AGM operator. Then for any CWR Φ = (ϕ1, . . . , ϕn) and any formula µ, B(Φ ◦ µ) ≡ ϕi∗ ∧ µ, where i∗ = mini∈{1,...,n}{i | ϕi ∧ µ ̸|= ⊥}.

Proposition 3. Let ◦ be a DP-AGM operator. Then |=◦ is Θp2 -complete.

These results echo results of the same nature about (one step) base revision [Nebel, 1998], and showing that the inference problem for revision is NP-hard and coNP-hard when the operator under consideration satisfies the revision postulates. They cohere with other results pointed out in [Liberatore, 1997], where the complexity of inference for a given sequence of change formulae is identified (the problem is P NP - complete for many iterated revision operators).

3.2 Soft Improvement

Let us start with a useful lemma:

Lemma 2. Let · be a soft improvement operator, Φ = (ϕ1, . . . , ϕn) be a CWR and µ be any formula. Then:

The above result provides a set of sufficient conditions to characterize the beliefs of a revised CWR: given a CWR Φ = (ϕ1, . . . , ϕn) and a formula µ, B(Φ · µ) can be characterized in the case when µ is consistent with ϕ1, or when µ is inconsistent with ϕ1 ∨ ϕ2. As a consequence, one can derive the following hardness result for soft improvement operators:

Proposition 4. Let · be a soft improvement operator. Then |=· is coNP(3)-hard, even when Φ has at most three strata.

This means that for any soft improvement operator ·, at least three calls to an NP oracle are necessary to decide |=· . Interestingly, this is also an upper bound for the case of oneimprovement. This result uses the following lemma which characterizes B(Φ·O µ) in the case not covered in Lemma 2:

Lemma 3. Let Φ = (ϕ1, . . . , ϕn) be an ES, µ be any formula, and assume that ϕ1 ∧ µ |= ⊥ and ϕ2 ∧ µ ̸|= ⊥. Then B(Φ ·O µ) ≡ ϕ1 ∨ (ϕ2 ∧ µ).

Proposition 5. Let Φ = (ϕ1, . . . , ϕn) and α, µ be two formulae. Then |=·O can be decided by the following procedure:

1. if ϕ1 ∧ µ ∧¬α ̸|= ⊥ then return False;
2. if ϕ1 ∧ µ ̸|= ⊥ then return True;
3. if (ϕ1 ∨ (ϕ2 ∧ µ)) ∧¬α ̸|= ⊥ then return False;
4. Return True;

So as a consequence of Prop. 4 and 5, we get that:

For half-improvement and best-improvement, five calls to an NP oracle are necessary and sufficient to provide an answer to the inference problem: Prop. 7 and 8 below show membership to coNP(5), while Prop. 9 shows coNP(5)- hardness. The proofs take advantage of the following useful lemma, which shows how B(Φ ·H µ) and B(Φ ·B µ) are characterized in the remaining case not covered in Lemma 2:

Lemma 4. Let Φ = (ϕ1, . . . , ϕn) be an ES, µ be any formula, and assume that ϕ1 ∧ µ |= ⊥ and ϕ2 ∧ µ ̸|= ⊥. Then

Proposition 7. Let Φ = (ϕ1, . . . , ϕn) and α, µ be two formulae. Then |=·H can be decided by the following procedure:

1. if ϕ1 ∧ µ ∧¬α ̸|= ⊥ then return False;
2. if ϕ1 ∧ µ ̸|= ⊥ then return True;
3. if ϕ1 ∧¬α ̸|= ⊥ then return False;
4. if ϕ2 ∧¬µ ̸|= ⊥ then return True;
5. if ϕ2 ∧¬α ̸|= ⊥ then return False;
6. Return True;

Proposition 8. Let Φ = (ϕ1, . . . , ϕn) and α, µ be two formulae. Then |=·B can be decided by the procedure described in Prop. 7, where line 4 is replaced by the following:

• 4'. if Γ ̸|= ⊥ then return True,

where Γ = ∨ni=1 ϕ2i-1 i ∧ µ2i-1 ∧ϕ2i i ∧¬µ2i , and each ϕji (resp. µj ) is defined as the original formula ϕi (resp. µ) by renaming each propositional variable x into a fresh one xj .

Proposition 9. |=·H and |=·B are coNP(5)-hard. Hardness holds in each case even when Φ has at most three strata.

So from Prop. 7-9, we get that:

Proposition 10. |=·H and |=·B are coNP(5)-complete.

4 Implementing Iterated Belief Change

We describe now for each belief change operator ⋆ among the seven considered in the previous section how to encode a changed CWR Φ′ = Φ ⋆ µ, given any initial CWR Φ = (ϕ1, . . . , ϕn) and any change formula µ. In every case, Φ′ consists of formulae that are Boolean combinations (obtained using the connectives ∧, ∨, ¬) of the input formulae ϕi and µ. Noteworthy, our encodings could easily be adapted to other belief revision operators, e.g., those listed in [Rott, 2009].

4.1 Iterated Revision

For any DP-AGM operator ◦, the general idea in the construction of the CWR Φ′ = Φ ◦ µ is described as follows. One searches for the smallest index i∗ such that ϕi∗ ∧ µ is consistent, which defines the first stratum of Φ ◦ µ. Then, depending on the operator ◦ under consideration, the remaining strata ϕj (j ̸= i∗) of Φ either (i) remain unchanged in Φ ◦ µ, or (ii) are split into two consecutive strata ϕj ∧µ and ϕj ∧¬µ in Φ ◦ µ, or lastly (iii) are (disjunctively) merged with others and ranked according to an order specific to ◦.

In the descriptions, given a vector Ψ = (ψ1, . . . , ψk) of formulae whose sets of models are JEPD (but where some formulae ψi may be inconsistent), we say that Ψ′ = (ψ′1 , . . . , ψ′ l ) is a ⊥-fitering of Ψ when Ψ′ is defined as the restriction of Ψ to its consistent formulae, listed in the same order (identifying those formulae requires consistency tests). Obviously enough, the resulting vector Ψ′ is a CWR.

Boutiler's natural revision. We define the vector of formulae Ψ = (ψ1, . . . , ψn+1) as follows. We first search for i∗ and define ψ1 = ϕi∗ ∧ µ. Then we set ψi+1 = ϕi for each i ∈ {1, . . . , i∗ - 1, i∗ + 1, . . . , n}, and ψi∗+1 = ψi∗ ∧ ¬µ. Then we define Φ′ = Φ ◦B µ as the ⊥-filtering of Ψ.

Nayak's lexicographic revision. We define the vector of formulae Ψ = (ψ1, . . . , ψ2n) as ψi = ϕi ∧ µ and ψn+i = ϕi∧¬µ for each i ∈ {1, . . . , n}. Then we define Φ′ = Φ◦N µ as the ⊥-filtering of Ψ.

Lehmann's ranked revision. We define the vector of formulae Ψ = (ψ1, . . . , ψn-i∗+2) as ψ1 = ϕi∗ ∧ µ, ψ2 = (ϕi∗ ∧ ¬µ) ∨ ∨i∗-1 i=1 ϕi, and for each i ∈ {3, . . . , n-i∗ +2}, ψi = ϕi∗+i-2. Then we define Φ′ = Φ◦Lµ as the ⊥-filtering of Ψ.

Booth and Meyer's restrained revision. We first define the vector of formulae Ψ = (ψ1, . . . , ψ2n) as ψ2i-1 = ϕi ∧µ and ψ2i = ϕi ∧ ¬µ for each i ∈ {1, . . . , n}. Then, we associate with Ψ its ⊥-filtering Ψ′ . Lastly, we take advantage of the procedure described above for computing Boutiler's natural revision and define Φ′ = Φ ◦BM µ as Φ′ = Ψ′ ◦B µ.

4.2 Soft Improvement

In contrast to what happens in the iterated revision case, in order to perform an improvement of any formula into a CWR, we do not need to search for the corresponding ϕi∗ in the CWR.

One-improvement. We define the vector of formulae Ψ = (ψ1, . . . , ψn+1) as ψ1 = ϕ1 ∧ µ, ψn+1 = ϕn ∧ ¬µ, and for each i ∈ {2, . . . , n}, ψi = (ϕi-1 ∧ ¬µ) ∨ (ϕi ∧ µ). Then we define Φ′ = Φ ·O µ as the ⊥-filtering of Ψ.

Half-improvement. We first define the vector of formulae Ψ = (ψ1, . . . , ψ2n) as ψ2i-1 = ϕi∧µ and ψ2i = ϕi∧¬µ, for each i ∈ {1, . . . , n}. Then, we associate with Ψ the vector Θ = (θ1, . . . , θ2n) defined as θ1 = ψ1, θ2n = ϕ2n, and for each i ∈ {1, . . . , n - 1},

Lastly, we define Φ′ = Φ ·H µ as the ⊥-filtering of Θ.

Best-improvement. We first define the vector of formulae Ψ = (ψ1, . . . , ψ2n) as ψ2i-1 = ϕi ∧ µ and ψ2i = ϕi ∧ ¬µ, for each i ∈ {1, . . . , n}. Now, let Ψ′ be the ⊥-filtering of Ψ. Then Φ′ = Φ·Bµ is defined as Φ′ = Ψ′ if Ψ′ ̸= Φ, otherwise Φ′ = Ψ′ ·O µ.

5 Empirical Results

To evaluate from the practical viewpoint the belief change operators considered in the previous sections, we made some experiments. We generated belief change instances that consist of consistent, yet non-valid propositional formulae ϕ so that the CWR considered at start is of the form (ϕ, ¬ϕ), and sequences of change formulae µ, and we computed the corresponding changed CWR for each one of the seven operators. We measured the cumulated time required to compute the resulting CWR, and the corresponding number of strata. The propositional formulae ϕ and µ considered in our experiments are 3-CNF formulae (i.e., conjunctions of clauses of size at most 3), built using the modularity-based random generator presented in [Gir´aldez-Cru and Levy, 2015]. This generator takes advantage of a modularity parameter, impacting the community structure of the produced instances. As advocated in this paper, the corresponding formulae can be considered as pseudo-industrial random instances given that industrial instances are not purely random but have some structure.

The SAT solver used in the experiments is MiniSAT [E´en and S¨orensson, 2003]. It takes as inputs CNF formulae. Since the formulae occurring in the CWRs obtained after a sequence of change are not in CNF in the general case, achieving the consistency tests used to implement a change operation (cf. previous section) requires first to turn the corresponding formulae into CNF. This is done through the introduction of new variables, while preserving the set of logical consequences over the variables considered at start [Plaisted and Greenbaum, 1986]. All the experiments have been conducted on a cluster of Intel Xeon E5-2643 (3.30 GHz) quad core processors with 32 GiB RAM. A time-out of 900s and a memoryout of 7.6 GiB has been considered for each instance.

(d) Nb of strata (light change)

Figure 2: Empirical results.

Fig. 2(a) presents on its y-axis the median cumulated time (in seconds, over 100 instances) for computing the output CWRs associated with a sequence of change formulae, the length of it being given on the x-axis. For each instance, the 3-CNF formula ϕ considered at start is built over 4048 variables, has 12144 clauses, and is obtained using a modularity of 512, while every change formula µ of the sequence is a 3-CNF formula generated from 814 variables (among the 4048 ones used in ϕ), with 2442 clauses and for a modularity picked up at random between 3 and 50. Given the number of variables and clauses in it, every such µ corresponds to a "severe" change scenario. It must also be noted that nothing ensures that the communities existing in any µ are connected to the ones existing in ϕ. Fig. 2(b) gives on its y-axis the median number of strata in the resulting CWRs obtained for the same inputs, depending on the number of change formulae, given on the x-axis. Fig. 2(c) and 2(d) report results of the same nature as the ones given in Fig. 2(a) and 2(b), respectively, but considering "light" changes. Thus, every change formula µ of the sequence is a 3-CNF formula generated from 45 variables (among the 4048 ones used in ϕ), with 135 clauses. Logarithmic scales are used for the y-axis in each figure.

These empirical results show that both the time needed to compute the revised CWRs and the number of strata in them do not grow very quickly with the number of changes (unsurprisingly for Lehmann's ranked revision, the number of strata never increases by definition). This can be explained by the fact that the logical strength of the formulae corresponding to the strata of a CWR increases with the number of strata. Indeed, though the complexity of achieving a change step depends on the number of consistency checks that are performed (hence, on the number of strata of the CWR), the consistency checks become at some point easier when the formulae of the CWR involved in them have few models, and are more likely to be inconsistent with the change formula (and as such, filtered out). Experimentally, the nature of the change (severe vs. light) does not seem to have a strong impact on the number of strata in the resulting base (it has a more salient influence on the computation times). Interestingly, these experiments show that feasibility of iterated belief change for bases and sequences of change formulae of significant sizes.

6 RelatedWork

A closely related work is [Liberatore, 1997] where the complexity of iterated belief revision was investigated, given a sequence of change formulae. Our work differs from Liberatore's one in a number of directions. First, among the seven operators we considered, five were not studied in [Liberatore, 1997] as they have been introduced a decade later. Second, some of our complexity results apply to any DPAGM operator (Prop. 3) and any soft improvement operator (Prop. 4), while Liberatore [1997] focused on "concrete" revision operators. Lastly, the results from Liberatore [1997] are all theory-oriented, while we also performed experiments to show the extent to which iterated belief change is feasible in practice.

From the practical side, though there exist a couple of implementations of (one-step) belief revision operators (see mainly [Chou and Winslett, 1991; Dixon and Wobcke, 1993; Liberatore, 1999; Williams and Sims, 2000; Gorogiannis and Ryan, 2002; Delgrande et al., 2007; Thimm, 2014; Konieczny et al., 2017]), only few papers describe pieces of software for iterated belief revision. Indeed, the case of iterated belief revision is more tricky since it requires the representation of (complex) epistemic states. The system for iterated belief revision presented in [Zhuang et al., 2007] is based on a notion of compiled epistemic entrenchment (roughly, each cluster of formulae in the ranking is turned into its prime implicate form). Such compiled epistemic entrenchments can be viewed as compact encodings of epistemic states based on formulae, which contrasts with the representations of epistemic states we considered (our CWRs are compact, formulabased encodings of epistemic states based on worlds). The experiments reported in [Zhuang et al., 2007] consider a limited number of propositional variables (only 5).

7 Conclusion

In this paper, iterated belief change has been considered from a computational perspective. A number of complexity results for the inference problem has been provided for several (families of) iterated change operators, and empirical results have been reported as well. As future work, we plan to identify the computational complexity of the inference problem when a sequence of change formulae is considered, focusing on the change operators not considered in [Liberatore, 1997]. In addition, since iterated contraction operators [Booth and Chandler, 2016; Konieczny and Pino P´erez, 2017] are closely related to iterated revision operators, one can take advantage of our framework to encode and compute the resulting CWRs for these operators too. This is left for future work. Lastly, we will implement some other change operators (especially, those described in [Rott, 2009]) and make the code we developed for generating and querying CWRs available online.