On the Parameterized Complexity of Belief Revision

1 Introduction

Belief revision [Alchourr´on et al., 1985] is a core formalism of Artificial Intelligence (see e.g. [Peppas, 2008]) aiming for a formal way of adapting one's beliefs in the light of new information. Following Katsuno and Mendelzon [1991], we consider revision in the setting where beliefs and new information are given as propositional formulas. Operators like the one by Satoh [1988] characterize the result of revision by a set of models representing the adapted belief base.

Understanding the computational complexity of reasoning is an indispensable step towards the design of practically efficient systems. Unfortunately, Eiter and Gottlob [1992] have shown that many revision operators suffer from a high computational complexity in the general case of propositional logic. For instance, deciding whether a formula follows from the result of a revision in terms of Satoh's operator has been shown to be ΠP2 -complete. Those results were later strengthened in terms of model checking by Liberatore and Schaerf [2001]. While these two papers studied easier cases in terms of the HORN fragment, other fragments that might lead to tractability have not been thoroughly investigated; a recent analysis [Creignou et al., 2013] for KROM formulas being a notable exception.

∗Supported by the Austrian Science Fund (FWF) under grants P25518, P25521, and Y698, and the German Research Foundation (DFG) under grant ER 738/2-1.

Inspecting these results, it becomes clear that tractability requires rather strong restrictions on the involved formulas, i.e., the knowledge base and the revision formula. On the other hand, these components might be of vastly different size and shape. For exploiting this potential heterogeneity of the two components towards novel tractability results, parameterized complexity and parameterized algorithmics [Downey and Fellows, 1999] are the formal tools of choice. Here the complexity is not measured with respect to the input size alone but also with respect to one or multiple features of the instance that are expressed as an integer value, the socalled parameter. Parameterized complexity has been investigated already in several AI domains (see e.g. [Fellows et al., 2012; Gottlob and Szeider, 2008; Gottlob et al., 2010; Lackner and Pfandler, 2012]) and such results have been successfully put to practice, in particular in the area of argumentation [Dvoˇr´ak et al., 2012; 2014].

In this paper we utilize parameterized complexity theory for belief revision with the aim to keep the restrictions on the theory and new information as independent and relaxed as possible without destroying tractability. Our analysis not only gives new insights on the different sources of complexity of revision, but also provides the basis for novel implementations. We shall focus here on Satoh's operator and start our analysis by generalizing already established tractable cases from [Eiter and Gottlob, 1992] as well as the only fpt result we are aware of, viz. [Pichler et al., 2009] which utilizes the combined treewidth parameter. The main contributions of our work are:

• We generalize existing tractability results due to Eiter and Gottlob [1992] via backdoors to Horn and show certain limits of the treewidth approach, in particular we provide paracoNP-hardness if treewidth is bound independently in the knowledge base T and the revision formula ϕ. Furthermore, also combining bounded treewidth of ϕ with the restriction of T to be Horn results in para-coNP-hardness.
• Towards a generic algorithm, we identify a novel parameter, namely the cardinality of the variables shared by knowledge base T and revision formula ϕ. Our algorithm is fpt when adding (possibly independent) parameters that make T's and ϕ's satisfiability fpt. We show that these additional bounds are necessary, since otherwise completeness for the class FPT NP [f(k)] is obtained. FPT NP [f(k)] contains prob-

lems that can be computed by an fpt-algorithm that may make f(k) many NP oracle calls. From a practical perspective, this result is interesting since it shows that the problem at hand can by implemented via an iterative SAT-procedure.

• Finally, we show that a relaxation of the bound on the shared vocabulary to a bound on the maximum symmetric distance between models of T and ϕ is less promising since this increases the complexity to para-ΘP2 -hardness.

2 Background

Propositional Logic. We consider propositional logic over some fixed universe U of propositional atoms and standard connectives ∨, ∧, and ¬. A literal is an atom a or a negated atom ¬a. A clause is a set of literals. A clause is called Horn if at most one of its literals is positive. Unless otherwise stated, formulas are in conjunctive normal form (CNF). For formula ϕ we denote the set of its clauses by C(ϕ) and its set of atoms by var (ϕ). A formula is called Horn if all of its clauses are Horn. We denote by HORN the class of Horn formulas. We represent an interpretation by a set I ⊆ U containing all variables set to true. If interpretation I satisfies formula ϕ, we call I a model of ϕ, denoted by I |= ϕ. By Mod(ϕ) we denote the set of models of ϕ (over U). For formulas ϕ and ψ we denote by ϕ |= ψ that Mod(ϕ) ⊆ Mod(ψ). A truth assignment τ for a set V ⊆ U is a function that assigns a truth value to each variable in V . We denote by ϕ[τ ] the formula obtained from formula ϕ by deleting all clauses satisfied by τ and by deleting all literals that are set to false by τ from the remaining clauses.

