Marco Voigt

A fine-grained hierarchy of hard problems in the separated fragment

Recently, the separated fragment (SF) has been introduced and proved to be decidable. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. The known upper bound on the time required to decide SF's satisfiability problem is formulated in terms of quantifier alternations: Given an SF sentence ∃ z ∀ x1∃ y1 . . . ∀ xn∃ yn. ψ in which ψ is quantifier free, satisfiability can be decided in nondeterministic n-fold exponential time. In the present paper, we conduct a more fine-grained analysis of the complexity of SF-satisfiability. We derive an upper and a lower bound in terms of the degree ∂ of interaction of existential variables (short: degree)a novel measure of how many separate existential quantifier blocks in a sentence are connected via joint occurrences of variables in atoms. Our main result is the k-NEXPTIME-completeness of the satisfiability problem for the set SF ∂≤k of all SF sentences that have degree k or smaller. Consequently, we show that SF-satisfiability is non-elementary in general, since SF is defined without restrictions on the degree. Beyond trivial lower bounds, nothing has been known about the hardness of SF-satisfiability so far.

Introduction

In [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF] the separated fragment (SF) of firstorder logic with equality is introduced. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. (Topmost existential quantifier blocks are exempt from this rule.) SF properly generalizes both the Bernays-Schönfinkel-Ramsey (BSR) fragment (∃ * ∀ * -sentences with equality) and the relational monadic fragment without equality (MFO). Still, the satisfiability problem for SF is decidable.

In computational logic formulas are often classified based on the shape of quantifier prefixes. There is a wealth of results that separate decidable first-order formulas from undecidable ones in this fashion, see [START_REF] Börger | The Classical Decision Problem[END_REF] for references. The definition of the BSR fragment is only one example. In the context of computational complexity, hierarchies are defined, such as the polynomial hierarchy, where the hardness of problems is assumed to grow with the number of quantifier alternations that are allowed to occur.

Although the definition of SF breaks with the paradigm of restricting quantifier prefixes, the known upper bound on the complexity of SF-satisfiability is again based on quantifier prefixes: Deciding whether an SF sentence ϕ := ∃ z ∀ x 1 ∃ y 1 . . . ∀ x n ∃ y n .ψ with quantifier-free ψ is satisfiable requires a nondeterministic computing time that is at most n-fold exponential in the length of ϕ (cf. Theorem 17 in [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF]). On the one hand, we complement this result with a corresponding lower bound in the present paper. That is, we show that SF-satisfiability is indeed nonelementary. On the other hand, we derive a refined upper bound that is based on the degree ∂ of interaction of existential variables. An overview of the resulting hierarchy of complete problems is depicted in Figure 1. Intuitively, ϕ exhibits a degree ∂ ϕ = k, if variables from k distinct existential quantifier blocks interact. We say that two variables x, y interact, if they occur together in at least one atom or if there is a third variable z that interacts with both x and y (i.e. the property is transitive). For instance, in the SF sentence ∀x 1 ∃y 1 v 1 ∀x 2 ∃y 2 v 2 ∀x 3 ∃y 3 v 3 . P (x 1 , x 2 , x 3 ) ∧ ¬Q(y 1 , y 3 ) ∨ P (y 2 , v 2 , v 3 ) ∨ ¬Q(y 3 , v 1 ) the sets {y 1 , y 3 , v 1 } and {y 2 , v 2 , v 3 } form the maximal sets of interacting existential variables. Since each of these sets contains variables from at most two distinct quantifier blocks, the formula exhibits a degree ∂ = 2.

In Section 4.1, and in particular in Theorem [START_REF] Plaisted | Complete Problems in the First-Order Predicate Calculus[END_REF], we observe that the satisfiability problem for SF ∂≤k -the set of all SF sentences ϕ with ∂ ϕ ≤ k-lies in k-NEXPTIME. It is worth mentioning that this result adequately accounts for the known complexity of MFO-satisfiability. For 978-1-5090-3018-7/17/$31.00 c 2017 IEEE every MFO sentence ϕ we trivially have ∂ ϕ = 1, since all occurring predicate symbols have an arity of at most one. Theorem 13 entails that MFO-satisfiability is in NEXPTIME, which is well known. Still, this bound is not reproducible with the analysis of the complexity of SF-satisfiability conducted in [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF].

Apparently, non-elementary satisfiability problems are not very widespread among the decidable fragments of classical fist-order logic known today. We show in Section 5 that SF falls into this category. To the present author's knowledge, the only known companion in this respect is the fluted fragment (FL). Indeed, Pratt-Hartmann, Szwast, and Tendera show in [START_REF] Pratt-Hartmann | Quine's Fluted Fragment is Non-Elementary[END_REF] that satisfiability of fluted sentences with at most 2k variables is k-NEXPTIME-hard. Moreover, they argue that satisfiability of fluted sentences with at most k variables lies in k-NEXPTIME. Although a significant gap between these lower and upper bounds remains to be closed, the fluted fragment seems to comprise a similar hierarchy of hard problems as SF does.

