Computer Science
Computer Science-2021.gz:143150
Computer Science
4e73df3cd5505b6686f9464b40679eeed42619a0
Parameterised Complexity of Propositional Inclusion and Independence Logic

In this work we analyse the parameterised complexity of propositional inclusion (PINC) and independence logic (PIND). The problems of interest are model checking (MC) and satisfiability (SAT). The complexity of these problems is well understood in the classical (non-parameterised) setting. Mahmood and Meier (FoIKS 2020) recently studied the parameterised complexity of propositional dependence logic (PDL). As a continuation of their work, we classify inclusion and independence logic and thereby come closer to completing the picture with respect to the parametrised complexity for the three most studied logics in the propositional team semantics setting. We present results for each problem with respect to 8 different parameterisations. It turns out that for a team-based logic L such that L-atoms can be evaluated in polynomial time, then MC parameterised by teamsize is FPT. As a corollary, we get an FPT membership under the following parameterisations: formula-size, formula-depth, treewidth, and number of variables. The parameter teamsize shows interesting behavior for SAT. For PINC, the parameter teamsize is not meaningful, whereas for PDL and PIND the satisfiability is paraNP-complete. Finally, we prove that when parameterised by arity, both MC and SAT are paraNP-complete for each of the considered logics.


Introduction
The research program on logics with team semantics was conceived in the early 2000s as a systematic study of semantical frameworks in which different notions of dependence between variables could be modelled and studied in a unified setting. Soon after the introduction of first-order dependence logic [27], the framework was extended to cover also propositional and modal logic [28]. In this context, a significant step forward was taken in [5], where the focus was shifted to study dependencies between formulae instead of just propositional variables. The framework of team semantics has proven to be remarkably malleable. During the past decade the framework has been re-adapted for the needs of an array of disciplines. In addition to the modal variant, team semantics has been generalized to temporal [18] and probabilistic [4] frameworks, and fascinating connections to fields such as database theory [11], statistics [1], real valued computation [9], verification [19], and quantum information theory [17] have been identified.
Boolean satisfiability problem (SAT) and quantified Boolean formula problem (QBF) have had widespread influence in diverse research communities. In particular QBF solving techniques are important in application domains such as planning, program synthesis and verification, adversary games, and nonmonotonic reasoning, to name a few [26]. Further generalizations of QBF are the dependency quantified Boolean formula problem (DQBF) and alternating DQBF which allow richer forms of variable dependence [10,23,24]. Propositional logics with team semantics offer a fresh perspective to study enrichments of SAT and QBF. Indeed, the so-called propositional dependence logic is known to coincide with DQBF, whereas quantified propositional logics with team semantics have a close connection to alternating DQBF [10,29].
Propositional dependency logics extend propositional logic with new atomic dependency statements that describe different forms of variable dependence; the most well studied of which are functional dependence, inclusion dependence, and independence. Formulae of these logics are evaluated over propositional teams (i.e, sets of propositional assignments with common variable domain). The dependence atom =(x; y) is satisfied in a team T if for each pair s, t ∈ T of assignments, s(x) = t(x) implies s(y) = t(y). That is, every pair of assignments that fixes every variable in x, also fixes every variable in y. Likewise the inclusion dependency x ⊆ y holds in T , if ∀s ∈ T ∃t ∈ T such that s(x) = t(y). Finally, an independence atom x⊥ z y is true in T if ∀t, t ′ ∈ T such that t(z) = t ′ (z), T contains an assignment t ′′ such that t ′′ (xzy) = t(xz)t ′ (y). The extension of propositional logic with dependence (=(x; y)), inclusion (x ⊆ y) and independence atoms (x⊥ z y) yield propositional dependence (PDL), inclusion (PIN C), and independence (PIN D) logics, respectively. Example 1. We illustrate an example from relational databases to provide understanding of various dependency atoms. In the propositional logic setting, datavalues can be represented as bit strings of appropriate length. Parameters discussed in this paper correspond to values in the propositional setting. This means there is no need to consider the blow-up observed during the binary encoding. The set of records in Table 1 corresponds to a team T . Then T satisfies the functional dependency =({Room, Time}; {Course}), and the inclusion dependency Responsible ⊆ Instructor. However, T violates the functional dependency =({Room, Time}; {Instructor}) as witnessed by tuples (Juha, 10, C.30, Bio-LAB, Jonni) and (Jonni, 10, C.30, Bio-LAB, Jonni). Lastly, T also violates the independence (multivalued dependency) Instructor⊥ Course Time as witnessed by tuples (Antti, 11.00, A10, Biochemistry, Juha) and (Juha, 13.00, A10, Biochemistry, Juha). The focus of the current paper is on the parametrized complexity of logics in the propositional team semantics setting. The complexity landscape of the classical (non-parametrized) decision problems -satisfiability, validity, and model checking -is well mapped in the propositional and modal team semantics setting (see [15, page 627] for an overview). In this paper, we present a more fine grained analysis of the complexity of these problems. That is, we study the parameterised complexity of these logics. Introduced by Downey and Fellows [2], parameterised complexity provides a way to further pin down the true source of hardness. In the propositional team semantics setting, the study of parameterised complexity was initiated by Meier and Reinbold [22] in the context of parameterised enumeration problems, and by Mahmood and Meier [21] in the context of classical decision problems, for PDL. The current paper continues the line of research initiated in [21]. Our focus is on the parameterised complexity of propositional inclusion and independence logic.
Parameterised complexity is a widely studied subarea of complexity theory. The motivation being that it provides a deeper analysis than the classical complexity theory by providing further insights in to the source of intractability. The idea here is to identify meaningful parameters of inputs such that fixing those makes the problem tractable. One example of a fruitful parameter is the treewidth of a graph. A parameterised problem (PP) is called fixed parameter tractable, or in FPT for short, if for a given input x with parameter k, the inclusion of x in PP can be decided in time f (k) · p(|x|) for some computable function f and polynomial p. That is, for each fixed value of k the problem is tractable in the classical sense of tractability (in P). If, on the other hand, PP is solvable in time p(|x|) f (k) , then PP lies in the parameterised complexity class XP. It is still true that for each fixed value of k, PP is in P, but the degree of the polynomial now depends on the parameter k. Consequently, one desires for FPT-run time for the problem at hand. Moreover, FPT XP [7] and in between the two classes, there exists a presumably infinite hierarchy of classes, the so-called W-hierarchy: The Whierarchy intuitively measures the degree of hardness of a problem under the given parameterisation. The class paraNP consists of problems decidable in time f (k) · p(|x|) on a nondeterministic machine.
In this paper we focus on the parameterised complexity of model checking (MC) and satisfiability (SAT) for PIN C and PIN D. We consider both lax and strict semantics. The lax semantics is the prevailing semantics in the team semantics literature. The past rejection of strict semantics was based on the fact that it does not satisfy locality [8] (simply put, locality principle dictates that satisfaction of a formula should be invariant on the truth values of variables that do not occur in the formula). However more recent works have revealed that locality of strict semantics can be recovered by moving to multiteam semantics (here teams are multisets instead of sets) [3]. Since, in propositional team semantics, the shift from teams to multiteams has no complexity theoretic implications, we stick with the simpler set based semantics for our logics.
In the model checking problem, one is given a team T and a formula φ, and the task is to determine whether T |= φ. In the satisfiability problem, one is given a formula φ, and the task is to decide whether there exists a non-empty satisfying team T for φ. Regarding PIN C, MC is either in P or NP-complete depending on whether lax or strict semantics is used. Consequently, for MC in PIN C we only consider strict semantics. However, SAT for PIN C is EXPcomplete under both semantics. Table 2 gives an overview of our results. Interestingly, MC for each L ∈ {PDL, PIN D, PIN C} under parameterisation k ∈ {team-size, formula-team-tw, formula-size, formula-depth, #variables} is FPT. The picture slightly changes regarding SAT. For PDL and PIN D, SAT parameterised by team-size is paraNP-complete, while for PIN C the parameter team-size is not meaningful anymore.
Organization We introduce the required notions in Section 2. This is followed by proving general results that hold not only for logics considered in this paper but for any team based logic L such that L-atoms can be evaluated in polynomial time. The parameterised complexity of PDL was analysed in [21]. We classify the parameterised complexity of model checking and satisfiability for inclusion and independence logic in Section 4 and 5 recpectively. Moreover, in Section 4 (resp., 5), MC and SAT correspond to the model checking and satisfiability for PIN C (PIN D). We conclude in Section 6 with interesting remarks and future directions for work.

Preliminaries
We assume familiarity with standard notions in complexity theory such as classes P, NP and EXP [25].
Parameterised Complexity We give a short exposition of relevant concepts from parameterised complexity theory. For a broader introduction consider the textbook of Downey and Fellows [2], or that of Flum and Grohe [7]. A parameterised problem (PP) Π ⊆ Σ * × N consists of tuples (x, k), where x is called an instance and k is the (value of the) parameter.
Definition 1 (FPT and paraNP). Let Π be a PP over Σ * × N. Then Π is fixed parameter tractable (FPT for short) if it can be decided by a deterministic algorithm A in time f (k) · p(|x|) for any input (x, k), where f is a computable paraNP paraNP paraNP paraNP function and p is a polynomial. If the algorithm A is nondeterministic instead, then Π belongs to the class paraNP.
Let P be a PP over Σ * × N. Then the ℓ-slice of P , for ℓ ≥ 0, is the set The notion of hardness in parameterised complexity is employed by FPT reductions, defined as follows.
there exists a computable function g : N → N such that for all (x, k) ∈ Σ * ×N and f (x, k) = (x ′ , k ′ ) we have that k ′ ≤ g(k).
We will use the following result to prove paraNP-hardness.
Moreover, we will use the following folklore result to get several upper bounds.
Proposition 2. Let Q be a problem such that (Q, k) is FPT and let ℓ be another parameter with k ≤ f (ℓ) for some computable function f , then (Q, ℓ) is also FPT.
Propositional Team Based Logics Let VAR be a countably infinite set of variables. The syntax of propositional logic (PL) is defined via the following EBNF: where ⊤ is verum, ⊥ is falsum and x ∈ VAR is a variable. The propositional dependence logic PDL is obtained by adding to PL the atomic formula of the form =(x; y), where x, y ⊂ VAR are finite tuples of variables. Similarly, adding inclusion atoms x ⊆ y where (|x| = |y|) and independence atoms x⊥ z y gives rise to the propositional inclusion (PIN C) and independence (PIN D) logic, respectively. Observe that we only consider atomic negation. The tuple x in =(x; y) can be empty, giving rise to formulas of the form =(; y), the logic with only such dependence atoms is called the constancy logic. Similarly, the tuple z in x⊥ z y can be empty, in which case we simply write x⊥y. When either argument of any atom consists of a single variable, we write it as such, for example, =(x; y). By dependency atoms, we mean a dependence, an independence or an inclusion atom. Finally, when we wish to talk about any of the three considered logics, then we simply write L. That is, unless otherwise stated, L ∈ {PDL, PIN C, PIN D} and L contains dependency atoms of only one form. For an assignment s and a tuple x = (x 1 , . . . , x n ), s(x) denotes the tuple (s(x 1 ), . . . , s(x n )).

Definition 3 (Team semantics).
Let ϕ, ψ be L-formulas and x, y, z ⊂ VAR be finite tuples of variables. A team T is a set of assignments t : VAR → { 0, 1 }. We define the satisfaction relation |= as follows, where T |= ⊤ is always true and T |= ⊥ iff T = ∅: Observe that for the satisfaction of formulas of the form =(; y) the team has to be constant with respect to y, that is why such atoms are called constancy atoms. Similarly, for x⊥y, the pair t, t ′ ranges over all assignments in T . The operator ∨ is also called a split-junction in the context of team semantics. Note that in literature there exist two semantics for the split-junction: lax and strict semantics (e.g., Hella et al. [15]). Strict semantics requires the "splitting of the team" to be a partition whereas lax semantics allows an "overlapping" of the team. Regarding PDL and PIN D, the complexity for SAT and MC is the same irrespective of the considered semantics. However, the picture is different for MC in PIN C as depicted in [15, page 627]. For any logic L, we denote MC under strict (respectively, lax) semantics by MC s (MC l ). Moreover, MC l is in P for PIN C and consequently, we have only MC s in Table 2. Finally, note that allowing the contradictory negation increases the complexity of SAT in these logic to ATIME-ALT(exp, poly) (alternating exponential time with polynomially many alternations) as shown by Hannula et al. [12].
In the following, we present well-known formula properties of these logics which are relevant to our results in the paper. A formula φ is flat if, given a team T , we have that T |= φ ⇐⇒ { s } |= φ for every s ∈ T . A logic L is downwards closed if for every L-formula φ and team T , if T |= φ then for every The classical PL-formulas are flat as well as union and downwards closed. The flatness implies that, the truth value for PLformulas is evaluated under each assignment individually. As a consequence, the semantics is the usual Tarski semantic. Every PDL-formula without a split is 2-coherent. Moreover, PDL is downwards closed, whereas PIN C is union closed.

Graph Representation of the Input
In order to consider specific structural parameters, we need to agree on a representation of an input instance. We follow the conventions given in [21]. Recall that the well-formed L-formulas, for every L ∈ {PDL, PIN C, PIN D}, can be seen as binary trees (the syntax tree) with leaves as atomic subformulas (variables and dependency atoms). Similarly to PDL [21], we take the syntax structure (defined below) rather than syntax tree as a graph structure in order to consider treewidth as a parameter. We use the same graph representation for each L-formula for L ∈ {PDL, PIN C, PIN D}. That is, when an atom =(x; y) is replaced by either x ⊆ y or x⊥y, the graph representation, and hence, the treewidth of this graph remains the same. Also, in the case of MC, we include assignments in the graph representation. In the latter case, we consider the Gaifman graph of the structure that models both, the team and the input formula.
Definition 4 (Syntax Structure [21]). Let T, φ be an instance of MC, where φ is an L-formula with propositional variables {x 1 , . . . , x n } and T = { s 1 , . . . s m } is a team of assignments s i : VAR → { 0, 1 }. The syntax structure A T,φ has the vocabulary, where superscripts denote the arity of each relation. The where SF(φ) and VAR(φ) denote the set of subformulas and variables appearing in φ, respectively.
-SF and VAR are unary relations representing 'is a subformula of φ' and 'is a variable in φ' respectively.
-DEP is a binary relation which connects each L-atom with used variables, as well as, two variables in the same L-atom. That is, if α = =(x; y) then DEP(α, x), DEP(α, y) and DEP(x, y) are true in A T,φ . -The set { c 1 , . . . , c m } encodes the team T . Each c i ∈ τ T,φ corresponds to an assignment s i ∈ T for i ≤ m, and interpreted as c A i ∈ A.
-isTrue and isFalse relate variables with the team elements. isTrue(c, x) (resp., isFalse(c, x)) is true if and only if x is mapped 1 (resp., 0) by the assignment in T interpreted by c.
Analogously, the syntax structure A φ over a respective vocabulary τ φ is defined.
Where τ φ neither contains the team related relations nor the constants c A i for Definition 5 (Gaifman graph). Given a team T and an L-formula φ, the Analogously, we let G φ to be the Gaifman graph for the τ φ -structure A φ .
is a collection of bags and E T is the edge relation such that the following is true.
is connected.
The width of a tree decomposition T = (B, E T ) is the size of the largest bag minus one: max b∈B |b| − 1. The treewidth of a graph G is the minimum over widths of all tree decompositions of G.
The treewidth of a tree is one. Intuitively, it measures the tree-likeness of a given graph.
Example 2 (Adapted from [21]). Figure 1 represents the Gaifman graph of the syntax structure A φ (in middle) with a tree decomposition (on the right). Since the largest bag is of size 3, the treewidth of the given decomposition is 2. Figure 2 presents the Gaifman graph of the syntax structure A T,φ , that is, when the team T = {s 1 , s 2 } = {0011, 1110} is also part of the input (an assignment s is denoted as s(x 1 . . . x 4 )). The presented graph representation is invariant under the logics we consider, that is, when the atom =(x 3 ; x 4 ) is replaced by either

Parameterisations Considered
We consider eight different parameters for both problems (MC and SAT). These include formula-tw, formula-team-tw, team-size, formula-size, #variables, formula-depth, #splits and arity. All these parameters arise naturally in problems we study. Let T be a team and φ an L-formula. The parameters are defined as follows: -#splits denotes the number of times a split-junction (∨) appears in φ and #variables denotes the number of distinct propositional variables. formula-depth is the depth of the syntax tree of φ, that is, the length of the longest path from root to any leaf in the syntax tree. team-size is the cardinality of the team T , and formula-size is |φ|.
-For a dependence atom =(x; y) and inclusion atom x ⊆ y, the arity is defined as |x| (recall that |x| = |y| for an inclusion atom), whereas, for an independence atom x⊥ z y, it is the number of distinct variables appearing in x⊥ z y. Finally, arity denotes the maximum arity of any L-atom in φ.
Regarding treewidth, recall that for MC, we also include the assignmentvariable relation in the graph representation. This yields two graphs: G φ for φ, and G T,φ for T, φ . Consequently, there are two treewidth notions as follows.
formula-tw is the treewidth of G φ .
formula-team-tw is the treewidth of G T,φ .
The name emphasises whether the team is also part of the graph. Clearly, formula-team-tw is only relevant for MC.
Given an instance T, φ and a parameterisation κ, then κ(T, φ) denotes the parameter value of T, φ . The following relationship between several of the aforementioned parameters was proven for PDL. It is easy to observe that the lemma also applies to PIN C and PIN D.
Moreover, recall that we use the same graph representation for PDL, PIN C and PIN D. As a consequence, the following result also applies. That is, bounding the treewidth of the structure also bounds the team-size when the team T is part of the graph representation.

General Complexity Results
In this section, we present general complexity results that hold not only for logics considered here, but for any team based logic L such that L-atoms are P-checkable. An L-atom α is P-checkable if given a team T , then in polynomial time one can check whether T |= α. It is immediate that each atom considered in this paper is P-checkable. Theorem 1. Let L be a team based logic such that L-atoms are P-checkable, then MC parameterised by team-size is FPT.
Proof. We claim that the bottom up (brute force) algorithm for the model checking of PDL [21, Thm. 17] works for any team based logic L such that L-atoms are P-checkable. This is because the algorithm begins by checking the satisfaction of atoms against each subteam. This can be achieved in FPT-time since teamsize and consequently the number of subteams is bounded. Moreover, by taking the union of subteams for split-junction and keeping the same team for conjunction the algorithm can find subteams for each subformula in FPT-time. Lastly, it checks that the team T is indeeded a satisfying team for the formula φ. For any team based logic L, the FPT runtime is guaranteed if L-atoms are P-checkable. Finally, the proof works for both strict and lax semantics.
This implies the following corollary in conjunction with Lemma 1 and Proposition 2.
Corollary 2. Let L be any team based logic such that L-atoms are P-checkable, then MC for L when parameterised by k is FPT, if k ∈ {formula-team-tw, formula-depth, #variables, formula-size}.
The following theorem states results for satisfiability.
Theorem 2. Let L be a team based logic such that L-atoms are P-checkable, then SAT parameterised by k is FPT if k ∈ {formula-size, formula-depth, #variables}.
Proof. The case for formula-size follows because any problem parameterised by input size is FPT. Moving on, bounding formula-depth also bounds formula-size, this yields the FPT-membership for formula-depth in conjunction with Proposition 2. Finally, for #variables, one can enumerate all of the 2 2 #variables -many teams in FPT-time and determine whether any of these satisfies the input formula. The last case requires that the model checking parameterised by team-size is FPT, which is indeed the case due to Theorem 1. This completes the proof.
Notice that one can also use the team properties of a logic L to determine MC and SAT more efficiently. For example, for SAT in PDL, it is enough to determine if there exists a satisfying singleton team for a given PDL-formula. This is because PDL is downwards closed. As a consequence, one only has to check 2 #variables -many assignments. Now we move on to results which are specific to logics considered in this paper.

Propositional Inclusion Logic (PIN C)
The model checking for PIN C under lax semantics is in P. As a consequence, we consider MC under strict semantics alone. We wish to point out that some of our results are directly translated from the reduction for proving NP-hardness of MC s for PIN C [15]. However, one still needs to assure that the reduction is indeed an fpt -reduction with respect to the considered parameters. We include the following lemma for self containment.

Lemma 2 ([14]). MC for PIN C under strict semantics is NP-hard.
Proof Idea. The hardness is achieved through a reduction from set splitting problem to the model checking problem for PIN C with strict semantics. An instance of set splitting problem consists of a family F of subsets of a finite set S. The problem asks if there are S 1 , S 2 ⊆ S such that S 1 ∪ S 2 = S, S 1 ∩ S 2 = ∅ and for each A ∈ F there exists a 1 , a 2 ∈ A such that a 1 ∈ S 1 , a 2 ∈ S 2 . Let F = {B 1 , . . . , B n } and F = S = {a 1 , . . . , a k }. Let p i and q j denote fresh variables for each a i ∈ S and B j ∈ F . Moreover, let V F = {p 1 , . . . , p k , q 1 , . . . , q n , p ⊤ , p c , p d }. Then define T F = {s 1 , . . . , s k , s c , s d }, where each assignment s i is defined as follows: That is, T F includes an assignment s i for each a i ∈ S. The reduction also yields the following PIN C-formula.
Clearly, the split of T F in to T 1 , T 2 ensures the split of S into S 1 and S 2 and vice versa. Whereas, s c and s d ensure that none of the split is empty.
Proof. Consider the PIN C-formula φ F from Lemma 2, which includes only one split-junction and the inclusion atoms have arity one. This gives the desired paraNP-hardness for MC s when parameterised by #splits and arity.
The proof for formula-tw is more involved and we prove the following claim.
Claim. φ F has fixed formula-tw. That is, the treewidth of φ F is independent of the input instance F of the set-spliting problem. Moreover treewidth(φ F ) ≤ 4.
Proof of Claim. The PIN C-formula φ F is related to an input instance F of the set splitting problem only through its input size, which is n. Therefore the formula structure remains unchanged when we vary an input instance, only the size of two big conjunctions vary. To prove the claim, we give a tree decomposition for the formula with treewidth(φ F ) = 4. Since treewidth is minimum over all the tree decompositions, this proves the claim. Let us rewrite the formula as below.
That is, each subformula is renamed so that it is easy to identify as to which side of the split it appears (e.g., p ⊤ ⊆ l i q i denotes the ith inclusion atom in the big conjunction on the left, denoted as I l i in the graph). The graphical representation of φ F with V = SF(φ F ) ∪ VAR(φ F ), as well as, a tree decomposition, is given in Figure 3. Notice that there is an edge between x and y in the Gaifman graph if and only if either y is an immediate subformula of x, or y is a variable appearing in the inclusion atom x. It is easy to observe that the decomposition presented in Figure 3 is indeed a valid tree decomposition (Def. 6) in which each node is labelled with its corresponding bag. Moreover, since the maximum bag size is 5, the treewidth of this decomposition is 4. This proves the claim.
This completes the proof to our theorem.
The remaining FPT-cases for MC s follow from Theorem 1 and Corollary 2.    The Gaifman graph (left) and a tree decomposition (right) for φF . Note that we abbreviated subformulas in the inner vertices of the Gaifman graph for presentation reasons. Also, edges between p ⊤ and variables qi are omitted for better presentation, but those are covered in the decomposition on the right.

Satisfiability
We begin by proving that SAT parameterised by arity is paraNP-complete. The hardness follows because the satisfiability for PL is NP-complete and PL is a fragment of PIN C. For membership, we give a non-deterministic algorithm A solving SAT.
Theorem 4. Given a PIN C-formula φ with arity k, then there is a nondeterministic algorithm A that runs in O(2 k · p(|φ|))-time and outputs a team T such that T |= φ if and only if φ is satisfiable.
Proof. Given an input φ, the procedure A operates on the syntax tree of φ as follows. A begins by guessing a subteam f 0 (α) for each atomic α ∈ SF(φ). For i ≥ 1, it implements the following steps recursively.
For odd i, f i (ψ) is defined in bottom-up fashion as follows.
For even i ≤ n, f i (ψ) is defined in top-down fashion as follows.
We first claim that each step of A takes (non-deterministic) polynomial time.
Clearly the only step when new assignments are added, is at the atomic level. Whereas, the split in Step 5 concerns those assignments which arise from other subformulas through union in Step 2. We prove the following claim.
Claim. Given a team S and an atomic subformula α of φ, then in polynomial time (in α and |S|), one can find a team T ⊇ S such that T |= α, if such a team exists. More precisely |T | ≤ 2 · |S|.
Proof of Claim. For a literal α, output S if S |= α, otherwise reject because no such team exists. WLOG, we assume that S is a team over variables in α alone. For a k-ary inclusion atom α := x ⊆ y, if S |= α then return S. Otherwise, T is obtained from S by adding for each s ∈ S, an assignment t such that t(xy) = s(xx) provided that t ∈ S. Clearly, T |= α by definition. In the worst case, one has to take care of every assignment in S, which doubles the size for T .
Next we claim that A runs in at most O(2 k ·p(|φ|)) steps for some polynomial p, where k is the arity of φ. That is, a fixed point is reached in this time.
Proof of Claim. In each round i, either A rejects, or keeps adding new assignments. The only step when new assignments are added occurs at the atomic level. However, due to Claim 5.1, at most 2 l many assignments can be added for an inclusion atom α of arity l ≤ k. Consequently, there is a j such that for each i ≥ j we have that f i (α) = f j (α). Let j m be such that for each atom (and indeed each subformula ψ), f i (ψ) = f i ′ (ψ) whenever i, i ′ ≥ j m . We denote this fixed point by f ∞ (ψ). Then f ∞ (ψ) is reached in at most O(2 k · p(|φ|)) steps.
We are now ready to present the correctness proof.

Claim. A accepts if and only if φ is satisfiable
Proof of Claim. Suppose that A accepts and outputs f ∞ (φ). We first prove by induction that f ∞ (ψ) |= ψ for each subformula ψ of φ. Notice that there is some i such that f ∞ (ψ) = f i (ψ).
-The case for atomic subformula is clear due to the way A works.
-Conjunction is easy to observe. This is because the team remains the same for each conjunct. That is, when ψ = ψ 0 ∧ψ 1 , and the claim holds for f ∞ (ψ i ) and In particular f ∞ (φ) |= φ and the correctness of our algorithm follows. For the other direction. Suppose that φ is satisfiable and T be a witnessing team. Then there exists a labelling function for the fact that T |= φ. That is, φ is labelled with T and for every subformula ψ = ψ 0 ⊕ ψ 1 and subteam P ⊆ T , the subteam for ψ i is P i such that for i = 0, 1 we have Moreover, P |= ψ for every ψ. Now, for each inclusion atom α := x ⊆ y with label P α , let f 0 (α) ⊆ P α denote the subteam obtained by removing an assignment t from P α if there exists an assignment s ∈ P α such that t(y) = s(y). Clearly, |f 0 (α)| ≤ 2 l since there are at most 2 l different values for y. Moreover, f 0 (α) |= α because P α |= α and an assignment t is removed only if there is an assignment s that agrees with t on y. Similarly, if α is a literal then let f 0 (α) be a singleton subteam of P α .
To prove that A accepts, we argue that in each iteration i, the algorithm does not stop by rejecting φ. This is easy to observe since A may begin with f 0 (α) ⊆ P α as its first guess. Clearly, in each round i, there exists a choice of assignments (to be added in round i), such that the subteam f i (α) satisfies the atom α. That is, A selects assignments in such a way that f i (α) ⊆ P α for every atom α of φ.
This completes the proof to our theorem.
Notice that, a minor variation in the algorithm A solves SAT s . When moving downwards, A needs to ensure that an assignment goes to only one side of the split. Moreover, for each atomic subformula, since the subteam is guessed nondeterministically, at each split-junction it rejects those subteams which do not split according to the strict semantics. The following corollary to Theorem 4 presents the upper bound for SAT when parameterised by treewidth. Proof. Recall the Graph structure (Def. 4) where we allow edges between variables within an inclusion atom. This implies that for each inclusion atom α, there is a bag in the tree decomposition that contains all variables of α. As a consequence, a formula φ with treewidth k has inclusion atoms of arity atmost k. Consequently, SAT parameterised by treewidth of the input formula can be solved using the paraNP-time algorithm from Theorem 4.
Regarding the parameter #splits, the precise parameterised complexity is still open for now. However, we prove that if there is no split in the formula, then SAT can be solved in polynomial time. This case is interesting in its own right because it gives rise to the so-called Poor Man's PIN C, similar to the case of Poor Man's PDL [6,20,22]. The model checking for this fragment is in P; this follows from the fact that MC for PIN C with lax semantics is in P. In the following, we prove that SAT for Poor Man's PIN C is also in P. We wish to emphasise that up to our knowledge, SAT for PIN C-formulas without splits has not been studied before in the propositional setting.
Theorem 5. Given a PIN C-formula φ with no splits, the problem to decide whether φ is satisfiable is in P.
Proof. We give a recursive labelling procedure (B) that runs in polynomial time and accepts if and only if φ is satisfiable. The labelling consists of assigning a value c ∈ {0, 1} to a variable x.
1. Begin by labelling all PL-literals in φ by the value that satisfies them, namely x = 1 for x and x = 0 for ¬x. 2. For each inclusion atom p ⊆ q and a labelled variable q i ∈ q, label the variable p i ∈ p with same value c as for q i . Where p i appears in p at the same position, as q i in q. 3. Propagate p i = c from the previous step. That is, replace every occurrence of p i with its label c ∈ {0, 1} and repeat step 2 for as long as possible. 4. If there is an inclusion atom p ⊆ q such that for some i, p i ∈ p and q i ∈ q are labelled with opposite values in {0, 1}, or if some variable x is labelled with two opposite values, then reject. Otherwise, accept.
Claim. B runs in polynomial time and accepts if and only if φ is satisfiable.
Proof of Claim. The fact that B works in polynomial time is clear because each variable is labelled at most once. If a variable is labelled to two different values, then it gives a contradiction and the procedure stops. For the correctness, notice first that if B accepts then we have a partition of VAR(φ) into a set X of labelled variables and a set Y = VAR(φ)\X. Moreover, when B stops, φ does not contain an inclusion atom p ⊆ q such that q i ∈ q and p i ∈ p for some q i ∈ X, p i ∈ Y (due to step 3). Where p i appears in p at the same position, as q i in q. Let T = {s | s ↾ Y ∈ 2 Y and s ↾ X satisfies each label in X}. One can easily observe that T |= φ. T satisfies each literal because each s ∈ T satisfies it. Let p ⊆ q be an inclusion atom and s ∈ T be an assignment. We know that for each x ∈ q that is fixed by s, the corresponding variable y ∈ p is also fixed, whereas, T contains every possible value for variables in q which are not fixed. This makes the inclusion atom true.
To prove the other direction, suppose that B rejects. If φ contains x ∧ ¬x for some variable x then the proof is trivial. Otherwise, there are variables x, y such that x ∧ ¬y ∈ φ and one of the following two cases occur. Intuitively, there is a sequence of inclusion atoms, such that keeping x = 1 and y = 0 contradicts some inclusion atoms (see Figure 4).
-There is a collection of inclusion atoms p j ⊆ q j and a sequence of variables z j for j ≤ n such that: z 0 = x, z n = y, and z j and z j+1 occur in the same position in q j and p j , respectively, for 0 ≤ j < n. This implies that φ is not satisfiable since for any team T such that T |= x ∧ ¬y, T does not satisfy the subformula j p j ⊆ q j of φ.
-There are two collections of inclusion atoms p j ⊆ q j for j ≤ n, and r k ⊆ s k for k ≤ m. Moreover, there are two sequences of variables z x j for j ≤ n and z y k for k ≤ m, and a variable v such that, z x 0 = x, z y 0 = y, z x n = v = z y m , and 1. for each j ≤ n, z x j appears in q j at the same position, as z x j+1 in p j , 2. for each k ≤ m, z y k appears in s k at the same position, as z y k+1 in r k . This again implies that φ is not satisfiable since for any satisfying team T such that T |= x ∧ ¬y, it does not satisfy the subformula Consequently, the claim follows.
This completes the proof.

Propositional Independence Logic (PIN D)
We begin by recalling that PIN D is more expressive than PDL. That is, for every PDL-formula φ, there is a PIN D-formula ψ, such that φ ≡ ψ. This follows from the fact that a dependence atom =(x; y) is equivalent to the independence atom y⊥ x y. As a consequence, (in the classical setting) the hardness results for PDL immediately translate to those for PIN D. Nevertheless, in the parameterised setting, one has to further check whether this translation 'respects' the parameter value of the two instances in the sense of Definition 2. This concerns the parameter arity and formula-tw. Recall that a dependence atom =(x; y) has arity |x|, whereas, the equivalent independence atom y⊥ x y has arity |x ∪ y|.
Proof. Notice that MC for PDL regarding these cases is also paraNP-complete. We argue that in reductions for PDL, replacing dependence atoms by the equivalent independence atoms yield fpt -reduction for the above mentioned cases. Moreover, this holds for both strict and lax semantics. For treewidth and arity, when proving paraNP-hardness of PDL, the resulting formula has treewidth of one [21,Cor. 16] and the arity is zero [21,Thm. 15]. Moreover, only the so-called constancy atoms of the form =(; p) where p is a propositional variable, are used and the syntax structure of the PDL-formula is already a tree. Consequently, replacing =(; p) with p⊥ ∅ p implies that only independence atoms of arity 1 are used. Notice also that replacing dependence atoms by independence atoms does not increase the treewidth. This is because when translating dependence atoms into independence atoms, no new variables are introduced. As a result, the reduction also preserves the treewidth. This proves the claim as 1-slice regarding both parameters arity and treewidth, is NP-hard.
Regarding the #splits, the claim follows due to Mahmood and Meier [21,Thm. 18] because the reduction from the colouring problem uses only 2 splits.

Satisfiability
Theorem 7. SAT for PIN D when parameterised by k is paraNP-complete if k ∈ {arity, team-size}. Whereas, it is FPT for all other cases.
Proof. Recall that a PIN D-formula φ is satisfiable if and only if it is satisfied by a singleton team {s} [13, Thm. 1]. Moreover, over singleton teams, the independence atoms are trivially true. Consequently, the question boils down to PL. This implies that when arity is zero and team-size is one, the satisfiability problem is NP-hard. As a consequence, the hardness cases follow due to the hardness of SAT for PL. The membership is clear since SAT for PIN D is NP-complete.
The FPT cases for k ∈ {formula-size, formula-depth, #variables} follows because of Theorem 2. The cases for #splits and treewidth follow from the corresponding cases for PDL ( [21]) because it is enough to find a singleton satisfying team. This completes the proof.

Concluding Remarks
We presented a parameterised complexity analysis for PIN C and PIN D. The problems we considered are satisfiability and model checking. Interestingly, the parameterised complexity results for PIN D coincide with that of PDL in each case. Moreover, the complexity of model checking under a given parameter remains same for all three logics. We proved that FPT cases are true for every team based logic L, such that L-atoms can be evaluated in P-time.
The parameters team-size and arity regarding SAT behave surprisingly in the logics we considered. Namely, for PIN C, SAT under team-size is not meaningful due to the reason that we do not impose a size restriction for the satisfying team in SAT. Consequently, the parameter team-size does not provide any 'useful information' to solve satisfiability. On the other hand, for PIN D and PDL, the problem parameterised by team-size is paraNP-complete. One possible explanation is that, PDL is downwards closed and a formula is satisfiable iff some singleton team satisfies it. However, PIN D also satisfies this 'satisfiable under singleton team' property. On the other hand, PIN C is not downwards closed and the satisfiability of a PIN C-formula φ might generate a team of exponential size. The parameter arity, on the other hand, is interesting because SAT for all three logics is paraNP-complete. This implies that while the fixed arity does not lower the complexity for SAT in PDL and PIN D, it does lower it from EXP-completeness to NP-completeness for PIN C.
As a future work, we wish to find the precise complexity of SAT for PIN C when parameterised by #splits and formula-tw. Hella and Stumpf ( [16]) posed an interesting question to determine the complexity of satisfiability for modal inclusion logic with only unary inclusion atoms. In Theorem 4 we proved that the fixed-arity fragment of PIN C has the same complexity for SAT as PL (NPcomplete). It might be interesting to explore whether the same complexity drop occurs for modal inclusion logic.