# on_computational_aspects_of_iterated_belief_change__09d1c665.pdf

On Computational Aspects of Iterated Belief Change

Nicolas Schwind1 , S ebastien Konieczny2 , Jean-Marie Lagniez3 and Pierre Marquis2,4

1National Institute of Advanced Industrial Science and Technology, Tokyo, Japan 2CRIL - CNRS, Universit e d Artois, Lens, France 3Huawei Technologies Ltd, Boulogne-Billancourt, France 4Institut Universitaire de France nicolas-schwind@aist.go.jp, konieczny@cril.fr, jmlagniez@gmail.com, marquis@cril.fr

Iterated belief change aims to determine how the belief state of a rational agent evolves given a sequence of change formulae. Several families of iterated belief change operators (revision operators, improvement operators) have been pointed out so far, and characterized from an axiomatic point of view. This paper focuses on the inference problem for iterated belief change, when belief states are represented as a special kind of stratiﬁed belief bases. The computational complexity of the inference problem is identiﬁed and shown to be identical for all revision operators satisfying Darwiche and Pearl s (R*1-R*6) postulates. In addition, some complexity bounds for the inference problem are provided for the family of soft improvement operators. We also show that a revised belief state can be computed in a reasonable time for large-sized instances using SAT-based algorithms, and we report empirical results showing the feasibility of iterated belief change for bases of signiﬁcant sizes.

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 deﬁned 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 ﬁrst one is

Contact Author

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]. 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 stratiﬁed 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 identiﬁed 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 Θp 2, 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 identiﬁed as well. Thus, for any iterated revision operator satisfying the postulates (R*1)-(R*6), the inference problem is shown Θp 2-hard (hence, given the re-

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

sults in 1., it is Θp 2-complete). For any soft improvement operator, it is shown co NP(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 efﬁcient 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 conﬁrm 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 ﬁnite 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:

Deﬁnition 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 µ, µ :

(R*1) B(Φ µ) |= µ;

(R*2) If B(Φ) µ |= , then B(Φ µ) B(Φ) µ;

(R*3) If µ |= , then B(Φ µ) |= ;

(R*4) If µ µ , then B(Φ µ) B(Φ µ );

(R*5) B(Φ µ) µ |= B(Φ (µ µ ));

(R*6) If B(Φ µ) µ |= , then B(Φ (µ µ )) |= B(Φ µ) µ .

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

Deﬁnition 2 (faithful assignment). A function Φ 7 Φ that maps each ES Φ to a total preorder1 over worlds Φ is a faithful assignment iff for all worlds ω, ω :

1. If ω |= B(Φ) and ω |= B(Φ), then ω Φ ω ;

2. If ω |= B(Φ) and ω |= B(Φ), then ω Φ ω ;

Proposition 1 ([Darwiche and Pearl, 1997]). An operator is a DP-AGM operator iff there exists a faithful assignment Φ 7 Φ 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

(CR1) If ω |= µ and ω |= µ, then ω Φ ω ω Φ µ ω ;

(CR2) If ω |= µ and ω |= µ, then ω Φ ω ω Φ µ ω ;

(CR3) If ω |= µ and ω |= µ, then ω Φ ω ω Φ µ ω ;

(CR4) If ω |= µ and ω |= µ, then ω Φ ω ω Φ µ ω ;

(PR) If ω |= µ and ω |= µ, then ω Φ ω ω Φ µ ω .

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]:

(CBR) If ω, ω |= B(Φ Bµ), then ω Φ ω ω Φ Bµ ω .

This operator does not satisfy (PR).

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]:

(R) If ω |= µ and ω |= µ, then ω Φ Nµ ω .

This operator satisﬁes (PR).