Belief Revision. The problem of belief revision is specified as follows: Given a knowledge base (i.e., a formula) T and a formula ϕ, find a revised knowledge base T ◦ ϕ, such that ϕ is true in all models of T ◦ ϕ and the change compared to the models of T is "minimal". Note that T, ϕ and ψ are throughout the paper assumed to represent theory, revision formula and query formula. The approach to belief revision we deal with in this paper relies on a so-called model-based operator. Such operators usually utilize a model distance M∆M ′ = (M \ M ′ ) ∪ (M ′ \ M) which yields the set of atoms differently assigned in interpretations M and M ′ . Assuming that T is consistent (we tacitly make this assumption throughout the paper), the operator due to Satoh [1988] can be defined as follows: Mod(T ◦ ϕ) = {J ∈ Mod(ϕ) | ∃I ∈ Mod(T) s.t. I∆J ∈ ∆min (T, ϕ)}, ∆min (T, ϕ) = min⊆{I∆J | I ∈ Mod(T), J ∈ Mod(ϕ)}, with min⊆ selecting minimal elements with respect to set inclusion. The decision problem BR is ΠP2 -complete even in case ψ is a single atom [Eiter and Gottlob, 1992].

Parameterized Complexity. Recall that FPT denotes the class of parameterized problems for which there exists an algorithm that decides the problem in time f(k) ·nO(1) , where f(·) is an arbitrary computable function that only depends on the parameter k. A parameterized reduction of a parameterized problemΠ to a parameterized problemΠ′ is an fpt algorithm that transforms an instance (I, k) of Π to an instance (I ′ , k′ ) of Π′ such that: (i) (I, k) is a yes-instance of Π if and only if (I ′ , k′ ) is a yes-instance of Π′ , and (ii) k′ = g(k), where g(·) is an arbitrary computable function that only depends on k. Hardness and completeness with respect to parameterized complexity classes is defined analogously to the concepts from classical complexity theory, using parameterized reductions. The following parameterized classes will be needed in this paper: FPT ⊆ co-W[1] ⊆ para-coNP ⊆ FPT NP [f(k)] ⊆ para-ΘP2 . The class co-W[1] is the co-class of W[1], the first level of the so-called W-hierarchy. A prominent complete problem for W[1] is the INDEPENDENT SET problem parameterized by the size of the required independent set [Downey and Fellows, 1995]. Hence its co-problem is complete for co-W[1]. Parameterized problems in the W-hierarchy share the property that they can be solved in polynomial time if the parameter value is fixed to a constant. On the other hand para-coNP and para-ΘP2 contain those parameterized problems that can be reduced via a parameterized reduction to a coNP-complete or ΘP2 -complete problem respectively. The class FPT NP [f(k)] was recently introduced by de Haan and Szeider [2014b] and contains all problems that can be solved by an fpt-algorithm that can use f(k) many calls to an NP oracle [de Haan and Szeider, 2014a]. Two important parameters that we use in this paper are treewidth (see e.g. [Bodlaender, 1993]) and backdoors (see e.g. [Gaspers and Szeider, 2012]).

Treewidth and Backdoors. A tree decomposition of a graph G = (V, E) is a pair (H, χ), where H is a tree and χ maps each node t of H (we use t ∈ H as a shorthand below) to a bag χ(t) ⊆ V , such that (i) for each v ∈ V , there is an t ∈ H, s.t. v ∈ χ(t); (ii) for each {v,w} ∈ E, there is an t ∈ H, s.t. {v,w} ⊆ χ(t); and (iii) for each t1, t2, t3 ∈ H, s.t. t2 lies on the path from t1 to t3, χ(t1) ∩ χ(t3) ⊆ χ(t2) holds. The width of a tree decomposition is defined as the cardinality of its largest bag χ(t) minus one. The treewidth of a graph G, denoted as tw(G), is the minimum width over all tree decompositions of G. To build tree decompositions for propositional formulas, we use their incidence graphs. For formula χ such a graph consists of a vertex for each clause and each variable occurring in χ, and has as edges all unordered pairs {x, c} where x ∈ var (χ) appears in clause c ∈ C(χ).

A strong HORN-backdoor set of a propositional formula χ is a set B of variables such that χ[τ ] ∈ HORN for each truth assignment τ over the variables B. This means, the cardinality of such a HORN-backdoor set measures the "distance" of χ to the class of HORN formulas. We denote with B(χ) the smallest HORN-backdoor set of χ.

3 Horn, Treewidth and Beyond

We start with an fpt-result for the setting where |var (ϕ)| is considered as the parameter and where T is HORN. Actually, this result is implicit in the proof of [Eiter and Gottlob, 1992, Theorem 8.3], where a polynomial time result was shown if the length of ϕ is bounded by a constant.

Proposition 1. (implicit in [Eiter and Gottlob, 1992, Theorem 8.3]) BR parameterized by |var (ϕ)| is fpt if T ∈ HORN.

