{'fraction_non_alphanumeric': 0.05841390711888182, 'fraction_numerical': 0.0150042583036922, 'mean_word_length': 3.5862148190695002, 'pattern_counts': {'":': 2, '<': 18, '<?xml version=': 0, '>': 8, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 28, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Enumeration Complexity of Poor Man's Propositional Dependence Logic

In this paper, we aim to initiate the study of enumeration complexity in the field of dependence logics. Consequently, as a first step, we investigate the problem of enumerating all satisfying teams of a given propositional dependence logic formula without the split junction operator. We distinguish between restricting the team size by arbitrary functions and the parametrised version where the parameter is the team size. We show that a polynomial delay can be reached for polynomials and otherwise, in the parametrised setting, we reach FPT delay. However, the constructed enumeration algorithm with polynomial delay requires exponential space. We show that an incremental polynomial delay algorithm exists which uses polynomial space only. Negatively, we show that for the general problem without restricting the team size, an enumeration algorithm running in polynomial space cannot exist.


Introduction
Consider the following scenario: a team of students wishes to stage a match of robot soccer. They have to assemble two teams of robots, where each robot consists of a COM-unit and a mobility unit. Two different companies C 0 and C 1 manufactured both units. To enable co-operation, robots of the same team have to be equipped with the same COM-units. Furthermore, each robot is assigned to one of two maintenance rooms. As the space in the maintenance rooms is limited, each room provides tools for maintaining the communication unit of only one company. The same applies for the mobility unit. Consequently, all robots assigned to the same maintenance room have to be equipped with the same units. Due to rumours concerning the reliability of the mobility-units manufactured by C 0 , the students wish to install mobility units of the company C 1 only. To minimise the risk of failure, as many robots as possible have to be configured differently. However, each pair of two robots still has to be compatible concerning the previous restrictions. We model each configuration by four binary properties x 1 , . . . , x 4 . The first property describes the team membership of a robot. The second property identifies the maintenance room for each robot. The third and fourth property provide the manufacturer of the COM-and mobility unit. A set of configurations T is conform with the scenario iff T |= ϕ with ϕ := where the expressions of the form =(P, Q) denote that the values of P functionally determine the values of Q. For this reason, the students are interested in enumerating all satisfying teams T for ϕ.
In 2007, Jouko Väänänen introduced dependence logic (DL) [21] as a novel variant of Hintikka's independence-friendly logic. This logic builds on top of compositional team semantics which emerges from the work of Hodges [13]. In this logic, the satisfaction of formulas is interpreted on sets of assignments, i.e., teams, instead of a single assignment as in classical Tarski semantics. Besides the mentioned dependence atoms =(P, Q) an important operator is the so-called split junction operator. This operator generalises the classical disjunction operator into the team semantics setting: a split junction ϕ ∨ ψ is satisfied by a team if there exist a split of the team into two (not necessarily disjunct) sub-teams where one satisfies ϕ and the other ψ. From a computational complexity perspective, this logic is well understood: most of the possible operator fragments have been sophistically classified [10,11]. However, it turned out that model checking and satisfiability for propositional dependence logic PDL are already NP-complete [7,17]. As a result, we focus on the split junction free fragment of PDL as we plan to initiate the study of enumeration in this area of research. For historical reasons, we will call this subset of the full logic the Poor Man's fragment [12].
The task of enumerating all solutions of a given instance is relevant in several prominent areas, e.g., one is interested in all tuples satisfying a database query, DNA sequencings, or all answers of a web search. In enumeration complexity one is interested in outputting all solutions of a given problem instance without duplicates. Often, one obyes a specific order on the output. Of course, all these algorithms usually are not running in polynomial time as there often exist more than polynomial many solutions. As a result, one classifies these deterministic algorithms with respect to their delay [14,19,20]. Informally, the delay is the time which elapses between two output solutions. For instance, the class DelayP then encompasses problems for which algorithms with a polynomial delay (in the input length) exist. Another important class for this study is IncP, incremental P. For this class the delay of outputting the ith solution of an instance is polynomial in the input size plus the index i of the solution. Consequently, problem instances exhibiting exponential many solutions eventually possess an exponential delay whereas, in the beginning, the delay was polynomial. Some natural problems in this class are known, e.g., enumerating all minimal edge dominating sets [8] or some problems for matroids [15].
A prominent approach of attacking computationally hard problems is the framework of parametrised complexity by Downey and Fellows [5,4]. Essentially, one searches for a parameter k of a given problem such that the problem can be solved in time f (k) · n O(1) instead of n f (k) where n is the input length and f is an arbitrary recursive function. Assuming that the parameter is slowly growing or even constant, then the first kind of algorithms is seen relevant for practice. In these cases, one says that the problem is fixed parameter tractable, or short, in FPT. A simple example here is the propositional satisfiability problem with the parametrisation numbers of variables. For this problem, the straightforward brute-force algorithm already yields FPT. Recently, this framework has been adapted to the field of enumeration by Creignou et al. [3,2] There, the authors introduced the corresponding enumeration classes DelayFPT and IncFPT and provided some characterisations of these classes.
In this paper, we investigate the problem of enumerating all satisfying teams of a given propositional dependence logic formula without the split junction operator. In particular, we distinguish between restricting the team size by arbitrary functions f and the parametrised version where the parameter is the team size. We show that DelayP can be reached if f is a polynomial in the input length and otherwise the parametrised approach leads to DelayFPT. However, the constructed DelayP enumeration algorithm requires exponential space. If one desires to eliminate this unsatisfactory space requirement, we show that one has to pay the price of an increasing delay, i.e., then an IncP algorithm can be constructed which uses polynomial space only. Here, we show, on the downside, that for the general problem without restricting the team size an enumeration algorithm running in polynomial space cannot exist.

Preliminaries
We will make use of standard notions in complexity theory. In particular, we will use the classes P and NP. Further, the underlying machine concept will be RAMs as we require data structures with logarithmic costs for standard operations. A detailed description of the RAM computation model may be found in [20, section 1.2.2]. The space occupied by a RAM is given by the total amount of used registers, provided that the content of each register is polynomially bounded in the size of the input. Furthermore, we will follow the notion of Durand et al. [6], Creignou et al. [3] and Schmidt [19].
Team-based Propositional Logic Let V be a (countably infinite) set of variables. The class of all Poor Man's Propositional formulas PL − is derived via the grammar The set of all variables occurring in a propositional formula ϕ is denoted by Var(ϕ). Now we will specify the notion of teams and its interpretation on propositional formulas. An assignment over V is a mapping s : V → {0, 1}. We set 2 V := {s : s assignment over V}. A team T over V is a subset T ⊆ 2 V . Consequently, the set of all teams over V is denoted by P 2 V . If X is a subset of V, we set T X := s X : s ∈ T , where s X is the restriction of s on X. If T has cardinality k ∈ N, we say that T is a k-Team. If ϕ is a formula, then a team (assignment) over Var(ϕ) is called a team (assignment ) for ϕ.
Definition 1 (Satisfaction) Let ϕ be a team-based propositional formula and T be a team for ϕ. We define T |= ϕ inductively by We say that T satisfies ϕ iff T |= ϕ holds.
Note that we have T |= (x ∧ ¬x) iff T = ∅. This observation motivates the definition for T |= 0. Observe that the evaluation in classical propositional logic occurs as the special case of evaluating singletons in team-based propositional logic.
Definition 2 (Downward closure) A team-based propositional formula ϕ is called downward closed, if for every team T it holds that T |= ϕ ⇒ ∀S ⊆ T : S |= ϕ. An atom is called downward closed, if its corresponding atomic formula is downward closed. An operator • of arity k is called downward closed, if •(ϕ 1 , . . . , ϕ k ) is downward closed for all downward closed formulas ϕ i , i = 1, . . . , k. A class φ of team-based propositional formulas is called downward closed, if all formulas in φ are downward closed.
The following lemma then is straightforwardly to prove. Lemma 3 All atoms and operators in PDL − are downward closed. In particular, PDL − is downward closed.
Proof It is easy to see that the atoms x, ¬x, 0, 1, =(·) are downward closed. Let ϕ, ψ be two downward closed formulas. Let T be a team with T |= ϕ ∧ ψ. Then we have T |= ϕ and T |= ψ, so that S |= ϕ and S |= ψ for every subset S ⊆ T . It follows that S |= ϕ ∧ ψ. For this reason ∧ is downward closed. The proof for is similar.
Enumeration problems Let Σ be a finite alphabet and (S, ≤) a poset of possible solutions. An enumeration problem is a triple E = (Q, Sol, ≤) such that (i) Q ⊂ Σ * is a decidable language and (ii) Sol : Q → P(S) is a computable function. For an element x ∈ Q we call x an instance and Sol(x) its set of solutions. If ≤ is the trivial poset given by x ≤ y :⇔ x = y, we omit it and write E = (Q, Sol). Analogously, we write x < y for x ≤ y and x = y.
Definition 4 (Enumeration algorithm) Let E = (Q, Sol, ≤) be an enumeration problem. A deterministic algorithm A is an enumeration algorithm for E if for every input x ∈ Q 1. A terminates, 2. A outputs the set Sol(x) without duplicates, 3. for every s, t ∈ Sol(x) with s < t the solution s is outputted before t.
Definition 5 (Delay) Let A be an enumeration algorithm for the enumeration problem E = (Q, Sol, ≤) and x ∈ Q. The i-th delay of A is defined as the elapsed time between outputting the i-th and (i + 1)-th solution of Sol(x), where the 0-th and (|Sol(x)| + 1)-th solutions are considered to be the start and the end of the computation respectively. The 0-th delay is called precalculation delay and the |Sol(x)|-th solution is called postcalculation delay.
Definition 6 Let E = (Q, Sol, ≤) be an enumeration problem and A be an enumeration algorithm for E. A is 1. an IncP-algorithm if there exists a polynomial p such that the i-th delay on input x ∈ Q is bounded by p(|x| + i).
2. a DelayP-algorithm if there exists a polynomial p such that all delays on input x ∈ Q are bounded by p(|x|).
3. a DelaySpaceP-algorithm if it is a DelayP-algorithm using polynomial amount of space with respect to the size of the input.
For ease of notation, we define the classes DelayP (IncP, DelaySpaceP) as the class of all enumeration problems admitting an DelayP-(IncP, DelaySpaceP)-algorithm. Now we introduce the parametrised version of enumeration problems. The extensions are similar to those when extending P to FPT. We follow Creignou et al. [3].

Definition 8 Let
A be an enumeration algorithm for a parametrised enumeration problem E = (Q, κ, Sol, ≤). If there exist a polynomial p and a computable function f : N → N such that the i-th delay on input x ∈ Q is bounded by f (κ(x)) · p(|x| + i), then A is a IncFPTalgorithm. We call A a DelayFPT-algorithm if all delays on input x ∈ Q are bounded by f (κ(x)) · p(|x|). The class IncFPT contains all enumeration problems that admit an IncFPTalgorithm. The class DelayFPT is defined analogously.

Group action
The following section provides a compact introduction in group actions on sets. For a deeper introduction see, for instance, Rotman's textbook [18].
Definition 9 (Group action) Let G be a group with identity element e and X be a set. A group action of G on X, denoted by G X, is a mapping G × X → X, (g, x) → gx, with Now observe the following. Let G be a group and X a set. The mapping (g, h) → gh for g, h ∈ G defines a group action of G on itself. A group action G X induces a group action of G on P(X) by gS := {gs : s ∈ S} for all g ∈ G, S ⊆ X. Note that this group action preserves the cardinality of sets.
Definition 10 (Orbit) Let G X be a group action and x ∈ X. Then the orbit of x is given by Gx := {gx : g ∈ G} ⊆ X.

Proposition 11 ([18])
Let G X be a group action and x, y ∈ X. Then either Gx = Gy or Gx ∩ Gy = ∅. Consequently the orbits of G X partition the set X.
Definition 12 (Stabiliser) Let G X be a group action and x ∈ X. The stabilizer subgroup of x is given by G x := {g ∈ G : gx = x} and indeed is a subgroup of G.
Proposition 13 (Orbit-Stabiliser theorem, [18,Theorem 3.19]) Let G be a finite group acting on a set X. Let x ∈ X. Then the mapping gG x → gx is a bijection from G/G x to Gx. In particular it holds that |Gx| · |G x | = |G|.
Proposition 14 (Cauchy-Frobenius lemma, [18,Theorem 3.22]) Let G be a finite group acting on a set X. Then the amount of orbits is given by 1 |G| g∈G |{x ∈ X : gx = x}|.

Results
In this section, we investigate the complexity of enumerating all satisfying teams for various fragments of team-based propositional logic. After introducing the problem EnumTeam and its parametrised version p-EnumTeam we develop two enumeration algorithms for PDL − , either guaranteeing polynomial delay or incremental delay in polynomial space.

Problem 15 Let Φ be a class of team-based propositional formulas and
We write EnumTeam(Φ) for EnumTeam(Φ, n → 2 n ). Since |T | ≤ 2 |ϕ| holds for every team T for ϕ, we effectively eliminate the cardinality constraint. As we shall see, the order in which the teams are outputted plays an important role in the following reasoning. There are two natural orders on teams to consider.
Definition 17 (Order of cardinality) Let R, S be two teams. Then we define a partial order on the set of all teams by R ≤ size S :⇔ |R| < |S| or R = S.
When a formula ϕ is given, we assume to have a total order ≤ on 2 Var(ϕ) such that comparing two elements is possible in O(|Var(ϕ)|) and iterating over the set of all assignments is feasible with delay O(|Var(ϕ)|). When interpreting each assignment as a binary encoded integer, we obtain an appropriate order on 2 Var(ϕ) by translating the order on N 0 . If necessary, one could demand that adjacent assignments differ in only one place by using the order induced by the Gray code. Now we are able to define the second order.
Definition 18 (Lexicographical order) Let R = {r 1 , . . . , r n }, S = {s 1 , . . . , s m } be two teams such that r 1 < · · · < r n and s 1 < · · · < s m . Let i be the maximum over all j ∈ N 0 such that j ≤ min(n, m), r ℓ = s ℓ for all ∀ℓ ∈ {1, . . . , j}. Then we define a partial order on P 2 Var(ϕ) by Observe that the lexicographical order is a total order that does not extend the order of cardinality. For example, we have {00, 01, 10} < lex {00, 10} when assignments are ordered according to their integer representation.

Problem 19
Let φ be a class of team-based propositional formulas and let f : N → N be a computable function. Then we define EnumTeamSize(φ, f ) := (φ, Sol, ≤ size ) with Sol as in Problem 15. p-EnumTeamSize is defined accordingly.

Enumerating in Poor Man's Propositional Dependence Logic
Now, we start with the task of enumerating satisfying teams for the fragment PDL − of Poor Man's Propositional Logic. The delay of the resulting algorithm is polynomial regarding the size of the input and the outputted teams. As teams may grow exponentially large according to the input size, the delay will not be polynomial in the classical sense of DelayP. As a result, we proceed to DelayFPT and set the maximal cardinality of outputted teams as the parameter. Note that the drawback of having a polynomial delay in the output is minor. When following algorithms process the outputted teams, they have to input them first, requiring at least linear time in the output size.
In fact, we will see that we cannot obtain a DelayP-algorithm when the output is sorted by cardinality. This sorting, however, is an inherent characteristic of our algorithm as satisfying teams of cardinality k are constructed by analysing those of cardinality k − 1.
Before diving into details, we would like to introduce some notation used in this section.
An assignment s ∈ 2 Var(ϕ) is depicted as a sequence of 0 and 1, precisely: Example 20 For ϕ := =(x 1 , x 2 ) we have: n = 2 and consequently Note that formulas of the form ϕ ≡ x∈I x ∧ x∈J ¬x ∧ ℓ∈L =(P ℓ , Q ℓ ) can simplified w.l.o.g. to For instance, the example formula from the introduction

The group action of flipping bits
By the semantics of =(·) we see that flipping the bit at a fixed position in all assignments of a team T is an invariant for T |= =(P, Q). For example, the team {00, 10} satisfies =(x 1 , x 2 ). The remaining 2-team satisfying the formula is {01, 11}. Note that this team may be constructed from the previous one by flipping the value of x 2 . Accordingly, it would be enough to compute the satisfying team {00, 10} and construct the last 2-team by flipping bits. The concept of computing a minor set of satisfying k-Teams and constructing the remaining ones by flipping bits is the main concept of our algorithm for ensuring FPT-delay. By identifying each assignment s with the vector (s(x 1 ), . . . , s(x n )) we obtain a bijection of sets F n 2 ↔ 2 Var(ϕ) . We will switch between interpreting an element as an assignment or a F 2 -vector as necessary, leading to expressions like s + t for assignments s and t. Those may seem confusing at first, but become obvious when interpreting s and t as vectors. Vice versa, we will consider F 2 -vectors as assignments that may be contained in a team. When both notations are to be used, this is indicated by taking s ∈ F n 2 ∼ = 2 Var(ϕ) instead of simply writing s ∈ F n 2 or s ∈ 2 Var(ϕ) .
Definition 21 (Group action of flipping bits) By the observation after Def. 9 the group action of (F n 2 , +) on itself induces a group action of F n 2 on P(F n 2 ). On that account we obtain a group action F n 2 P 2 Var(ϕ) , called group action of flipping bits.
Let e i be the i-th standard vector of F n 2 . Then the operation of e i on P 2 Var(ϕ) corresponds to flipping the value for x i in each assignment of a team.
Proof As the axioms of group actions still hold on a subset of P(F n 2 ), it remains to show that zT ∈ T k ∀z ∈ F n 2 , T ∈ T k . Let z ∈ F n 2 and T ∈ T k . By Remark 9 we have |zT | = k. Let P ⊆ Var(ϕ) and s, t ∈ 2 Var(ϕ) . If s ′ , t ′ ∈ 2 Var(ϕ) arise from s, t by flipping the value for a variable x i , then obviously s P = t P ⇔ s ′ P = t ′ P . It follows that When assuming that ϕ has the form of (⋆), it clearly holds that zT |= ϕ because of T |= ϕ. This proves zT ∈ T k .
The previous lemma states that we can compute T k from T 0 k by generating orbits. Next we want to present and analyse an algorithm for enumerating those orbits. The results are given in Theorem 27. Lemma 26 Let U be a subspace of the Then B is a basis for U .
Proof First we show that any set A ⊆ U \ { 0} satisfying (1) is linearly independent. We conduct an induction over |A|. For |A| = 1 the claim is obvious. Because of (1) there exists an element a 0 ∈ A with last(a 0 ) > last(a) for all a 0 = a ∈ A. When considering the last(a 0 )-th component, clearly the equation λ a a, λ a ∈ F 2 has no solution. As A \ {a 0 } is linearly independent by induction hypothesis, it follows that A is linearly independent. Now assume that B does not generate U . We take an element s ∈ U \ span(B) with minimal last(s). As B is a maximal subset fulfilling (1), we have last(b) = last(s) for a suitable element b ∈ B. But then s − b ∈ U \ span(B) with last(s − b) < last(s) contradicts the minimality of s.
Theorem 27 Let T ∈ T k , k ∈ N. Then F n 2 T can be enumerated with delay O(k 3 n). Proof W.l.o.g. let T ∈ T 0 k . Note that T may have a nontrivial stabilizer subgroup so that duplicates occur when simply applying each z ∈ F n 2 to T . However, Proposition 13 states that we can enumerate the orbit of T without duplicates when applying a representative system for F n 2 /(F n 2 ) T . When taking F n 2 as a vector space over F 2 , the subspaces of F n 2 correspond to the subgroups of (F n 2 , +). In view of this any basis for a complement of the stabilizer subgroup (F n 2 ) T of T in F n 2 generates a representative system for F n 2 /(F n 2 ) T . Take a basis B of (F n 2 ) T as in Lemma 26. Set C := {e i : i ∈ {1, . . . , n} \ last(B)}, where e i denotes the i-th standard vector of F n 2 . By construction of C we can arrange the elements of B ∪ C so that the matrix containing these elements as columns has triangular shape with 1-entries on its diagonal. Consequently B ∪ C is a basis for F n 2 and C is a basis for a complement of (F n 2 ) T . Now it remains to construct B as desired. For s ∈ 2 Var(ϕ) ∼ = F n 2 we have s ∈ (F n 2 ) T ⇒ sT = T ⇒ s = s + 0 ∈ T. Hence we can compute (F n 2 ) T by checking sT = T for |T | = k elements in F n 2 . In fact it is enough to check sT ⊆ T as we have |sT | = |T |. We obtain B by inserting each element of (F n 2 ) T \ { 0} preserving (1) into B. This shows that Algorithm 1 outputs F n 2 T without duplicates. The delay is dominated by the precalculation delay, which is O(k 3 n). Note that we sort the k assignments of each team in ascending order before returning it.
Example 28 Let n = 3 and T = {000, 100, 010, 110}. Note that T satisfies the reduced formula from page 6 describing the robot soccer scenario. We compute the orbit Finally we would like to relate t k to t 0 k . The larger the quotient t k /t 0 k , the more computation costs are saved by generating orbits instead of computing T k immediately.
Theorem 29 Let k ∈ N with t k = 0. Then it holds that t k /t 0 k = 2 n /k.
Proof Because of t k = 0 and Lemma 23 it follows that t 0 k = 0. For this reason we can choose T ∈ T 0 k . We claim For any s ∈ 2 Var(ϕ) ∼ = F n 2 it holds that Consequently we have F n 2 T ∩ T 0 k = {sT : s ∈ T } =: T T. Let r, s ∈ T . Both elements yield the same team rT = sT iff s ∈ r(F n 2 ) T so that for any fixed r ∈ T we find exactly |r(F n 2 ) T | = |(F n 2 ) T | ways of expressing rT in the form of sT , where s ∈ T by (3). When iterating over the k elements sT , s ∈ T , each team in T T is counted |(F n 2 ) T | times. It follows that proving (2). By Lemma 23 we find a representative system R ⊆ T 0 k for the orbits of F n 2 T k . With Equation (2) and the Orbit-Stabilizer theorem (see Proposition 13) we obtain Example 30 Consider the reduced formula ϕ := =(x 1 , x 3 ) ∧ =(x 2 , x 3 ) from page 6. Then the orbits of T k , k ∈ N, and their corresponding stabiliser subgroups are given in Figure 1. Teams located in T 0 k are coloured red. Note that the amount of red teams in each orbit of T k matches k divided by the cardinality of the stabiliser subgroup. Furthermore we have

Constructing T 0 k
Now that we are able to construct all satisfying k-teams from a representative system, the next step is the construction of T 0 k . For this purpose the concept of coherence will prove useful.
(i) ⇒ (ii): Let T ∈ T k . Any subset of cardinality 2 contained in T 1 red or T 2 red is a subset of T . The 2-coherence of ϕ yields T i red |= ϕ for i ∈ {1, 2}. Furthermore 0 = s 1 ∈ T i red and |T i red | = k −1 holds. This gives us T 1 red , T 2 red ∈ T 0 k−1 . Again by the 2-coherence of ϕ we obtain that {s k−1 , s k } ∈ T 2 . Applying the group action F n 2 T 2 shows that { 0, s k−1 + s k } ∈ T 0 2 . (ii) ⇒ (i): First note that 0 ∈ T 1 red ⊂ T and |T | = |T 1 red |+1 = k. Assume T |= ϕ. Then by 2-coherence there exists a subset R ⊆ T with |R| = 2 and R |= ϕ. In particular it holds that for s ∈ L with s > r do Algorithm 2 computes the sets T 0 k by exploiting the previous lemma. In order to ensure fast list operations, we sort teams by the lexicographical order as given in Definition 18. When the assignments of each team are saved in ascending order-which is easy to guarantee-the cost of comparing two k-teams is O(kn). We do not store duplicates, restricting the size of lists containing teams to By managing those lists in AVL Trees presented in [1], the standard list operations as searching, insertion and deletion are realised in With these considerations in mind, we begin proving the correctness and performance of the algorithm.
, then it follows that T ∪ {s} ∈ T 0 k and s > max(T ). Proof We conduct an induction over k.
Induction basis (k = 2): Let T ∈ T 0 2 . It follows that T 1 red = { 0}. As we have As a consequence checking { 0, s} |= ϕ can be accomplished in linear time by evaluating a PL-formula of length O(|ϕ|) (where ∨ has the classical propositional disjunction semantics). Accessing the list D k [T ] for a team T is in O(k 2 n 2 ) by (5). When managing the list in an AVL Tree, the list operations are realised in O(log 2 n ) = O(n), which is contained in O(k 2 n 2 ).
As the decomposition for T ∈ T 0 k−1 into T ′ and s with s > max(T ′ ) is unique, applying Lemma 35 yields that the loop body of line 11 is invoked t 0 k−1 times. Taking into account that n ≤ |ϕ|, we obtain the claim by adding up all costs.
Example 38 We construct the sets T 0 k for the reduced formula ϕ := =(x 1 , x 3 ) ∧ =(x 2 , x 3 ) from Example 3.1. Trivially it holds that T 0 1 = {{000}}. When computing T 0 2 , we have to identify all nonzero assignments that satisfy (x 1 ∨ ¬x 3 ) ∧ (x 2 ∨ ¬x 3 ). Obviously, the satisfying assignments are 100, 010, 110 and 111. We obtain D 2 [{000}] = {100, 010, 110, 111}. Figure  2 illustrates the construction of the remaining lists and the resulting sets T 0 k . We are able to verify that the orbits presented in Example 30 are exactly those of T k , k ∈ N. Each orbit contains at least one element of T 0 k and every team in T 0 k can be recovered in one orbit of Figure 1. Algorithm 3: Enumerating satisfying teams in PDL − , ordered by cardinality Input: A team-based propositional formula ϕ as in Equation (⋆), k ∈ N Output: All teams T for ϕ with T |= ϕ, 1 ≤ |T | ≤ k simultaneously Compute T 0 ℓ by Algorithm 2; 10 if T 0 ℓ = ∅ then break;

The algorithm
Although by Corollary 37 Algorithm 2 does not perform in polynomial time on input k ∈ N, we can ensure polynomial delay when distributing its execution over the process of outputting all satisfying teams of cardinality k −1. For this reason we investigate the costs of computing T 0 k divided by t k−1 . With Corollary 37 and which is a transformation of the equation in Theorem 29, we obtain Consequently, the delay of Algorithm 3 is bounded by O(k 3 |ϕ| 2 ). Note that the delay of generating the orbits F n 2 T , which is O(k 3 n) by Theorem 27, and the cost of removing elements in T 0 k , which is O(k 2 n 2 ), are contained in O(k 3 |ϕ| 2 ).
Theorem 39 Algorithm 3 enumerates all satisfying teams T for ϕ with 1 ≤ |T | ≤ k without duplicates.
Proof It is easy to see that all dependencies in Algorithm 2 and 3 are resolved in time. By Proposition 11 and Lemma 23 every satisfying team is outputted at least once. By removing every outputted element in line 8 no orbit is outputted twice, preventing duplicates.
Finally, we conclude.

Consequences of sorting by cardinality
In the previous section we have seen that the restriction on polynomial teams is sufficient to obtain a DelayP-algorithm for PDL − . As we will see in this section, the restriction is not only sufficient, but also necessary when the output is sorted by its cardinality. Consequently, the algorithm presented above is optimal regarding output size.
Lemma 41 Let k ≥ 2 and ϕ(x 1 , . . . , Then for any team T = ∅ with T |= ϕ and |T | ≥ 3 it holds that T {x k } = 1. Proof Let T be a team with T |= ϕ and |T | ≥ 3. Set T x k =i := {s ∈ T : s(x k ) = i} for i ∈ {0, 1}. Assume that |T {x k } | = 1 does not hold. Then w.l.o.g. T x k =0 = ∅ and |T x k =1 | > 1. Take r ∈ T x k =0 . For any s ∈ T x k =1 it holds that {r, s} |= ϕ because ϕ is downward closed. In particular, {r, s} |= =(x i , x k ) for all i ∈ {1, . . . , k − 1}, yielding r(x i ) = s(x i ) because of r(x k ) = s(x k ). On that account s is uniquely determined by r, Theorem 42 Let f be a polynomial time computable function. Then it holds that Proof "⇐": immediately follows from Theorem 40.
"⇒": Let f / ∈ n O (1) . Assume that EnumTeamSize(PDL − , f ) ∈ DelayP holds via an algorithm with a delay bounded by n c , c ∈ N. Then there exists k ∈ N such that Let ϕ be as in Lemma 41. Obviously, there exist teams T 0 , T 1 ∈ T z with s(x k ) = i for all s ∈ T i , i ∈ {0, 1}. Since the elements in T z have to be outputted in succession and T {x k } = 1 for any T ∈ T z , we can choose T 0 and T 1 such that both teams are outputted in consecutive order. However, both teams differ in at least z bits describing the evaluation at x k . For this reason the delay is at least z > (4k) c ≥ (|ϕ|) c , contradicting that the delay is bounded by n c .
The trick of examining the symmetric difference of consecutive teams gives rise to the previous theorem. Unfortunately this trick cannot be applied to arbitrary orders and certainly fails for the lexicographical order. In order to prove this claim, consider Theorem 44 with S = 2 Var(ϕ) , X = T ∈ P 2 Var(ϕ) : T |= ϕ .
Theorem 44 Let S = {s 1 , . . . , s n } be a total ordered, finite set and X ⊆ P(S) be a downward closed set, meaning T ∈ X ⇒ R ∈ X ∀R ⊆ T. When X is ordered lexicographically in respect to the order on S, the symmetric difference △ between two consecutive elements in X is at most 3.
Proof W.l.o.g, we assume that {s i } ∈ X for all i ∈ {1, . . . , n}. We prove the claim by induction over n. The induction basis for n = 1 is obvious. Consider the induction step from n − 1 to n.
Set X i := {T ∈ X : s 1 , . . . , s i−1 / ∈ T, s i ∈ T }, X i := {T \{s i } : T ∈ X i } for i ∈ {1, . . . , n}. The subsets X i together with {∅} form a partition of X. Furthermore it is easy to see that the sets X i are downward closed and that T < T ′ for all T ∈ X i , T ′ ∈ X j with i < j.
By induction hypothesis the symmetric difference for consecutive elements in X i is at most 3. As the order on X i corresponds to the order on X i , the same applies to X i . It remains to check the consecutive elements located in different X i 's. For any element In fact, it holds that T ≤ 0 + 1 < 3, and max T ∈Xi T ≤ 2 + 1 = 3 ∀i ∈ {1, . . . , n − 1}.

Limiting memory space
Next we examine the memory usage of Algorithm 3. Throughout the execution, D 2 [{ 0}], D k and T 0 k have to be saved. However the size of those lists increases exponentially when raising the size of the outputted teams or the amount of variables occurring in the formula ϕ. By Equation (4) from page 11 Algorithm 3 requires space O(2 2 n ), respectively, O(2 n ) when fixing the parameter k. In fact, any algorithm that saves a representative system for the orbits of F n 2 T k cannot perform in polynomial space by the following theorem. For this reason we have to discard the group action of flipping bits when limiting memory space to polynomial sizes.
Theorem 45 Let 1 = k ∈ N and n ∈ N. We set ϕ := =(x 1 , x 2 , . . . , x n ). Then the amount of orbits of F n 2 T k is not polynomial in n.
Proof Note that each orbit of F n−1 2 on the set of all k-teams over n − 1 variables maps to an orbit of F n 2 T k by extending all assignments of a team so that x n is assigned to the same value. As we have for any function f : N → N, we may assume that ϕ is equivalent to 1 with |Var(ϕ)| = n. By the Cauchy-Frobenius lemma (see Proposition 14) the amount of orbits is at least |{T ∈ P 2 Var(ϕ) : |T | = k}| 2 n when neglecting all summands except the one for 0 ∈ F n 2 . That is why the number of orbits in T k has to be larger than 2 n k /2 n , which already increases exponentially in n. In the previous sections we had to limit the cardinality of outputted teams for obtaining polynomial delay. As the following theorem shows, this measure is necessary as well when demanding polynomial space.
Theorem 46 Let φ be any fragment of team-based propositional logic and f be a function with f / ∈ n O(1) such that for any n ∈ N there exists a formula ϕ n ∈ φ in n variables with at least 2 f (n) satisfying teams. Then it follows that EnumTeam(φ) cannot be enumerated in polynomial space.
Proof Any enumeration algorithm enumerating Sol(ϕ n ) has to output 2 f (n) different teams. The same amount of configurations have to be adopted. In order to distinguish these, the configurations are encoded by at least f (n) bits. However, when considering a RAM performing in polynomial space, the contents of all registers may be encoded by a polynomial amount of bits. For this reason a RAM enumerating Sol(ϕ n ) cannot perform in polynomial space.
Corollary 47 The problem EnumTeam(PDL − ) cannot be enumerated in polynomial space.
Proof Let n ∈ N. Set ϕ n := =(x 1 , x 2 , . . . , x n ). All teams T with s(x n ) = 0 for all assignments s ∈ T satisfy ϕ n . For this reason at least 2 2 n−1 satisfying teams exist. Because of 2 n−1 / ∈ n O(1) , the claim follows by the previous theorem.
We now present an algorithm enumerating EnumTeamSize(PDL − , f ) for any f ∈ n O(1) in polynomial space. Compared to Algorithm 3, it saves memory space by recomputing the satisfying teams of lower cardinality instead of storing them in a list. As a downside we have to accept incremental delays.
Then, we define a unary relation hasNext on 2 Var(ϕ) by s ∈ hasNext if and only if ∃t ∈ 2 Var(ϕ) : s < t. For any s ∈ hasNext let next(s) be the unambiguous assignment such that s < next(s) holds but s < t < next(s) does not hold for any assignment t. We denote the smallest element in 2 Var(ϕ) by s first . The largest element is denoted by s last . As already mentioned when defining the lexicographical order, we assume that hasNext, next and s first may be determined in O(n) time. if |T | = k and T |= ϕ then output T ; Let k ∈ N. We write M k for the set of teams T is assigned to during the k-th iteration of the outer loop of Algorithm 4.
Lemma 49 Let S ∈ M k be a nonempty set such that s := max(S) ∈ hasNext. Then it follows that S \ {s} ∪ {next(s)} ∈ M k . In particular, we have S \ {s} ∪ {t} ∈ M k for all t ∈ 2 Var(ϕ) with t ≥ s.
Proof We conduct an induction over k − |S|.
Induction basis (|S| = k): Because of |S| ≮ k and s ∈ hasNext line 7 is executed and T is assigned to S \ {s} ∪ {next(s)}.
Induction step (|S| + 1 → |S|, 1 ≤ |S| < k): If S |= ϕ, line 7 is executed as before and the claim follows. If S |= ϕ, line 6 is executed. It follows that S ∪ {next(s)} ∈ M k . By induction hypothesis it follows that S ∪{s last } ∈ M k . When executing the body of the while loop with T assigned to S ∪ {s last }, the block beginning at line 9 is executed, assigning T to S \ {s} ∪ {next(s)}.
Lemma 50 Let k ∈ N and S be a team with S |= ϕ and |S| ≤ k. Then it follows that S ∈ M k .
Proof We conduct an induction over |S|.
Induction step (|S|− 1 → |S|, 1 < |S| ≤ k): Let s = max(S). Since ϕ is downward closed, it follows that S \ {s} |= ϕ. The induction hypothesis yields S \ {s} ∈ M k . Consequently the while loop is executed with T assigned to S \ {s}. Line 7 is executed, assigning T to a team S \ {s} ∪ {t}, where t is an appropriate assignment with t ≤ s. Lemma 49 yields S ∈ M k .
Lemma 51 Let f ∈ n O(1) be a polynomial time computable function. Then there exists a polynomial p such that the i-th delay of Algorithm 4 is bounded by i 2 p(|ϕ|).
Proof Note that the delay is constant when outputting the 2 n singletons that satisfy ϕ trivially. Hence we assume that i ≥ 2 n . It is easy to verify that any team T is assigned to is lexicographically larger than the previous value for T . For this reason the number of iterations of the inner while loop is bounded by |M k |.
As T is not assigned to teams with greater cardinality when the current value for T does not satisfy ϕ, it follows that S \ {max(S)} |= ϕ for any S ∈ M k with |S| > 1. Consequently Let S be the (i + 1)-th outputted element. Set k = |S|. We have S ∈ M k and |S| > 1. By outputting teams of lower cardinality first we guarantee that i ≥ k−1 l=1 t l . Furthermore S is outputted in the k-th iteration of the outer loop. Consequently the inner while loop has been executed at most k · i 2 times before outputting S. Since k is bounded by a polynomial in |ϕ|, by Lemma 48 it follows that the body of the inner while loop can be executed in polynomial time. We conclude that the i-th delay is bounded by i 2 p(|ϕ|), where p is an appropriate polynomial. Now let i be the total amount of outputted teams. Then the number of iterations of the inner while loop is bounded by Accordingly, we can choose p such that even the postcalculation delay is bounded by i 2 p(|ϕ|).
Theorem 52 Let f ∈ n O(1) be a polynomial time computable function. Then Algorithm 4 is an IncP-algorithm for EnumTeamSize(PDL − , f ) which performs in polynomial space.
Proof The algorithm saves only one team of cardinality ≤ f (|ϕ|) and one assignment for which (f (|ϕ|) + 1) registers are required. By Lemma 50 it is clear that the algorithm outputs the satisfying teams ordered by cardinality. Lemma 51 states that the delays conform to the definition of IncP.

Conclusion
In this paper we have shown that the task of enumerating all satisfying teams of a given propositional dependence logic formula without split junction is a hard task when sorting the output by its cardinality, i.e., only for polynomially sized teams, we constructed a DelayP algorithm. In the unrestricted cases, we showed that the problem is in DelayFPT when the parameter is chosen to be the team size. Further, we explained that the algorithm is optimal regarding its output size and pointed out that any algorithm saving a representative system for the orbits of F n 2 T k cannot perform in polynomial space. Furthermore, we want to point out that allowing for split junction (and accordingly talking about full PDL) will not yield any DelayFPT or DelayP algorithms in our setting unless P = NP.
Lastly, we would like to mention that the algorithms enumerating orbits and the satisfying teams, respectively, can be modified such that satisfying teams for formulas of the form ϕ 1 ϕ 2 · · · ϕ r where r ∈ N, ϕ i ∈ PDL − can be enumerated. The idea is to merge the outputs Sol(ϕ i ), i ∈ {1, . . . , r}, which is possible in polynomial delay if the output for each ϕ i is pre-sorted according to a total order. By now, we presented an algorithm that sorts the output by cardinality. It remains open to identify the enumeration complexity of Poor Man's Propositional Dependence Logic when other orders, e.g., the lexicographical order, are considered. Furthermore, one can investigate the conjunction free fragment of PDL, permitting the split junction operator but no conjunction operator. Similarly to the Poor Man's fragment, one can assume that the group action of flipping bits is an invariant for satisfying teams when formulas are simplified properly. Nonetheless, the 2-coherence property is lost so that the algorithm for constructing the sets T 0 k fails.