1For each preorder , denotes the corresponding indifference relation, and the corresponding strict ordering. 2For space reasons, we only provide the semantic versions of the postulates, i.e., in terms of properties on faithful assignments.

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

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: (L1) If ω, ω |= µ and ω |= µ, ω Φ ω , then ω Φ Lµ ω ; (L2) If ω |= µ s.t. ω Φ ω , then ω Φ ω ω Φ Lµ ω ; This operator satisﬁes (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]: (DR) If ω |= µ, ω |= B(Φ BM µ) and ω |= µ, then ω Φ ω ω Φ BMµ ω.

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: (I1) There exists n > 0 such that B(Φ n µ) |= µ, where Φ n is inductively deﬁned as Φ 1 α = Φ α and for each n 1, Φ n+1 α = (Φ n α) α. Deﬁnition 3 (soft improvement operator). A soft improvement operator is an operator associating an ES Φ and a formula µ with a new ES Φ µ such that postulates3 (I1-I10) from [Konieczny et al., 2010] are satisﬁed. Konieczny et al. [2010] also provided the following representation theorem : Deﬁnition 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: (S4) If ω |= µ and ω |= µ, then ω Φ ω ω Φ µ ω.

Proposition 2 ([Konieczny et al., 2010]). An operator is a soft improvement operator iff there exists a soft gradual assignment Φ 7 Φ such that for each ES Φ and each formula4 µ, [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 reﬂected by (S4). Lastly, let us introduce the (semantic) characterization of the three soft improvement operators found in [Konieczny et al., 2010].

3Postulates 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 µ) |= µ.

Φ Φ Bµ Φ Nµ Φ Lµ

ω1 ω2 ω3 ω7

ω4 ω5 ω6 ω8 ω1 ω2 ω3

Φ BMµ Φ Oµ Φ Hµ Φ Bµ

Figure 1: Illustration of an ES Φ as a total preorder over worlds, and the changed ES Φ µ for { B, N, L, BM, O, H, B} with [µ] = {ω4, ω5, ω6, ω8}.

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

(S5) If ω |= µ and ω |= µ, then ω Φ ω ω Φ µ ω .

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

(SH1) If ω |= µ, ω |= µ, ω Φ ω and ω |= µ such that ω Φ ω, then ω Φ µ ω ;

(SH2) If ω |= µ, ω |= µ, ω Φ ω and ω |= µ such that ω Φ ω, then ω Φ µ ω.

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

Deﬁnition 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 Wn i=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 Φ

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

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 stratiﬁed 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 satisﬁed. 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:

Deﬁnition 6 (|= ). Let be a change operator. |= is the decision problem deﬁned as follows:

Input: A CWR Φ, formulae µ, α.

Question: Does B(Φ µ) |= α hold?