A successful technique to generalize tractability results is to move from the restrictions to HORN formulas (or other tractable fragments of SAT) to the backdoor approach and use, e.g., strong HORN-backdoor sets. Using this formalism it is possible to generalize the result of Proposition 1 from the restriction to HORN formulas to propositional formulas which are close to being HORN and hence have a small backdoor.

Theorem 2. BR parameterized by |B(T)| + |var (ϕ)| is fpt.

Proof. Let B be a strong HORN-backdoor set of T . The basic idea is to iterate over all (2|B| many) assignments τ to B and to simplify T accordingly. Since T[τ] ∈ HORN, checking whether (T [τ ] ◦ ϕ) |= ψ holds is in FPT by Theorem 1.

Notice that this result does not hold if BR is parameterized by |B(T)| only. In fact, BR remains coNP-complete if T, ϕ ∈ HORN [Eiter and Gottlob, 1992, Theorem 7.2], which also immediately yields para-coNP-hardness. Another important structural parameter is the combined treewidth of T , ϕ, and ψ.

Proposition 3. [Pichler et al., 2009, Theorem 1] BR is fpt when parameterized by tw(T ∧ ϕ ∧ ψ).

These initial fpt results possess quite strong conditions on T and ϕ. As we will see in the next section, the key to gain more versatile fpt results is to parameterize on joint properties of T and ϕ. Before that, we show that further independent relaxations on T and ϕ indeed increase complexity. Our first result in this direction is concerned with the situation when treewidth of T as well as of ϕ are bound individually. Then, we study the case of bound treewidth on ϕ where T is HORN.

Theorem 4. BR is para-coNP-hard if parameterized by tw(T ) + tw(ϕ).

Proof. We show coNP-hardness for the acyclic case, i.e., tw(T) = tw(ϕ) = 1 via reduction from the SAT problem. There we are given a formula χ in CNF and have to decide whether χ is satisfiable. Given an instance of SAT χ = c1 ∧ c2 ∧ · · · ∧ cm where c1, . . . , cm are clauses, we construct an instance (T, ϕ, ψ) of BR as follows. Let var (χ) = V . We create 2m new copies of the set V , denoted by V1, . . . , Vm and V ′ 1 , . . . , V ′m. For variable x ∈ V we denote the i-th copy by xi and the i-th copy of its primed version by x′i . Additionally, let r be a new propositional variable. For clause ci of χ we replace its variables with their i-th copy and add the literal ¬r. We call the resulting clause γi, e.g., for c2 = (x ∨ ¬y ∨ z), γ2 = (x2 ∨ ¬y2 ∨ z2 ∨ ¬r). Then T = (γ1 ∧ γ2 ∧ · · · ∧ γm) ∧ ∧x∈V ∧1≤i≤m(xi → x′i ), ϕ = ∧x∈V ∧1≤i≤m(x′i → x) ∧ (x → xi), and ψ = ¬r. Note that the incidence graphs of T and ϕ are acyclic.

Next, we show the correctness of the reduction. Assume that χ is a yes-instance, i.e., there exists M ∈ Mod(χ). We construct an interpretation M ′ , which is a model of T and ϕ. For all x ∈ V and all 1 ≤ i ≤ m we assign x ∈ M ′ iff xi ∈M ′ iff x′i ∈M ′ iff x ∈M. Additionally, r ∈M ′ . Since M satisfies all clauses ci, it holds that M ′ satisfies all clauses γi. The additional implication clauses in T and ϕ are satisfied byM ′ since all the different copies of the same variable agree on the truth value. Hence, M ′ is indeed a model of T and of ϕ.

Therefore, M ′ ∈ Mod(T ◦ ϕ). But since r ∈ M ′ , it follows that Mod(T ◦ ϕ) ̸|= ¬r. Hence, (T, ϕ, ψ) is a no-instance.

For the other direction, assume that (T, ϕ, ψ) is a noinstance, i.e., there exists a model M ∈ Mod(T ◦ ϕ) with r ∈ M. First we show that M is a model of T ∧ϕ. To this end, we show that there is an interpretation M ∗ , which is a model of T ∧ ϕ. This immediately yields ∆min (T, ϕ) = {∅}. We construct the interpretationM ∗ as follows: Let r ̸∈ M ∗ and for all x ∈ V and all 1 ≤ i ≤ m we assign x ∈ M ∗ iff xi ∈ M ∗ iff x′i ∈ M ∗ . The latter part ensures that all implication clauses in T and ϕ are satisfied. Since r ̸∈M ∗ , it follows that M ∗ trivially satisfies all clauses γi, 1 ≤ i ≤ m. Hence, M ∗ is indeed a model of T ∧ ϕ and we have ∆min (T, ϕ) = {∅}. Therefore, we know that M is a model of T ∧ ϕ, since M ∈ Mod(T ◦ ϕ) holds by assumption. Next we construct the interpretation M ′ = M ∩ V and show that M ′ is a model of χ. Since r ∈ M and each clause γi is satisfied by M, there is a literal from Vi in γi that is true in M. By construction, x ∈ M iff xi ∈ M and hence x satisfies also clause ci in M ′ . Since this holds for all clauses c1, . . . , cm, interpretationM ′ is indeed a model of χ and χ is a yes-instance.