Another characteristic of SF is that it enjoys a small model property. More precisely, given an SF sentence ϕ, one can compute a positive integer n that depends on the degree ∂ ϕ and the length of ϕ such that, if there is a model of ϕ at all, then there also is a model whose domain contains at most n elements. Many first-order fragments are known to enjoy a small model property. The BSR fragment and MFO are among the classical ones (see [START_REF] Börger | The Classical Decision Problem[END_REF] for references). More recently defined fragments include the two-variable fragment (FO [12], [START_REF] Grädel | On the Decision Problem for Two-Variable First-Order Logic[END_REF], the fluted fragment (FL) [START_REF] Quine | On the Limits of Decision[END_REF], [START_REF] Quine | The Variable[END_REF], [START_REF] Pratt-Hartmann | Quine's Fluted Fragment is Non-Elementary[END_REF], the guarded fragment (GF) [START_REF] Andréka | Modal Languages and Bounded Fragments of Predicate Logic[END_REF], [START_REF] Grädel | On the Restraining Power of Guards[END_REF], the guarded negation fragment (GNF) [START_REF] Bárány | Guarded Negation[END_REF], and the uniform one-dimensional fragment (UF 1 ) [START_REF] Kieronski | Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality[END_REF]. While GNF and UF 1 are incomparable, GNF extends GF, and UF 1 can be considered as a generalization of FO 2 . Guarded fragments and the two-variable fragment have received quite some attention due to the fact that modal logics have natural translations into them. As a continuation of that theme, we shall see in Section 3.1 how classes of sentences enjoying a small model property can be effectively translated into subclasses of SF. During the translation process the length of formulas increases by a factor that is logarithmic in the size of small models of the original. One benefit of translating non-SF sentences into SF sentences is that in SF one can natively express concepts such as transitivity and basic counting quantifiers (Proposition 5). This is not always possible in other fragments enjoying a small model property. For example, transitivity cannot be expressed in FO 2 , GF, and FL.

Summing up, the main contributions are: (i) Based on the novel concept of the degree of interaction of existential variables, we substantially refine the existing analysis of the time required to decide SF-satisfiability. More concretely, we show that a satisfiable SF sentence ϕ with ∂ ϕ = k has a model whose domain is of a size that is at most k-fold exponential in the length of ϕ (Section 4, Theorem 13). With this refined approach we can close the complexity gap for the class of strongly separated sentences (Corollary 15) that was left open in [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF]. Moreover, the complexity of MFO can be explained in the refined framework. (ii) We complement the complexity analysis with corresponding lower bounds in two respects. We first derive a lower bound on the length of shortest BSR sentences that are equivalent to a given SF sentence (Section 4.2, Theorem 16). In Section 5, we prove k-NEXPTIME-hardness of satisfiability for the class of SF sentences ϕ with ∂ ϕ = k (Theorem 21). Since SF is in general defined without restrictions on the degree ∂ ϕ , our result implies that SF-satisfiability is non-elementary. (iii) We devise a simple translation from classes of first-order sentences that enjoy a small model property into SF (Proposition 4). Moreover, we argue that SF can express basic counting quantifiers (Proposition 5).

Due to space limitations, we mostly resort to sketches of proofs. The interested reader is referred to the extended version of the present paper [START_REF] Voigt | A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment[END_REF].

Preliminaries

We mainly reuse the basic notions from [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF]. We repeat the definition of necessary concepts and notation for the sake of completeness.

We consider first-order logic formulas. The underlying signature shall not be mentioned explicitly, but will become clear from the current context. For the distinguished equality predicate we use ≈. We follow the convention that negation binds strongest, that conjunction binds stronger than disjunction, and that all of the aforementioned bind stronger than implication. The scope of quantifiers shall stretch as far to the right as possible. By len(•) we denote a reasonable measure of the length of formulas satisfying len(ϕ → ψ) = len(¬ϕ ∨ ψ) and len(ϕ

↔ ψ) = len((¬ϕ ∨ ψ) ∧ (ϕ ∨ ¬ψ)).
We write ϕ(x 1 , . . . , x m ) to denote a formula ϕ whose free variables form a subset of {x 1 , . . . , x m }. In all formulas we tacitly assume that no variable occurs freely and bound at the same time and that no variable is bound by two different occurrences of quantifiers, unless explicitly stated otherwise. For convenience, we sometimes identify tuples x of variables with the set containing all the variables that occur in x. We write vars(ϕ) to address the set of all variable symbols that occur in ϕ. Similarly, consts(ϕ) denotes the set of all constant symbols in ϕ. We denote substitution by ϕ x/t if every free occurrence of x in ϕ is to be substituted with the term t.

A literal is an atom or a negated atom, and a clause is a disjunction of literals. We say that a formula is in conjunctive normal form (CNF), if it is a conjunction of clauses, possibly preceded by a quantifier prefix. A formula in CNF is Horn if every clause contains at most one non-negated literal. It is Krom if every clause contains at most two literals at all.

A sentence ϕ := ∀ x 1 ∃ y 1 . . . ∀ x n ∃ y n .ψ is in standard form, if it is in negation normal form (i.e. every negation symbol occurs directly before an atom) and ψ is quantifier free, contains exclusively the Boolean connectives ∧, ∨, ¬, and does not contain non-constant function symbols. The tuples x 1 and y n may be empty, i.e. the quantifier prefix does not have to start with a universal quantifier, and it does not have to end with an existential quantifier. Moreover, we require that every variable occurring in the quantifier prefix does also occur in ψ.

As usual, we interpret a formula ϕ with respect to given structures. A structure A consists of a nonempty universe U A (also: domain) and interpretations f A and P A of all considered function and predicate symbols, respectively, in the usual way. Given a formula ϕ, a structure A, and a variable assignment β, we write A structure A is a substructure of a structure B (over the same signature) if (1) U A ⊆ U B , (2) c A = c B for every constant symbol c, (3)

P A = P B ∩ U m
A for every m-ary predicate symbol P , and (4) f A (a 1 , . . . , a m ) = f B (a 1 , . . . , a m ) for every m-ary function symbol f and every m-tuple a 1 , . . . , a m ∈ U m A . The following is a standard lemma, see, e.g., [START_REF] Ebbinghaus | Mathematical Logic[END_REF] We use the notation [k] to abbreviate the set {1, . . . , k} for any positive integer k. Moreover, P shall be used as the power set operator, i.e. PS denotes the set of all subsets of a given set S. Finally, we need some notation for the tetration operation. We define 2 ↑k (m) inductively: 2 ↑0 (m) := m and 2 ↑k+1 (m) := 2 (2 ↑k (m)) .

The separated fragment

Let ϕ be a first-order formula. We call two disjoint sets of variables X and Y separated in ϕ if and only if for every atom A occurring in ϕ we have vars(A) ∩ X = ∅ or vars(A) ∩ Y = ∅. Definition 3 (Separated fragment (SF), [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF]). The separated fragment (SF) of first-order logic consists of all existential closures of prenex formulas without non-constant function symbols in which existentially quantified variables are separated from universally quantified ones. More precisely, SF consists of all first-order sentences with equality but without non-constant function symbols that are of the form ∃ z ∀ x 1 ∃ y 1 . . . ∀ x n ∃ y n . ψ, in which ψ is quantifier-free, and in which the sets x 1 ∪. . .∪ x n and y 1 ∪ . . . ∪ y n are separated.

The tuples z and y n may be empty, i.e. the quantifier prefix does not have to start with an existential quantifier and it does not have to end with an existential quantifier either.

Notice that the variables in z are not subject to any restriction concerning their occurrences.

In [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF] the authors show that the satisfiability problem for SF sentences (SF-satisfiability) is decidable. Before we start investigating the complexity issues related to SF-satisfiability, we elaborate on the expressiveness of SF.

Expressiveness

Every SF sentence is equivalent to a BSR sentence ( [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF], Lemma 6). We shall outline in Section 4 how to analyze the blow-up that we have to incur during this translation process and how it depends on the degree of interaction of existential variables. Since the BSR fragment enjoys a small model property (cf. Proposition 6), SF inherits the small model property from BSR. However, regarding the size of minimal models of satisfiable formulas, SF sentences are much more compact. While satisfiable BSR sentences have models whose domain is linear in the length of the formula, satisfiable SF sentences can enforce domains of a size that cannot be bounded from above by a finite tower of exponentials. We provide first evidence for this fact in Theorem 16, where we give a non-elementary lower bound on the length of equivalent BSR sentences. This lower bound even applies to the SF-Horn-Krom subfragment of SF. Moreover, we exploit the capability of SF sentences ϕ to enforce models of ∂ ϕ -fold exponential size in the proof of the k-NEXPTIME-hardness of SFsatisfiability (for every k ≥ 1).

Apart from compactness of representation, and from the perspective of satisfiability, all first-order fragments that enjoy small model properties share a common ground of expressiveness. Neglecting efficiency, every sentence ϕ from such a fragment can be effectively translated into a (finite) propositional formula φ in such a way that from a satisfying variable assignment for φ one can straightforwardly reconstruct a (Herbrand) model of ϕ. The reason is simply that universal quantification can then be understood as finite conjunction (over a finite domain) and existential quantification can be conceived as finite disjunction.

The following proposition illustrates why SF is to some extent prototypical for first-order fragments that enjoy a small model property.

Proposition 4. Consider any nonempty class C of first-order formulas without non-constant function symbols for which we know a computable mapping f : C → N such that every satisfiable ϕ in C has a model of size at most f (ϕ). Then there exists an effective translation T from C into SF such that for every ϕ ∈ C, (a) every model of T (ϕ) is also a model of ϕ, (b) every model of ϕ whose size is at most f (ϕ) can be extended to a model of T (ϕ) over the same domain, and (c) the length of

T (ϕ) lies in O len(ϕ) • log f (ϕ) • log log f (ϕ) .
Proof. We outline the translation T for some given input sentence ϕ, which we assume to be in negation normal form (without loss of generality). Let m := log 2 f (ϕ) and let Q 1 , . . . , Q m be unary predicate symbols that do not occur in ϕ. For all terms s, t we define s ≈ t as abbreviation of

m i=1 Q i (s) ↔ Q i (t).
In order to restrict the domain to 2 m elements, we conjoin the formula χ fin := ∀xy. x ≈ y → x ≈ y. Since in any structure A there are at most 2 m domain elements that can be distinguished by their membership in the sets

Q A 1 , . . . , Q A m , it is clear that A |= χ fin entails |U A | ≤ 2 m .
( * ) Let A be any structure, let β be any variable assignment over A's domain, and let s, t be two terms. If A |= χ fin holds, then we get

A, β |= s ≈ t if and only if A, β |= s ≈ t.
This means, if we restrict our attention to domains with at most 2 m domain elements, we can now use a separated form of equality. ( * * ) Let ψ be any first-order formula and let v be some variable that does not occur in ψ. Then ψ is equivalent to ∀v. u ≈ v → ψ u/v . We can transform ϕ into an equivalent sentence ϕ by consecutively replacing each subformula of the form ∃y.ψ in ϕ with ∃y∀v. y ≈ v → ψ y/v , where we assume v to be fresh (one fresh variable for every replaced subformula). Consequently, every atom in ϕ that is not an equation contains exclusively universally quantified variables. Moreover, ( * * ) implies that ϕ and ϕ are equivalent.

Let ϕ be the result of replacing all equations y ≈ v, v ≈ y in ϕ in which y is existentially quantified and v universally quantified with the formula y ≈ v. We then set ϕ SF := χ fin ∧ ϕ . By ( * ), any model of ϕ SF is also a model of ϕ.

Conversely, any model A of ϕ that has at most 2 m domain elements can be converted into a model B of ϕ SF by defining the relations Q B 1 , . . . , Q B m in an appropriate way.

The ϕ SF in the above proof belongs to a subfragment of SF that we call strongly separated (cf. Definition 14) and whose satisfiability problem is complete for NEXPTIME (cf. Corollary 15).

Unfortunately, the translation methodology of Proposition 4 does not help in the quest for new decidable first-order fragments. The reason is simply that we already need arguments leading to a small model property before we can start the translation process, as we need information about the size of the models that have to be considered. Nevertheless, such translations can be useful in view of the expressiveness of SF that other firstorder fragments, such as FO 2 , the fluted fragment, and GF, lack. For instance, SF sentences can naturally express the axioms of equivalence, most prominently, transitivity. Hence, fundamental and interesting properties of predicates that have to be assumed at the meta-level when dealing with less expressive logics can be formalized directly in SF. Moreover, basic counting quantifiers can be defined natively in SF and do not have to be introduced via special operators. More precisely, given any formula ∃ ≥n y. ϕ with positive n and without nonconstant function symbols, its standard translation ∃y 1 . . . y n . n i=1 ϕ y/y i ∧ i<j y i ≈ y j is not in conflict with the separateness conditions of SF's definition, if the set {y 1 , . . . , y n } is separated in ϕ from the set of universally quantified variables. Proposition 5. Counting quantifiers ∃ ≥n with positive integer n are expressible in SF.

Basic complexity considerations

We first recall the well-known small model properties of SF's subfragments BSR and MFO (see [START_REF] Börger | The Classical Decision Problem[END_REF] for references). Proposition 6. Let ϕ := ∃ z ∀ x.ψ be a satisfiable BSR sentence, i.e. ψ is quantifier free and does not contain non-constant function symbols. There is a model

A |= ϕ such that |U A | ≤ max | z| + |consts(ϕ)|, 1 .
We make use of this property when we derive an upper bound on the size of small models for satisfiable SF sentences, as our approach will be based on an effective translation of SF sentences into equivalent BSR sentences. Proposition 7. Let ϕ := ∃ z ∀ x 1 ∃ y 1 . . . ∀ x n ∃ y n .ψ be a satisfiable monadic sentence without equality and without non-constant function symbols, i.e. all predicate symbols in ϕ are of arity 1. Moreover, assume that ϕ contains k distinct predicate symbols. There is a model

A |= ϕ such that |U A | ≤ 2 k .
Notice that the shape of the quantifier prefix does not contribute to the upper bound.

The following lemma links bounds on the size of models with the computing time that is required to decide satisfiability.

Lemma 8 (cf. [START_REF] Börger | The Classical Decision Problem[END_REF], Proposition 6.0.4). Let ϕ be a first-order sentence in prenex normal form containing n universally quantified variables. The question whether ϕ has a model of cardinality m can be decided nondeterministically in time p m n • len(ϕ) for some polynomial p.

With this lemma at hand, it is enough to prove a small model property for a given class of firstorder sentences, in order to bound the worst-case time complexity of the corresponding satisfiability problem from above. This is exactly what the authors of [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF] have done for SF. Proposition 9 ([17], Theorem 17). Let ϕ := ∃ z ∀ x 1 ∃ y 1 . . . ∀ x n ∃ y n .ψ be an SF sentence for some quantifier-free ψ. There is some equivalent BSR sentence ∃ u ∀ v.ψ in which the number of occurring constant symbols plus the number of existential quantifiers is at most len(ϕ)+n•len(ϕ)• 2 ↑n (len(ϕ))

n . As a result, satisfiability of ϕ can be decided nondeterministically in time that is at most n-fold exponential in len(ϕ).

Clearly, applying this result to an MFO sentence substantially overshoots the actual worst-case time requirements. To stress it again, the notion of the degree of interaction is a remedy to this sort of inaccuracies, as we shall see in Section 4.

A special case that is worth considering, before we investigate the complexity of full SF, is the class of SF sentences that do not contain universal quantifiers. This species of formulas coincides with the purely existential fragment of first-order logic without non-constant function symbols, and it is a close relative of propositional logic. Recall that SAT is NP-complete [START_REF] Cook | The Complexity of Theorem-Proving Procedures[END_REF], Horn-SAT is P-complete [START_REF] Kasif | On the Parallel Complexity of Some Constraint Satisfaction Problems[END_REF], [START_REF] Plaisted | Complete Problems in the First-Order Predicate Calculus[END_REF], and 2SAT is NL-complete [START_REF] Jones | New Problems Complete for Nondeterministic Log Space[END_REF]. Proposition 10.

(i) Satisfiability for the class of SF sentences without universal quantifiers is NP-complete.

(ii) Satisfiability for the class of SF-Horn sentences without universal quantifiers is Pcomplete. (iii) Satisfiability for the class of SF-Krom sentences without universal quantifiers and without equality is NL-complete.

Translation of SF sentences into BSR sentences

In this section, we analyze the transformation process from SF into the BSR fragment from the perspective of the degree of interaction of existential variables. Our aim is to derive upper and lower bounds on the length of the resulting BSR-formulas. Roughly speaking, in the first phase of the translation process all quantifiers are moved inwards as far as possible (cf. the proof of Lemma 12). In order to do so, we first transform the sentence in question into a formula in CNF. After that, we employ the well-known rules of miniscoping (cf. Lemma 2), supplemented by the rule formulated in the following lemma.

Lemma 11. Let I and K i , i ∈ I, be sets that are finite, nonempty, and pairwise disjoint. The elements of these sets serve as indices. Let

ϕ := ∃ y. i∈I χ i ( z) ∨ k∈Ki η k ( y, z)
be some first-order formula where the χ i and the η k denote arbitrary subformulas that we treat as indivisible units in what follows. We say that f : I → i∈I K i is a selection function if for every i ∈ I we have f (i) ∈ K i . We denote the set of all selection functions of this form by F.

Then ϕ is equivalent to ϕ :=

S ⊆ I S = ∅ i∈S χ i ( z) ∨ f ∈F ∃ y. i∈S η f (i) ( y, z) .
Proof sketch. The proof of this lemma follows a conceptually simple strategy. Using the distributivity of ∧ over ∨, we first transform ϕ into a disjunction of conjunctions of the indivisible units χ i ( z) and η k ( y, z). Then, exploiting the equivalences in Lemma 2, we push the existential quantifier block ∃ y inwards such that it only binds conjunctions of units η k ( y, z). This is possible, because none of the variables in y occurs in any of the χ i ( z). From this point on, we treat the newly emerged subformulas ∃ y. k η k ( y, z) as if they were indivisible. We then transform the formula back into a conjunction of disjunctions of indivisible units, this time using the distributivity of ∨ over ∧. It then remains to show that the result of this transformation exhibits a highly redundant structure and is actually equivalent to ϕ .

4.1. Degree of interaction of existential variables and the size of small models Consider the formula ϕ := ∃ z ∀ x 1 ∃ y 1 . . . ∀ x n ∃ y n .ψ in standard form in which ψ is quantifier free and in which the sets x := x 1 ∪ . . . ∪ x n and y := y 1 ∪ . . . ∪ y n are separated. In addition, we assume that x 1 and y 1 are nonempty. The tuple z, on the other hand, may be empty.

For any j ∈ [n] and any variable y ∈ y j we say that y is a level-j variable, denoted lvl(y) = j.

For any nonempty set Y ⊆ y of existentially quantified variables and any positive integer k we say that Y has degree k in ϕ, denoted ∂ Y,ϕ = k, if k is the maximal number of distinct variables y 1 , . . . , y k ∈ Y that belong to different levels in ϕ, i.e. lvl(y 1 ) < . . . < lvl(y k ). We say that ϕ's degree of interaction of existential variables (short: degree) is k, denoted ∂ ϕ = k, if k is the smallest positive integer such that we can partition y into m > 0 parts Y 1 , . . . , Y m that are all pairwise separated in ϕ and for which k = max k j ∂ Yj ,ϕ = k j , 1 ≤ j ≤ m . Sentences ϕ := ∃ z ∀ x. ψ in standard form with quantifier-free ψ are said to have degree zero, i.e. ∂ ϕ = 0, if x is empty and we define ∂ ϕ = 1 if x is nonempty. Lemma 12. Let ϕ := ∃ z ∀ x 1 ∃ y 1 . . . ∀ x n ∃ y n .ψ be an SF sentence of positive degree ∂ ϕ in standard form. Let L ϕ ( y) denote the set of all literals in ϕ that contain at least one variable y ∈ y := y 1 ∪ . . . ∪ y n . There exists a sentence ϕ BSR = ∃ z ∃ u ∀ v.ψ BSR in standard form with quantifierfree ψ BSR that is equivalent to ϕ and contains at most

| z| + | y| • ∂ ϕ • 2 ↑∂ϕ (|L ϕ ( y)|)
∂ϕ leading existential quantifiers.

Proof sketch. Let x := x 1 ∪. . .∪ x n . We transform ϕ into CNF and then apply Lemma 11 and the rules of miniscoping given in Lemma 2 to push all quantifier blocks inwards. Since the sets x and y are separated in ϕ, these operations can be performed in such a way that in the resulting formula ϕ no universal quantifier lies within the scope of any existential quantifier (other than the ones in ∃ z) and vice versa. After removing redundant parts from ϕ , the depth of nestings of existential quantifier blocks (interspersed with conjunctive connectives in ϕ 's syntax tree) can be upper bounded by ∂ ϕ . As a consequence, ϕ contains at most 2 ↑∂ϕ (|L ϕ ( y)|) distinct subformulas that are of the form ∃y.ψ and do not lie within the scope of any quantifier.

After further transformations, we obtain a formula

ϕ := k χ k ( x) ∧ r k η r k ( y)
where the r k range over at most 2 ↑∂ϕ (|L ϕ ( y)|) indices. Moreover, every constituent

r k η r k in ϕ contains at most | y| • ∂ϕ k =1 ∂ϕ d=k 2 ↑d (|L ϕ ( y)|
) occurrences of existential quantifiers. Since these existential quantifiers distribute over the topmost disjunction when we move them outwards to the front of the sentence ϕ , and since the universal quantifiers in the χ k may also be moved back outwards, one can show that ϕ is equivalent to some BSR sentence with at most

| y| • ∂ ϕ • 2 ↑∂ϕ (|L ϕ ( y)|)
∂ϕ leading existential quantifiers.

Proposition 6 now entails that any satisfiable SF-sentence ϕ has a model of size at most

len(ϕ) + len(ϕ) • ∂ ϕ • 2 ↑∂ϕ (len(ϕ)) ∂ϕ . (1)
Theorem 13. Let k be any positive integer. The satisfiability problem for the class of SF sentences ϕ in standard form with degree ∂ ϕ ≤ k can be decided in nondeterministic k-fold exponential time.

Together with Proposition 10(i), this establishes the upper bounds depicted in Figure 1.

In cases where ∂ ϕ = 1, Expression (1) simplifies to len(ϕ) + len(ϕ) • 2 len(ϕ) . The syntactic class of sentences satisfying this property is called strongly separated in [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF].

Definition 14 ( [17]

). Let ϕ := ∀ x 1 ∃ y 1 . . . ∀ x n ∃ y n .ψ be an SF sentence and assume that ψ is quantifier free. We say that ϕ belongs to the strongly separated fragment (SSF) if and only if the sets x := x 1 ∪ . . . ∪ x n and y 1 , . . . , y n are all pairwise separated in ϕ.

Since MFO and BSR sentences fall into this syntactic category, and since their decision problem is known to be NEXPTIME-hard, we obtain the following corollary.

Corollary 15. The satisfiability problem for SSF is NEXPTIME-complete.

Notice that the presented method can explain the asymptotic complexity of MFO-satisfiability and yields a reasonable upper bound on the size of small models of satisfiable MFO sentences. This works in spite of the fact that monadic sentences may contain arbitrarily nested alternating quantifiers. This is a considerable improvement compared to the methods used in [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF].

Let ϕ be any SF sentence with the maximally possible degree ∂ ϕ = n, where n is the number of occurring ∀∃-alternations. Then the upper bound shown in Expression (1) regarding the number of elements in small models fits the corresponding result entailed by Proposition 9. As one consequence, Theorem 13 in the present paper subsumes Theorem 17 in [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF]. Moreover, Corollary 15 improves the double exponential upper bound on SSFsatisfiability given in Theorem 15 in [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF]. Finally, it is worth noticing that all SF sentences with the quantifier prefix ∃ * ∀ * ∃ * ∀ * belong to the strongly separated fragment. Hence, Corollary 15 subsumes Theorem 14 in [START_REF] Sturm | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated[END_REF]. The latter stipulates NEXP-TIME-completeness of SF sentences with quantifier prefix ∃ * ∀ * ∃ * . Clearly, the refined analysis based on the degree of interaction of existential variables, rather than the number of quantifier alternations, yields significantly tighter results in many cases.

Lower bounds on the length of equivalent BSR formulas

Before we derive lower bounds on the time that is required to decide SF-satisfiability in the worst case, we establish lower bounds on the length of the results of the translation from SF into the BSR fragment.

Theorem 16. There is a class of SF sentences that are Horn and Krom such that for every positive integer n the class contains a sentence ϕ of degree ∂ ϕ = n and with a length linear in n for which any equivalent BSR sentence contains at least n k=1 2 ↑k (n) leading existential quantifiers. Proof sketch. Recall that [n] abbreviates the set {1, . . . , n} and that PS denotes the power set of a given set S. Let n ≥ 1 be some positive integer. Consider the following firstorder sentence in which the sets {x 1 , . . . , x n } and {y 1 , . . . , y n } are separated: ϕ := ∀x n ∃y n . . . ∀x 1 ∃y 1 .

4n i=1 P i (x 1 , . . . , x n ) ↔ Q i (y 1 , . . . , y n ) .
Notice that we change the orientation of the indices in the quantifier prefix in this proof.

In order to construct a particular model of ϕ, we inductively define the following sets:

S 1 := S ⊆ [4n] |S| = 2n , S k+1 := S ∈ PS k |S| = 1 2 • |S k | for every k, 1 < k ≤ n. Hence, we observe |S 1 | = 4n 2n ≥ 4n 2n 2n = 2 2n , |S 2 | = |S1| |S1|/2 ≥ |S1| |S1|/2 |S1|/2 ≥ 2 2 2n-1 , . . . |S n | = |Sn-1| |Sn-1|/2 ≥ 2 2 2 . . . 2 2n-1 -1 -1 ≥ 2 ↑n (n + 1).
We now define the structure A as follows:

• U A := n k=1 a (k) S , b (k) S S ∈ S k , • P A i := a (1) S1 , . . . , a (n) Sn ∈ U n A i ∈ S 1 ∈ S 2 ∈ . . . ∈ S n for i = 1, . . .

, 4n, and

• Q A i := b (1) S1 , . . . , b (n) Sn ∈ U n A i ∈ S 1 ∈ S 2 ∈ . . . ∈ S n for i = 1, . . . , 4n.
One can easily show that A is a model of ϕ. Moreover, employing a game-theoretic argument, one can show the following property:

( * ) the substructure induced by A's domain after removing at least one of the b

(k) S
does not satisfy ϕ. We know that U A contains at least The key idea is that ϕ * , which is satisfied by A, must contain one existential quantifier for each and every b Since every atom Q i (y 1 , . . . , y n ) contains n variables from existential quantifier blocks that are separated by universal ones, the degree ∂ ϕ of ϕ is n. Moreover, ϕ can easily be transformed into a CNF that is Horn and Krom at the same time.

Hence, the theorem holds.

Theorem 16 entails that there is no elementary upper bound on the length of the BSR sentences that result from an equivalence-preserving transformation of SF sentences into BSR. On the other hand, by Lemma 12, there is an elementary upper bound, if we only consider SF sentences up to a certain degree.

Lower bounds on the computational complexity of SF-satisfiability

In this section we establish lower bounds on the worst-case time complexity of SF-satisfiability. Our arguments will be based on a particular form of bounded domino (or tiling) problems developed by Grädel (see [START_REF] Grädel | On solvable cases of Hilbert's 'Entscheidungsproblem[END_REF] and [START_REF] Börger | The Classical Decision Problem[END_REF], Section 6.1.1). By Z t we denote the set of integers {0, . . . , t -1} for any positive t ≥ 1.

Definition 17 ([3], Definition 6.1.1). A domino system D := D, H, V is a triple where D is a finite set of tiles and H, V ⊆ D × D are binary relations determining the allowed horizontal and vertical neighbors of tiles, respectively. Consider the torus Z 2 t := Z t × Z t and let D := D 0 . . . D n-1 be a word over D of length n ≤ t. The letters of D represent tiles. We say that D tiles the torus Z 2 t with initial condition D if and only if there exists a mapping τ : Z 2 t → D such that for every x, y ∈ Z 2 t the following conditions hold, where "+1" denotes increment modulo t.

(a) If τ (x, y) = D and τ (x + 1, y) = D , then D, D ∈ H. (b) If τ (x, y) = D and τ (x, y + 1) = D , then D, D ∈ V. (c) τ (i, 0) = D i for i = 0, . . . , n -1.
Definition 18 ([3], Definition 6.1.5). Let T : N → N be a function and let D := D, H, V be a domino system. The problem DOMINO(D, T (n)) is the set of those words D over the alphabet D for which D tiles Z 2 T (|D|) with initial condition D. Domino problems provide a convenient way of deriving lower bounds via reductions. Suppose we are given some well-behaved time bound T (n) that grows sufficiently fast. Further assume there is a reasonable translation from DOMINO(D, T (n)) into some problem L where the length of the results is upper bounded by a function g(n). It follows that the time required to solve the hardest instances of L lies in Ω T (h(n)) , where h(n) may be conceived as an inverse of g(n) from an asymptotic point of view. The next proposition formalizes this observation.

Proposition 19 ( [3], Theorem 6.1.8). Let T : N → N be a time-constructible function with T (c n) 2 ∈ o(T (n))
for some constant c > 0 and let L be a problem such that for every domino system D we have DOMINO(D, T (n)) ≤ g(n) L, i.e. DOMINO(D, T (n)) is polynomially reducible to L via length order g(n) (cf. Definition 6.1.7 in [START_REF] Börger | The Classical Decision Problem[END_REF]). Moreover, let h : N → N be a function such that h(d • g(n)) ∈ O(n) for any positive d. There exists a positive constant c > 0 such that (i) Fix some positive integer k > 0 and let D be an arbitrary domino system. Let Sat(SF ∂≤k ) be the set containing all satisfiable SF sentences whose degree ∂ is at most k. We have DOMINO D, 2 ↑k (n) ≤ n•log n Sat(SF ∂≤k ). (ii) Fix some positive integer m > 1 and let D be an arbitrary domino system. Let Sat(SF) be the set containing all satisfiable SF sentences.

L ∈ NTIME(T (c • h(n))).
We have DOMINO(D,

2 ↑n (m)) ≤ n 2 •log n Sat(SF).
Having these reduction results at hand, Proposition 19 implies the sought lower bounds on SFsatisfiability for classes of sentences with bounded degree and the class of unbounded SF sentences.

Theorem 21. There are positive constants c, d > 0 for which Sat(SF ∂≤k ) ∈ NTIME 2 ↑k (cn/ log n) and Sat(SF

) ∈ NTIME 2 ↑d• √ n/ log n (2) .
These lower bounds also hold if we do not allow equality in SF, see Section 5.3. The remainder of Section 5 is devoted to the formalization of sufficiently large tori in SF and to the translation from a given domino system D = D, H, V (for nonempty D, H, V) plus an initial condition D into an SF sentence ϕ such that ϕ is satisfiable if and only if D ∈ DOMINO(D, T i (|D|)) with T 1 (n) = 2 ↑κ (n) for any given κ > 0 and T 2 (n) = 2 ↑n (µ) for any given µ > 1.

Enforcing a large domain

The following description gives a somewhat simplified view. Technical details will follow.

A crucial part in the reduction is that a grid of size t × t has to be encoded, where t defines the required computing time and we assume t := 2 ↑κ (µ) for positive integers κ and µ > 1 that we consider as parameters of the construction.

Every point p on the grid is represented by a pair p = x, y , where each of the coordinates x and y is represented by a bit string of length log 2 ↑κ (µ) = 2 ↑κ-1 (µ). Given a bit string b, we represent the j-th bit b j by the truth value of the atom J(κ, b, j), where κ is the constant used to address the topmost level of a hierarchy of κ + 1 sets of indices. The crux of our approach is that we have to enforce the existence of sufficiently many indices j, namely 2 ↑κ-1 (µ) many, to address the single bits of b. Again, we address each of these indices as a bit string, this time of length 2 ↑κ-2 (µ).

Thus, we proceed in an inductive fashion, building up a hierarchy of indices with κ + 1 levels. The lowest level, level zero, is inhabited by µ indices, which we represent as constants with distinct values. For every ≥ 1 any index j on the -th level is represented by a bit string consisting of 2 ↑ -1 (µ) bits, i.e. the -th level of the index hierarchy contains 2 ↑ (µ) indices. The i-th bit of an -th-level index j corresponds to the truth value of the atom J( , j, i).

Example 65536 On every index level, the bits of one index are indexed by the indices from the previous level. We illustrate this for the word 1010 on all levels from 2 down to 0. The bits of 1010 on level two are indexed by bit strings from level one, each of them having a length of two. The bits of the indices of level one are themselves indexed by objects of level zero which are some values c 1 , c 2 assigned to the constants c 1 , c 2 . To improve readability, we connect the bits of words by dashes. level 2: 1----0----1----0

↑ ↑ ↑ ↑ level 1: 0-0 0-1 1-0 1-1 ↑ ↑ ↑ ↑ ↑ ↑ ↑ ↑ level 0: c 1 c 2 c 1 c 2 c 1 c 2 c 1 c 2
For technical reasons the number of indices per level grows slightly slower than described above (cf. Lemma 24). The described index hierarchies can be encoded by SF formulas with the quantifier prefix ∃ * (∀∃) κ that have a length that is polynomial in κ and µ. We use the following constant and predicate symbols with the indicated meaning: 0, 1, . . . , κ constants denoting the levels from 0 to κ, c 1 , . . . , c µ denote the indices at level 0, d 1 , . . . , d κ d is the min. index at level , e 1 , . . . , e κ e is the max. index at level , L( , j)

index j belongs to level , MinIdx( , j) j is a min. index at level , MaxIdx( , j) j is a max. index at level , J( , j, i, b) the i-th bit of the index j at level is b, J * ( , j, i, b) b = 1 indicates that all the bits of the index j that are less significant than j's i-th bit are 1, Succ( , j, j ) j is the successor index of j at level . On every level we establish an ordering over the indices of that level. We use the usual ordering on natural numbers encoded in binary. Moreover, we formalize the usual successor relation on these numbers by the predicate Succ.

One difficulty that we encounter is that we cannot assert the existence of successors simply by adding ∀j∃j . Succ( , j, j ), as j and j would not be separated. Therefore, we fall back on a trick: we start from the equivalent formula ∀j∃ jj . j ≈ j ∧ Succ( , j, j ), and replace the atom j ≈ j by a subformula eq j, j in which j and j are separated and which expresses a certain similarity between j and j instead of identity. However, it turns out that we can specify the hierarchy of indices in a sufficiently strong way such that the similarity expressed by eq j, j actually coincides with identity.

Next, we formalize the described index hierarchies in SF ∂≤κ . Every formula is accompanied by a brief description of its purpose. We shall try to use as few non-Horn sentences as possible.

ψ1 := κ =0 κ = 0 = ∀j. L( , j) → ¬L( , j)
Every index belongs to at most one level. ∧ ∀jj . MinIdx( , j) → ¬Succ( , j , j) A min. index of level belongs to level . A min. index does not have a predecessor.

ψ3 := κ =0 MinIdx( , d ) ∧ ∀j. MinIdx( , j) → j ≈ d
There is a unique min. index on every level.

ψ4 := κ =0 ∀j. MaxIdx( , j) → L( , j)
∧ ∀jj . MaxIdx( , j) → ¬Succ( , j, j ) A max. index of level belongs to level . A max. index does not have a successor.

ψ5 := κ =0 MaxIdx( , e ) ∧ ∀j. MaxIdx( , j) → j ≈ e
There is a unique max. index on every level.

ψ6 := κ =0 ∀jj . Succ( , j, j ) → L( , j) ∧ L( , j )
If j is the successor of j at level , then both j and j belong to level . ψ7 := κ =0 ∀jj j . ¬Succ( , j, j) ∧ Succ( , j, j ) ∧ Succ( , j, j ) → j ≈ j ∧ Succ( , j , j) ∧ Succ( , j , j) → j ≈ j

The successor relation is irreflexive. Every index j has at most one successor and at most one predecessor.

ψ8 := MinIdx(0, c1) ∧ MaxIdx(0, cµ) ∧ µ-1 i=1 Succ(0, ci, ci+1)
At level zero we have the sequence c1, . . . , cµ of successors, where c1 is min. and cµ max.

ψ9 := κ =1 ∀jj i. Succ( , j, j ) ∧ L( -1, i)
→ J * ( , j, i, 1) ∧ J( , j, i, 1) → J( , j , i, 0) ∧ J * ( , j, i, 1) ∧ J( , j, i, 0) → J( , j , i, 1) ∧ J * ( , j, i, 0) ∧ J( , j, i, 1) → J( , j , i, 1)

∧ J * ( , j, i, 0) ∧ J( , j, i, 0) → J( , j , i, 0)
Define what it means to be a successor at level , > 0, in terms of the binary increment operation modulo 2 ↑ (µ).

ψ10 := κ =1 ∀ji. MinIdx( , j) ∧ L( -1, i) → J( , j, i, 0)
All bits of a minimal index j are 0.

ψ11 := κ =1 ∀ji. MaxIdx( , j) ∧ MaxIdx( -1, i) → J( , j, i, 1)
Define what it means to be max. (part 1): the most significant bit is 1.

ψ12 := κ =1 ∀ji. L( , j) ∧ MaxIdx( -1, i) ∧ J( , j, i, 1) → MaxIdx( , j)
Define what it means to be max. (part 2): any index with 1 as its most significant bit is max.

ψ13 := κ =1 ∀ji. L( , j) ∧ L( -1, i) → J( , j, i, 0) → ¬J( , j, i, 1) ∧ J * ( , j, i, 0) → ¬J * ( , j, i, 1)
No bit of an index is 0 and 1 at the same time. An analogous requirement is stipulated for J * . 1) holds for every index j. ψ15 := κ =1 ∀jii . L( , j) ∧ Succ( -1, i, i ) → J * ( , j, i , 1) ↔ J * ( , j, i, 1) ∧ J( , j, i, 1) ∧ J( , j, i, 0) → J * ( , j, i , 0) ∧ J * ( , j, i, 0) → J * ( , j, i , 0) Define the semantics of J * as indicating that all bits strictly less significant than the i-th bit are 1. eq 1 j, j := L(1, j) ∧ L(1, j)

ψ14 := κ =1 ∀ji. L( , j) ∧ MinIdx( -1, i) → J * ( , j, i, 1) J * ( , j, d -1 ,
∧ µ i=1
J(1, j, ci, 0) ↔ J(1, j, ci, 0)

∧ J(1, j, ci, 1) ↔ J(1, j, ci, 1) Base case of equality of indices. eq j, j := L( , j) ∧ L( , j) ∧ ∀i. L( -1, i)

→ ∃ i. L( -1, i) ∧ eq -1 i, i ∧ J( , j, i, 0) ↔ J( , j, i, 0) ∧ J( , j, i, 1) ↔ J( , j, i, 1) Inductive case of equality of indices for > 1. ψ16 := κ =1 ∀ji. L( , j) ∧ MaxIdx( -1, i) ∧ J( , j, i, 0)
→ ∃ j j . eq j, j ∧ Succ( , j, j )

For every index at level that is not maximal, i.e. whose most significant bit is 0, there exists a successor index.

Until now, we have only introduced sentences that can easily be transformed into SF sentences in Horn form in which existential variables are separated from universal ones, as all quantifiers occur with positive polarity and as consequents of implications are (conjunctions of) literals. Regarding the length of the sentences, we observe len(ψ 1 ∧ . . . ∧ψ 16 ) ∈ O κ 2 log κ + κµ(log κ + log µ) .

The following three sentences do not produce Horn formulas when transformed into CNF. They serve the purpose of removing spurious elements from the model. In particular, χ 3 is essential to enforce large models for κ ≥ 2.

χ1 := ∀j. L(0, j) → µ i=1 j ≈ ci
On level 0 there are no indices but c1, . . . , cµ.

χ2 := κ =1 ∀ji. L( , j) ∧ L( -1, i) → J( , j, i, 0) ∨ J( , j, i, 1)
We stipulate totality for the predicate J. χ3 := κ =1 ∀jj . L( , j) ∧ L( , j ) → ∃ j j . eq j, j ∧ eq j , j ∧ ∀ i. L( -1, i) → J( , j, i, 0) ↔ J( , j , i, 0) → j ≈ j Two indices at the same level that agree on all of their bits are required to be identical.

Notice that χ 3 is (almost) an SF sentence, since the ∀ i turns into a ∃ i as soon as we bring the sentence into prenex normal form. We observe len(χ 1 ∧ χ 2 ∧ χ 3 ) ∈ O κ 2 log κ + κµ(log κ + log µ) .

Consider any model

A of ψ 1 ∧ . . . ∧ψ 16 ∧ χ 1 ∧ χ 2 ∧ χ 3 .
Definition 23. We define the following sets and relations: I := a ∈ U A | A, [j →a] |= L( , j) for every = 0, . . . , κ; ≺ ⊆ I × I for every = 0, . . . , κ such that a ≺ a holds if and only if A, [j →a, j →a ] |= Succ( , j, j ).

Lemma 24. For every = 1, . . . , κ we have |I | = p where p := 2 |I -1 |-1 + 1 = 2 ↑ (µ -1) + 1. Moreover, there is a unique chain a 1 ≺ . . . ≺ a p comprising all elements in I .

Leaving out the non-Horn parts χ 1 , χ 2 , χ 3 renders the lemma invalid for > 1. On the other hand, for κ = 1 the sentence ψ 1 ∧ . . . ∧ ψ 16which can be transformed into an equivalent Horn sentence-has only models A for which I 1 contains at least 2 µ-1 + 1 elements. Notice that this could be used to derive EXPTIME-hardness of satisfiability for the class of Horn SF sentences of degree 1. But such lower bounds are already known for the Horn subfragments of MFO and of the BSR fragment, which are proper subsets of SF's Horn subfragment.

Formalizing a tiling of the torus

In order to formalize a given domino problem D = D, H, V and an initial condition D, we introduce the following constant and predicate symbols: H(x, y, x , y )

x , y is the horiz. neighbor of x, y , i.e. x = x + 1 (mod 2 ↑κ (µ -1) + 1) and y = y, V (x, y, x , y )

x , y is the vert. neighbor of x, y , D(x, y)

x, y is tiled with D ∈ D, f 1 , . . . , f |D| constants addressing points 0, 0 , . . . , |D| -1, 0 . With the ideas we have seen when formalizing the index hierarchy, it is now fairly simple to formalize the torus. For instance, the following sentence makes sure that every point that is not on the "edge" of the torus has a horizontal neighbor. The next sentence, on the other hand, makes sure that the rules of the domino system D are obeyed. Lemma 25. Assume that D, H, and V are nonempty and let A be a model of the sentence ψ 1 ∧. . .∧ψ 16 ∧χ 1 ∧χ 2 ∧χ 3 ∧η. A induces a tiling τ of Z 2 t with initial condition D := D 1 , . . . , D n , where t := 2 ↑κ (µ -1) + 1.

Replacing the equality predicate

Since SF can express reflexivity, symmetry, transitivity, and congruence properties, it is easy to formulate an SF sentence without equality that is equisatisfiable to ψ 1 ∧ . . . ∧ ψ 16 ∧ χ 1 ∧ χ 2 ∧ χ 3 ∧ η and uses atoms E(s, t) instead of s ≈ t. In addition to replacing equational atoms as indicated, we add the usual axioms concerning the fresh predicate symbol E. Overall, the additional formulas have a length that lies in O κ log κ + |D| log |D| .

Consequently, the hardness result that we have obtained for SF with equality can be directly transferred to SF without equality.

Conclusion

We stress in this paper that an analysis of the computational complexity of satisfiability problems can greatly benefit from an analysis of how variables occur together in atoms instead of exclusively considering the number of occurring quantifier alternations. What we have not yet taken into account is the Boolean structure of sentences. This may widen the scope of our methods considerably and may moreover help understand where the hardness of satisfiability problems stems from.

Consider a quantified Boolean formula ϕ := ∀ x 1 ∃ y 1 . . . ∀ x n ∃ y n .ψ with quantifier-free ψ. All satisfiable formulas of this shape together form a hard problem residing on the n-th level of the polynomial hierarchy. But what if, for instance, ψ has the form i K i ∧ j L j , where the K i and the L j are literals and none of the existential variables in i K i occurs in j L j ? Since Boolean variables cannot jointly occur in atoms, ϕ can be transformed into the equivalent formula ∃ y 1 . . . y n ∀ x 1 . . . x n .ψ by application of the rules of miniscoping (cf. Lemma 2). Apparently, ϕ belongs to a class of QBF sentences that resides on the first level of the polynomial hierarchy rather than on the n-th.

Perhaps it is time to reconsider some of the definitions that are based on the shape of quantifier prefixes alone.

Figure 1 .

 1 Figure1. The subfragments of SF scale over the major nondeterministic complexity classes in ELEMENTARY, while SF itself goes even beyond.

n k=1 2

 2 ↑k (n) elements of the form b (k) S . Using ( * ) and the substructure lemma, one can argue that any BSR sentence ϕ * that is semantically equivalent to ϕ must contain at least n k=1 2 ↑k (n) leading existential quantifiers.

S

  . Otherwise, there would be one b (k) S , call it b * , such that we could remove b * from A's domain and any tuple . . . , b * , . . . from the sets Q A i , and the resulting structure would then still be a model of ϕ * . But this would contradict ( * ).

Subsections 5 .

 5 1 and 5.2 are devoted to the purpose of outlining the following reductions.Lemma 20.

  MinIdx( , j) → L( , j)

  η3 := ∀xyi. L(κ, x) ∧ L(κ, y) ∧ MaxIdx(κ -1, i) ∧ J(κ, x, i, 0) → ∃ x y x . eq κ x,x ∧ eq κ y, y ∧ D∈D D(x, y) ↔ D( x, y) ∧ H( x, y, x , y)

  η15 := ∀xx y. H(x, y, x , y) → D,D ∈H D(x, y) ∧ D (x , y)Proceeding this way, the formalization η of a domino system in SF requires a length in O n log n , where n := max{κ, µ, |D|, |D| 2 }.

  A, β |= ϕ if ϕ evaluates to true under A and β. We write A |= ϕ if A, β |= ϕ holds for every β. The symbol |=| denotes (semantic) equivalence of formulas, i.e. ϕ |=| ψ holds whenever for every structure A and every variable assignment β we have A, β |= ϕ if and only if A, β |= ψ. We call two sentences ϕ and ψ equisatisfiable if ϕ has a model if and only if ψ has one.

  for a proof.Lemma 1 (Substructure lemma). Let ϕ be a firstorder sentence in prenex normal form without existential quantifiers and let A be a substructure of B. B |= ϕ entails A |= ϕ.

	Lemma 2 (Miniscoping). Let ϕ, ψ, χ be arbitrary
	first-order formulas, and assume that x does not
	occur freely in χ.
	∃x.(ϕ ∨ ψ) |=| (∃x 1 .ϕ) ∨ (∃x 2 .ψ) ,
	∃x.(ϕ • χ) |=| (∃x.ϕ) • χ ,
	∀x.(ϕ ∧ ψ) |=| (∀x 1 .ϕ) ∧ (∀x 2 .ψ) ,
	∀x.(ϕ • χ) |=| (∀x.ϕ) • χ ,
	where • ∈ {∧, ∨}.

  22. Assume µ = 2 and κ = 3.

	index	set of	number
	level	indices	of indices
	0	{c 1 , c 2 }	2
	1	{00, 01, 10, 11}	4
	2	{0000, 0001, . . . , 1111}	16
	3	{0, 1} 16