We assume that the reader is familiar with the complexity classes NP and co NP. We brieﬂy recall below some complexity classes of interest in this paper, all at the ﬁrst level of the polynomial hierarchy. The class ΘP 2 = PNP[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 deﬁnition of BH). Roughly speaking, a problem belongs to the class NP(k) or co NP(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 Θp 2-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 co NP-hard when the operator under consideration satisﬁes 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 identiﬁed (the problem is PNPcomplete 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:

(a) if ϕ1 µ |= then B(Φ µ) ϕ1 µ; and

(b) if (ϕ1 ϕ2) µ |= then B(Φ µ) ϕ1.

The above result provides a set of sufﬁcient 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 co NP(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: Proposition 6. |= O is co NP(3)-complete. For half-improvement and best-improvement, ﬁve calls to an NP oracle are necessary and sufﬁcient to provide an answer to the inference problem: Prop. 7 and 8 below show membership to co NP(5), while Prop. 9 shows co NP(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

B(Φ H µ) ϕ1 ϕ2 if ϕ2 |= µ, ϕ1 otherwise.

B(Φ B µ) ϕ1 ϕ2 if µ is separated in Φ, ϕ1 otherwise.

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:

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

4 . if Γ |= then return True,

where Γ = Wn i=1 ϕ2i 1 i µ2i 1 ϕ2i i µ2i, and each ϕj i (resp. µj) is deﬁned as the original formula ϕi (resp. µ) by renaming each propositional variable x into a fresh one xj. Proposition 9. |= H and |= B are co NP(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 co NP(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 deﬁnes the ﬁrst 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 speciﬁc 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 -ﬁtering of Ψ when Ψ is deﬁned 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 deﬁne the vector of formulae Ψ = (ψ1, . . . , ψn+1) as follows. We ﬁrst search for i and deﬁne ψ1 = ϕi µ. Then we set ψi+1 = ϕi for each i {1, . . . , i 1, i + 1, . . . , n}, and ψi +1 = ψi µ. Then we deﬁne Φ = Φ B µ as the -ﬁltering of Ψ. Nayak s lexicographic revision. We deﬁne the vector of formulae Ψ = (ψ1, . . . , ψ2n) as ψi = ϕi µ and ψn+i = ϕi µ for each i {1, . . . , n}. Then we deﬁne Φ = Φ N µ as the -ﬁltering of Ψ. Lehmann s ranked revision. We deﬁne the vector of formulae Ψ = (ψ1, . . . , ψn i +2) as ψ1 = ϕi µ, ψ2 = (ϕi µ) Wi 1 i=1 ϕi, and for each i {3, . . . , n i + 2}, ψi = ϕi +i 2. Then we deﬁne Φ = Φ Lµ as the -ﬁltering of Ψ. Booth and Meyer s restrained revision. We ﬁrst deﬁne the vector of formulae Ψ = (ψ1, . . . , ψ2n) as ψ2i 1 = ϕi µ and ψ2i = ϕi µ for each i {1, . . . , n}. Then, we associate with Ψ its -ﬁltering Ψ . Lastly, we take advantage of the procedure described above for computing Boutiler s natural revision and deﬁne Φ = Φ 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 deﬁne 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 deﬁne Φ = Φ O µ as the -ﬁltering of Ψ.

Half-improvement. We ﬁrst deﬁne 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) deﬁned as θ1 = ψ1, θ2n = ϕ2n, and for each i {1, . . . , n 1}, [θ2i = ψ2i ψ2i+1 and θ2i+1 = ] if ψ2i+2 |= , [θ2i = ψ2i and θ2i+1 = ψ2i+1] otherwise.

Lastly, we deﬁne Φ = Φ H µ as the -ﬁltering of Θ.

Best-improvement. We ﬁrst deﬁne the vector of formulae Ψ = (ψ1, . . . , ψ2n) as ψ2i 1 = ϕi µ and ψ2i = ϕi µ, for each i {1, . . . , n}. Now, let Ψ be the -ﬁltering of Ψ. Then Φ = Φ Bµ is deﬁned 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 Mini SAT [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 ﬁrst 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 Gi B RAM. A time-out of 900s and a memoryout of 7.6 Gi B has been considered for each instance.

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

20 40 60 80 100 120

number of iterations (a) Time in sec (severe change)

20 40 60 80 100 120 number of iterations (b) Nb of strata (severe change)

20 40 60 80 100 120

number of iterations (c) Time in sec (light change)

20 40 60 80 100 120 number of iterations (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 ﬁgure. 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 deﬁnition). 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, ﬁltered 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 inﬂuence on the computation times). Interestingly, these experiments show that feasibility of iterated belief change for bases and sequences of change formulae of signiﬁcant sizes.

6 Related Work

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, ﬁve 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.

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

References [Alchourr on et al., 1985] C. E. Alchourr on, P. G ardenfors, and D. Makinson. On the logic of theory change: Partial meet contraction and revision functions. Journal of Symbolic Logic, 50:510 530, 1985. [Booth and Chandler, 2016] R. Booth and J. Chandler. Extending the harper identity to iterated belief change. In IJCAI 16, pages 987 993, 2016. [Booth and Meyer, 2006] R. Booth and T. A. Meyer. Admissible and restrained revision. Journal of Artiﬁcial Intelligence Research, 26:127 151, 2006. [Boutilier, 1996] C. Boutilier. Iterated revision and minimal change of conditional beliefs. Journal of Philosophical Logic, 25(3):263 305, 1996. [Cai et al., 1988] J-Y. Cai, T. Gundermann, J. Hartmanis, L. A. Hemachandra, V. Sewelson, K. Wagner, and G. Wechsung. The Boolean hierarchy I: Structural properties. SIAM Journal of Computing, 17(6):1232 1252, 1988. [Chou and Winslett, 1991] S-C. T. Chou and M. Winslett. The implementation of a model-based belief revision system. SIGART Bulletin, 2(3):28 34, 1991. [Darwiche and Pearl, 1997] A. Darwiche and J. Pearl. On the logic of iterated belief revision. Artiﬁcial Intelligence, 89(1-2):1 29, 1997. [Delgrande et al., 2007] J. P. Delgrande, D. H. Liu, T. Schaub, and S. Thiele. COBA 2.0: A consistency-based belief change system. In ECSQARU 07, pages 78 90, 2007. [Dixon and Wobcke, 1993] S. Dixon and W. Wobcke. The implementation of a ﬁrst-order logic AGM belief revision system. In ICTAI 93, pages 40 47, 1993. [E en and S orensson, 2003] N. E en and N. S orensson. An extensible SAT-solver. In SAT 03, pages 502 518, 2003. [Eiter and Gottlob, 1997] T. Eiter and G. Gottlob. The complexity class θp 2: Recent results and applications in AI and modal logic. In FCT 97, pages 1 18, 1997. [Ferm e and Hansson, 2011] E. Ferm e and S. O. Hansson. AGM 25 years: Twenty-ﬁve years of research in belief change. Journal of Philosophical Logic, 40(2):295 331, 2011. [G ardenfors, 1988] P. G ardenfors. Knowledge in ﬂux. MIT Press, 1988. [Gir aldez-Cru and Levy, 2015] J. Gir aldez-Cru and J. Levy. A modularity-based random SAT instances generator. In IJCAI 15, pages 1952 1958, 2015. [Gorogiannis and Ryan, 2002] N. Gorogiannis and M. Ryan. Implementation of belief change operators using BDDs. Studia Logica, 70(1):131 156, 2002. [Hansson, 1999] S. O. Hansson. A Textbook of Belief Dynamics. Theory Change and Database Updating. Kluwer, 1999. [Jin and Thielscher, 2007] Y. Jin and M. Thielscher. Iterated belief revision, revised. Artiﬁcial Intelligence, 171(1):1 18, 2007.

[Konieczny and Pino P erez, 2008] S. Konieczny and R. Pino P erez. Improvement operators. In KR 08, pages 177 187, 2008. [Konieczny and Pino P erez, 2017] S. Konieczny and R. Pino P erez. On iterated contraction: Syntactic characterization, representation theorem and limitations of the levi identity. In SUM 17, pages 348 362, 2017. [Konieczny et al., 2010] S. Konieczny, M. M. Grespan, and R. Pino P erez. Taxonomy of improvement operators and the problem of minimal change. In KR 10, pages 161 170, 2010. [Konieczny et al., 2017] S. Konieczny, J-M. Lagniez, and P. Marquis. Boosting distance-based revision using SAT encodings. In LORI 17, pages 480 496, 2017. [Lehmann, 1995] D. Lehmann. Belief revision, revised. In IJCAI 95, pages 1534 1540, 1995. [Liberatore, 1997] P. Liberatore. The complexity of iterated belief revision. In ICDT 97, pages 276 290, 1997. [Liberatore, 1999] P. Liberatore. BRe LS: a system for revising, updating, and merging knowledge bases. In NRAC 99, 1999. [Nayak et al., 2003] A. C. Nayak, M. Pagnucco, and P. Peppas. Dynamic belief revision operators. Artiﬁcial Intelligence, 146(2):193 228, 2003. [Nebel, 1998] B. Nebel. How Hard is it to Revise a Belief Base?, pages 77 145. Springer Netherlands, Dordrecht, 1998. [Plaisted and Greenbaum, 1986] D. A. Plaisted and S. Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2(3):293 304, 1986. [Rott, 2006] H. Rott. Revision by comparison as a unifying framework: Severe withdrawal, irrevocable revision and irrefutable revision. Theoretical Computer Science, 355(2):228 242, 2006. [Rott, 2009] H. Rott. Shifting priorities: Simple representations for twenty-seven iterated theory change operators. In D. Makinson, J. Malinowski, and H. Wansing, editors, Towards Mathematical Philosophy, pages 269 296. Springer, 2009. [Thimm, 2014] M. Thimm. Tweety: A comprehensive collection of java libraries for logical aspects of artiﬁcial intelligence and knowledge representation. In KR 14, 2014. [Wagner, 1987] K. W. Wagner. More complicated questions about maxima and minima, and some closures of NP. Theoretical Computer Science, 51:53 80, 1987. [Williams and Sims, 2000] M-A. Williams and A. Sims. SATEN: an object-oriented web-based revision and extraction engine. Co RR, cs.AI/0003059, 2000. [Zhuang et al., 2007] Z. Q. Zhuang, M. Pagnucco, and T. Meyer. Implementing iterated belief change via prime implicates. In AI 07, pages 507 518, 2007.

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)