Theorem 5. BR is para-coNP-hard if parameterized by tw(ϕ) even if T ∈ HORN.

Proof. Actually, we show coNP-hardness in the case where ϕ is acyclic, i.e., tw(ϕ) = 1. We give a reduction from the co-problem of the NP-complete INDEPENDENT SET problem.

Let an instance of INDEPENDENT SET be given by G = (V, E) and k > 0. The question is, whether there exists a set of exactly k vertices V ′ ⊆ V such that there exists no edge between vertices in V ′ . Let V = {v1, . . . , vm}. By slight abuse of notation we use the vertices of G also as propositional variables. Thus, we fix the set of variables var (T ∪ ϕ) = {r, v1, . . . , vm} ∪ {v1 1 , . . . , v1m, . . . , vk 1 , . . . , vkm}, where for 1 ≤ i ≤ m the variables v1 i , . . . , vk i are k new copies of the variable vi and r is a new variable.

Similar to the proof of [Lackner and Pfandler, 2012, Theorem 14] we make use of the following subformulas to encode the INDEPENDENT SET problem. The crucial difference in this proof is the distribution of the subformulas to T and ϕ. We define χIS = ∧{vi,vj}∈E (¬vi ∨¬vj ), χ1 = ∧1≤l≤k (vl1 ∨ · · · ∨ vlm), χ2 = ∧1≤i≤m ∧1≤l<l′≤k (¬vl i ∨ ¬vl′ i ), and χ3 = ∧1≤i≤m ∧1≤l≤k (vl i → vi).

The role of χIS is to permit only interpretations over {v1, . . . , vm} that correspond to an independent set in G. Formula χ1 ensures that for each copy l with 1 ≤ l ≤ k there is an index i with 1 ≤ i ≤ m representing a vertex that is added to the independent set. In formula χ2 it is ensured that at most one copy of each vertex can be set to true. Finally, in formula χ3 the copies vl i are mapped back to the original vertices vi in order to represent the independent set candidate.

The important step is now to distribute these subformulas as follows. In order to construct a BR instance (T, ϕ, ψ) we set T = r → (χIS ∧ χ2 ∧ χ3), ϕ = χ1, and ψ = ¬r. Notice that T can be transformed into CNF by adding the literal ¬r to each clause of χIS∧χ2∧χ3. Observe that T ∈ HORN and tw(ϕ) = 1, since each variable in var (ϕ) occurs only once in ϕ.

For the correctness we show that there is a model M ∈ Mod(T ◦ ϕ) with r ∈ M (i.e., (T, ϕ, ψ) is a no-instance) iff G has an independent set of size k (i.e., yes-instance of INDEPENDENT SET). To this end, consider the models in Mod(T), of which there are two types. The first type t1 contains the models M with r ̸∈ M, whereas the second type t2 contains models M ′ such that r ∈M ′ andM ′ |= χIS ∧χ2 ∧χ3.

Assume there is w.l.o.g. an independent set I ⊆ V with I = {v1, . . . vk} (of size exactly k). Then, due to construction of the subformulas χIS, χ1, χ3, χ3, we can construct a model M such that v ∈ M for all v ∈ {r, v1, . . . , vk, v1 1 , . . . , vk k }, whereas all other variables are set to false. One can verify that M is also model of T ∧ϕ and that M is of type t2. Notice that the first property yields that ∆min (T, ϕ) = {∅} and hence M ∈ Mod(T ◦ ϕ) whereas the second property yields r ∈ M.

For the reverse direction assume that there is a model M ∗ ∈ Mod(T ◦ ϕ) with r ∈ M ∗ . Observe that for all models M ∈ Mod(ϕ) with r ̸∈ M it holds that M ∈ Mod(T ). Hence, we have ∆min (T, ϕ) = {∅}. Combining this with the assumption that M ∗ ∈ Mod(T ◦ ϕ) it follows that M ∗ |= T. But since r ∈M ∗ , i.e. it is of type t2, we know thatM ∗ |= χIS∧χ2∧χ3. FromM ∗ |= ϕ it follows that M ∗ |= χ1. Since the models of formula χIS ∧ χ1 ∧ χ2 ∧ χ3 correspond to independent sets of G of size k [Lackner and Pfandler, 2012, Theorem 14], it follows that V ∩M ∗ is an independent set of G of size k.

With help of the construction used in the proof of Theorem 5, we obtain the following result where the number of clauses in ϕ, |C(ϕ)|, is used as a parameter.

Corollary 6. BR is co-W[1]-hard if parameterized by |C(ϕ)| even if T ∈ HORN.

Proof. We reduce from the co-problem of INDEPENDENT SET parameterized by the size of the independent set k, which is co-W[1]-complete. In the construction used in the proof of Theorem 5, |C(ϕ)| is bounded by k. Therefore, the reduction is an fpt-reduction, which yields the result.

4 Shared Variables

If we take a closer look at the constructions used in the proofs of Theorem 4 and 5, we realize that the number of shared variables, i.e., |var (T) ∩ var (ϕ)|, is unbounded. As it turns out in our next result, using these shared variables as parameter yields a versatile fpt-result.

Theorem 7. Let S = var (T) ∩ var (ϕ) and let pT and pϕ be parameters such that for any assignment τ to S ∪ var (ψ) the SAT problem of T [τ ] and ϕ[τ ], respectively, can be decided by an fpt-algorithm. Then BR parameterized by |S| +pT +pϕ is fpt for queries ψ of constant size.

Proof. The postulated algorithm is Algorithm 1. Intuitively, this algorithm computes first all partial models on the shared variables. The crucial observation is that the symmetric set difference of models of T and ϕ is restricted to shared variables. Hence, it suffices to restrict the expensive minimality check to those partial models.

We now show the correctness of this algorithm. We claim that MT after line 5 contains all truth assignments τ to the variables in S and ψ such that τ can be extended to a model of T .

Similarly, the set Mϕ after line 5 contains all truth assignments τ to the variables in S and ψ such that τ can be extended to a model of ϕ. To this end, note that line 2 enumerates all subsets of the variables in S and ψ. Line 3 extends such a subset to a truth assignment. In lines 4-5 we test if this truth assignment can be extended to a model of T and ϕ respectively, and if this is true, we store the assignment inMT andMϕ respectively. Next, we want to compute ∆min (T, ϕ) = min⊆({I∆J | I ∈ Mod(T), J ∈ Mod(ϕ)}). We claim that for the set D in line 6 it holds that D = {X ∪ ¬X | X ∈ ∆min (T, ϕ)}, where ¬X = {¬x | x ∈ X}. Note that the first difference between line 6 and the definition of ∆min (T, ϕ) is that we consider the symmetric set difference between assignments (containing positive and negative literals) instead of models (containing positive literals only). But this does not change the correctness, since models I and J disagree on variable x iff the corresponding assignments I and J disagree on literals x and ¬x. The second difference between line 6 and the definition of ∆min (T, ϕ) is that we consider only assignments over the variables of S and var (ψ) instead of assignments over all variables. To see that this does not change the correctness, consider a arbitrary set δ ∈ ∆min (T, ϕ). We will show that var (δ) ⊆ S. Assume towards a contradiction that this does not hold, i.e., there exists a variable x ∈ var (δ) with x ∈ var (T ) (the case x ∈ var (ϕ) is symmetric) and x ̸∈ S. By definition there exists I ∈ Mod(T ) and J ∈ Mod(ϕ) such that I∆J = δ. Since x ∈ δ we know that I and J do not agree on the truth value of x. But since x ̸∈ ϕ there exists J ′ ∈ Mod(ϕ) which differs from J only in the truth value of x. Note that the resulting symmetric set difference I∆J ′ is strictly smaller than δ, violating that δ ∈ ∆min (T, ϕ). Hence, indeed var (δ) ⊆ S and it is enough to compute the symmetric set differences over assignments over variables that contain at least all variables of S. Next, if we compare line 7 with the definition of Mod(T ◦ϕ) = {J ∈ Mod(ϕ) | ∃I ∈ Mod(T) s.t. I∆J ∈ ∆min (T, ϕ)}, we can observe two differences. First, we get again a set of assignments instead of a set of models (containing positive literals only). Second, the resulting assignments are restricted to the variables in S and var (ψ). Formally, we have the relation R = {(J ∩ (S ∪ var (ψ))) ∪ ⋃x∈J∩(S∪var (ψ)) ¬x | J ∈ Mod(T ◦ ϕ)}. Finally, we have to check T ◦ ϕ |= ψ. This means we go over each model of T ◦ ϕ and check if any of these models does not satisfy ψ (lines 8-9). Note that it is indeed enough to go over assignments I ∈ R since the truth value of all variables in var (ψ) is fixed in these assignments.

For the complexity, note that the loop in line 2 is executed 2|S∪var (ψ)| times. Since the two SAT calls can be executed by an fpt-algorithm with respect to parameters pT and pϕ, we get an overall time for this loop of O∗ (2|S∪var (ψ)| (f(pT ) + g(pϕ))), where f and g are computable functions only depending on pT and pϕ, respectively. Furthermore, the size of MT and Mϕ after line 5 is bounded by 2|S∪var (ψ)| as well. Therefore, fpt for |S|, pT and pϕ follows.

Observe that the above result actually gives a family of fptresults for BR with the parameter "number of shared variables" in common. In addition, since the revision formula ϕ usually does not contribute new knowledge to all parts of the theory,

Input: Formulas T, ϕ and ψ. Output: Decision whether T ◦ ϕ |= ψ holds. 1 MT = ∅, Mϕ = ∅ 2 foreach J ∈ 2S∪var (ψ) do 3 I = J ∪ ⋃x∈(S∪var (ψ))\J ¬x 4 if T[I] is satisfiable thenMT =MT ∪ {I} 5 if ϕ[I] is satisfiable then Mϕ = Mϕ ∪ {I} 6 D =min⊆({I∆J | I ∈MT , J ∈Mϕ}) 7 R = {J ∈Mϕ | ∃I ∈MT s.t. I∆J ∈ D} 8 foreach I ∈ R do 9 if I ̸|= ψ then return no 10 return yes

but rather introduces new information on a certain subject, one can hope that the number of shared variables is rather small even if theory T is large. The advantage of this result is that it becomes possible to combine any tractable fragments that make that satisfiability problem for T and ϕ fpt. Furthermore, notice that the choice of pT and pϕ is completely independent. This yields a modular approach that can be instantiated with any reasonable combination of tractable fragments. For example, we obtain an fpt-result where we decouple the treewidth of T from the treewidth of ϕ if we additionally parameterize by |var (T) ∩ var (ϕ)|. Compared to the hardness result in Theorem 4 we see that the number of shared variables is the essential parameter to obtain the fpt-result.

Although parameterizing by the number of shared variables provides an important bridge towards tractability, considering this parameter in isolation does not yield an fpt result.

Theorem 8. BR is FPT NP [f(k)]-complete if parameterized by |S|, where S = var (T ) ∩ var (ϕ).

Proof. We start by showing membership in FPT NP [f(k)]. Let (T, ϕ, ψ) be an arbitrary instance of BR with var (T) ∩ var (ϕ) = S and k = |S|. As discussed in the proof of Theorem 7, ∆min (T, ϕ) is restricted to variables in S. Hence, an upper bound for the number of minimal symmetric differences is given by ∣∣∆min (T, ϕ)∣∣ ≤ 2k . We can test for each symmetric difference Z with a single NP oracle call if (i) it is minimal, or (ii) whether there exist models M and M ′ such that M |= T, M ′ |= ϕwithM∆M ′ = Z andM ′ ̸|= ψ. Thus, we can decide whether T ◦ ϕ |= ψ holds by invoking O(2k ) calls to an NP oracle.

We prove hardness via reduction from the FPT NP [f(k)]- complete problem BH(LEVEL)-SAT [de Haan and Szeider, 2014a] with parameter k, s.t. the constructed instance (T, ϕ, ψ) satisfies |S| ≤ k. We recall first the definition of the unparameterized problem BHn-SAT. An instance of this problem is given by I = (χ1, . . . , χn), where each χi is a formula. If n = 1, then I is a yes-instance iff χ1 is satisfiable. If n ≥ 2 is odd then I is a yes-instance iff χn is satisfiable or (χ1, . . . , χn-1) is a yes-instance of BHn-1-SAT. Otherwise, if n ≥ 2 is even then I is a yes-instance iff χn is unsatisfiable and (χ1, . . . , χn-1) is a yes-instance of BHn-1-SAT. A problem instance of the parameterized problem BH(LEVEL)-SAT

is now such a sequence I = (χ1, . . . , χk) with parameter k, and we ask whether I is a yes instance of BHk-SAT.

Let now I = (χ1, . . . , χk) be an arbitrary instance of BH(LEVEL)-SAT. W.l.o.g. we assume disjoint vocabularies for each pair of formulas. We define T = ∧1≤i≤k qi and ϕ = (r(I) → q) ∧ ∧1≤i≤k (qi → χi) where q and the qis are fresh variables, and r(·) is a recursive function. If k = 1, then r(I) = q1. If k ≥ 2 is odd, then r(I) = (qk ∨ (r(χ1, . . . , χk-1))). If k ≥ 2 is even, then r(I) = (¬qk ∧ (r(χ1, . . . , χk-1))). We can transform ϕ straightforwardly to CNF. Finally let ψ = q.

We show that (T, ϕ, ψ) is a yes-instance of BR iff I is a yes-instance of BH(LEVEL)-SAT. First, consider the two cases for each χi: (i) χi is unsatisfiable, or (ii) χi is satisfiable. If χi is unsatisfiable, then (qi → χi) ≡ ¬qi. Thus, for all M ∈ Mod(T ◦ ϕ) we have qi /∈ M. If χi is satisfiable, then there is a model Mi |= χi. Now suppose that there is a model M ∈ Mod(T ◦ ϕ), s.t. qi /∈ M. It follows that for an MT |= T we have MT∆M ∈ ∆min (T, ϕ). Let M ′ = (M \ var (χi)) ∪ (Mi ∩ var (χi)) ∪ {qi, q}. Clearly, M ′ |= (qi → χi) and M ′ |= (r(I) → q) and thus M ′ |= ϕ. Define the following model of T: M ′T = M ′ ∪ {qj | 1 ≤ j ≤ k}. It is straightforward to see that both M ′∆M ′T and M∆MT are subsets of the shared variables {qj | χj ∈ I}. We can conclude that M ′∆M ′T ⊂ M∆MT (they differ only in qi, since qi ∈ MT ), contradicting that M ∈ Mod(T ◦ ϕ).

It follows that ∆min (T, ϕ) = {{qi | χi unsatisfiable }}. If I is a yes-instance of BH(LEVEL)-SAT, we can derive that for an M ∈ Mod(T ◦ϕ) it holds that M |= r(I), and thus q ∈ M and M |= ψ. If (T, ϕ, ψ) is a yes-instance of BR, then all models M ∈ Mod(T ◦ ϕ) satisfy ψ = q, and thus M |= r(I). This implies that I is a yes-instance of BH(LEVEL)-SAT.

5 MaximumHamming Distance

Finally, we investigate a further natural relaxation for capturing distance between T and ϕ. Define the maximum Hamming distance between T and ϕ as |∆|max (T, ϕ) = max({|(I∆J) ∩S| | I ∈ Mod(T), J ∈ Mod(ϕ)}), where S = var (T) ∩ var (ϕ). In words, |∆|max (T, ϕ) delivers the maximum number of shared variables that are assigned differently in a model of T and a model of ϕ. Bounding S implies a bound on |∆|max (T, ϕ). However, parameter |∆|max (T, ϕ) is not enough for membership in FPT NP [f(k)].

Theorem 9. BR is para-ΘP2 -hard if parameterized by maximum Hamming distance.

Proof. We use a reduction from the ΘP2 -complete problem UOCSAT [Kadin, 1989] such that the constructed instance has a maximum Hamming distance of 5. Let Γ = c1 ∧ · · · ∧cn be an arbitrary instance of UOCSAT, where Γ is a formula in CNF with clauses c1, . . . , cn. Γ is a yes-instance of UOCSAT if it is the case that for all interpretations satisfying a maximum number of clauses of Γ it holds that they satisfy the same clauses. For the reduction we utilize encodings for cardinality constraints. In particular we use so-called at-most constraints, atMost(i,X), which evaluate to true under an interpretation M iff |M ∩X| ≤ i. Furthermore, exact(i,X) states that exactly i variables are assigned to true. One can construct formulas for such constraints which are polynomial in size (see [Roussel and Manquinho, 2009, Section 22.2.3.]).

For our reduction, we introduce three sets of variables: L = {li | 1 ≤ i ≤ n}, R = {ri | 0 ≤ i ≤ n}, and A = {ai | 0 ≤ i ≤ n}. We translate the given formula to Γ∗ = (l1 ∨ c1) ∧ · · · ∧ (ln ∨ cn). One of the main subformulas for the reduction is χ = Γ∗ ∧ ∧ri∈R(ri ↔ exact(i, L)). That is, it contains the instrumented original formula with the fresh literals lj and variables ri such that any model of χ assigns ri to true iff i variables from L are assigned to true. A basic observation is that, if M |= χ then there is an i with 0 ≤ i ≤ n such that M |= ri and for j ̸= i it holds that M ̸|= rj. In addition, M satisfies at least n - i clauses of Γ. The formula χ can be transformed to an equivalent formula in CNF. The problematic conjuncts are (ri ↔ exact (i, L)). We can change these to (ri → exact(i,L)), which can be transformed to CNF in polynomial time, and add further clauses to ensure that exactly one ri is true in a model of χ. All the formulas in the sequel of this proof can be easily transformed to CNF, but for the sake of readability we will use non-CNF formulas.

Construct ϕ = χ ∧ χ′ ∧ ((α → β) → q) ∧ ∧ai∈A(ri ↔ ai) with α = (∧ri∈R ri ↔ r′i ), β = (∧li∈L li ↔ l′i ), and q as a fresh variable. Within this proof if G is a formula, then we denote by G′ the formula obtained by uniformly renaming all atoms with a prime. Define T = (∧ai∈A ¬ai) ∧ atMost(1, R′ ) ∧ R′ < R ∧ exact(1, R), where R′ < R = ∧r′j ∈R′ (r′j → (∨j<i ri)). To finish our instance let ψ = q.

We now state some properties of the instance (T, ϕ, ψ). The instance can be computed in polynomial time w.r.t. Γ. All three formulas are satisfiable. It holds that |∆|max (T, ϕ) ≤ 5, since the shared vocabulary is A∪R∪R′ and all models of ϕ may assign only one variable per set to true, while all models of T may assign at most one variable of R′ to true and exactly one variable of R to true (and none of A). Further, it cannot be the case that both ri and r′i are in a model of T . It cannot be the case that ∅ ∈ ∆min (T, ϕ). For each D ∈ ∆min (T, ϕ) it holds that ai ∈ D for some 0 ≤ i ≤ n. For two models Mϕ, MT s.t. Mϕ |= ϕ and MT |= T we have {ai} = Mϕ∆MT only if {ri, r′j } ⊆ Mϕ for some j < i. A last crucial observation is that if Mϕ |= ϕ and {ri, r′i} ⊆ Mϕ, then there is a model MT |= T such that Mϕ∆MT = {ai, r′i}, and there is no M ′T such that M ′T |= T and Mϕ∆M ′T ⊂ Mϕ∆MT (the set {ai, r′i} is a minimal symmetric difference we can achieve).

Let n - d be the maximum number of clauses of Γ that can be simultaneously satisfied. Further let M1,M2 be two interpretations such that M1 |= ϕ with M1 |= rd ∧ r′d and M2 |= ϕ with M2 |= rd1 ∧ r′d1 such that d < d1. We show that (i) M1 ∈ Mod(T ◦ ϕ), and (ii) M2 /∈ Mod(T ◦ ϕ). For (i), we first show that there is no Mϕ such that Mϕ |= ϕ and {rd, r′j , ad} ⊆ Mϕ for j < d. Suppose to the contrary that such an Mϕ exists. Then Mϕ satisfies n - j clauses of Γ′ where n - j > n - d. This is a contradiction to n - d being the maximum number of clauses simultaneously satisfiable for Γ. By the observations above, we know that {ad, r′d } is a minimal symmetric difference we can find for M1 when comparing it to all models of T . We now show that there are no Mϕ |= ϕ and MT |= T such that Mϕ∆MT ⊂ {ad, r′d }. Due to the observations above, we cannot find such models such that the symmetric difference is a proper subset and does not contain ad. To achieve the symmetric difference of {ad} we would need a model of ϕ that assigns rd and r′j to true for some j < d. This is a contradiction. Thus M1 ∈ Mod(T ◦ ϕ). The second case (ii) follows analogously, just note that we can find in this case a model of ϕ and model of T such that the symmetric difference contains only ad1 . It follows that {M ∈ Mod(T ◦ϕ) | M |= α}∩var (Γ) = {M ′ | M ′ satisfies a maximum number of clauses of Γ} ∩ var (Γ).

We now show that (T, ϕ, ψ) is a yes-instance of BR iff Γ is a yes-instance of UOCSAT. Assume Γ is a yes-instance of UOCSAT. This implies that if an M ∈ Mod(T ◦ ϕ) satisfies α (M |= α) it holds that M |= β (otherwise M would encode two different interpretations of Γ satisfying a maximum number of clauses, but satisfying different clause sets). Thus M |= ψ. The other direction can be shown analogously: if two models satisfying a maximum number of clauses for Γ exist, s.t. they satisfy different clauses, then there is an M ∈ Mod(T ◦ ϕ), s.t. M |= α, M ̸|= β, and q /∈ M.

We complement this result by an upper bound on the required number of calls to a SAT-solver in order to solve the problem. The number of possible symmetric differences projected to the shared variables S is bounded by ∑di=0 (|S| i ), with d the maximum Hamming distance. We can bound this by ∑di=0 (|S| i ) ≤ (1 + |S|)d . Thus, we can bound the number of required NP oracle calls by O((1 + |S|)d ).

6 Discussion

In this work we have studied the parameterized complexity of belief revision for parameters beyond treewidth. We summarize our results in Table 1. In particular, we have explored to what extend it is possible to decouple the theory from the revision formula. The parameter "shared variables" turned out to be crucial to obtain fpt-results in the decoupled setting. Ultimately, this parameter led to a versatile, modular fpt-result where tractable fragments of the theory and the revision formula can be combined arbitrarily. Moreover, if we do not rely on tractable fragments the problem becomes complete for the recently introduced class FPT NP [f(k)]. This result is interesting as it adds a natural problem to this rather unexplored class, and, furthermore, it shows the applicability of a SAT-based procedure that can solve the problem with a restricted number of calls if the parameter is bounded. Our result also complements the work of Delgrande et al. [2007], who presented algorithms and implementations based on SAT-solvers for belief change problems, and provides further evidence that the usage of such solvers is a promising and interesting direction for devising systems in the area of belief revision.

We envisage the study of further belief revision operators, such as Dalal's operator [Dalal, 1988], in a parameterized setting. For other operators, the results might be very different as the computational complexity is heavily influenced by the choice of the operator (cf. [Creignou et al., 2013]). Furthermore, we want to investigate to what extend the shared variables are key towards tractability for other belief change formalisms, like belief merging, contraction, or update.