Abstract Let $\mathscr {C}$ be a class of finite and infinite graphs that is closed under induced subgraphs. The well-known Łoś–Tarski Theorem from classical model theory implies that $\mathscr {C}$ is definable in first-order logic by a sentence $\varphi $ if and only if $\mathscr {C}$ has a finite set of forbidden induced finite subgraphs. This result provides a powerful tool to show nontrivial characterizations of graphs of small vertex cover, of bounded tree-depth, of bounded shrub-depth, etc. in terms of forbidden induced finite subgraphs. Furthermore, by the Completeness Theorem, we can compute from $\varphi $ the corresponding forbidden induced subgraphs. This machinery fails on finite graphs as shown by our results: – There is a class $\mathscr {C}$ of finite graphs that is definable in first-order logic and closed under induced subgraphs but has no finite set of forbidden induced subgraphs. – Even if we only consider classes $\mathscr {C}$ of finite graphs that can be characterized by a finite set of forbidden induced subgraphs, such a characterization cannot be computed from a first-order sentence $\varphi $ that defines $\mathscr {C}$ and the size of the characterization cannot be bounded by $f(|\varphi |)$ for any computable function f. Besides their importance in graph theory, the above results also significantly strengthen similar known theorems for arbitrary structures.

It is well known [Lovász, 67] that up to isomorphism a graph~$G$ is determined by the homomorphism counts $\hom(F, G)$, i.e., the number of homomorphisms from $F$ to $G$, where $F$ ranges over all graphs. Thus, in principle, we can answer any query concerning $G$ with only accessing the $\hom(\cdot,G)$'s instead of $G$ itself. In this paper, we deal with queries for which there is a hom algorithm, i.e., there are finitely many graphs $F_1, \ldots, F_k$ such that for any graph $G$ whether it is a Yes-instance of the query is already determined by the vector\[\overrightarrow{\hom}_{F_1,\ldots,F_k}(G):= \big(\hom(F_1,G),\ldots,\hom(F_k,G)\big),\]where the graphs $F_1, \ldots, F_k$ only depend on $φ$. We observe that planarity of graphs and 3-colorability of graphs, properties expressible in monadic second-order logic, have no hom algorithm. On the other hand, queries expressible as a Boolean combination of universal sentences in first-order logic FO have a hom algorithm. Even though it is not easy to find FO definable queries without a hom algorithm, we succeed to show this for the non-existence of an isolated vertex, a property expressible by the FO sentence $\forall x\exists y Exy$, somehow the ``simplest'' graph property not definable by a Boolean combination of universal sentences.These results provide a characterization of the prefix classes of first-order logic with the property that each query definable by a sentence of the prefix class has a hom algorithm. For adaptive query algorithms, i.e., algorithms that again access $\overrightarrow{\hom}_{F_1,\ldots,F_k}(G)$ but here $F_{i+1}$ might depend on $\hom(F_1,G),\ldots,\hom(F_i,G)$, we show that three homomorphism counts $\hom(\cdot,G)$ are both sufficient and in general necessary to determine the isomorphism type of $G$.

LetCbe a class of finite and infinite graphs that is closed under induced subgraphs. The well-known Łoś-Tarski Theorem from classical model theory implies thatCis definable in first-order logic (FO) by a sentence φ if and only ifChas a finite set of forbidden induced finite subgraphs. It provides a powerful tool to show nontrivial characterizations of graphs of small vertex cover, of bounded tree-depth, of bounded shrub-depth, etc. in terms of forbidden induced finite subgraphs. Furthermore, by the Completeness Theorem, we can compute from φ the corresponding forbidden induced subgraphs. Our results (a) and (b) show that this machinery fails on finite graphs. (a)There is a class of finite graphs that is definable in FO and closed under induced subgraphs but has no finite set of forbidden induced subgraphs. (b)Even if we only consider classesCof finite graphs that can be characterized by a finite set of forbidden induced subgraphs such a characterization cannot be computed from an FO-sentence φ that definesCand the size of the characterization cannot be bounded by f(|φ|) for any computable function f.Besides their importance in graph theory, our results also significantly strengthen similar known theorems for arbitrary structures.

Shrub-depth is a graph invariant often considered as an extension of tree-depth to dense graphs. We show that the model-checking problem of monadic second-order logic on a class of graphs of bounded shrub-depth can be decided by AC^0-circuits after a precomputation on the formula. This generalizes a similar result on graphs of bounded tree-depth [Y. Chen and J. Flum, 2018]. At the core of our proof is the definability in first-order logic of tree-models for graphs of bounded shrub-depth.

For a class K of finite graphs we consider the following three statements. (i) K has bounded tree-depth. (ii) First-order logic FO has an effective generalized quantifier elimination on K. (iii) The parameterized model checking for FO on K is in para-AC0. We prove that (i) ⟹ (ii) and (ii) ⟺ (iii). All three statements are equivalent if K is closed under taking subgraphs, but not in general.

For every natural number q let FO_q denote the class of sentences of first-order logic FO of quantifier rank at most q. If a graph property can be defined in FO_q, then it can be decided in time O(n^q). Thus, minimizing q has favorable algorithmic consequences. Many graph properties amount to the existence of a certain set of vertices of size k. Usually this can only be expressed by a sentence of quantifier rank at least k. We use the color coding method to demonstrate that some (hyper)graph problems can be defined in FO_q where q is independent of k. This property of a graph problem is equivalent to the question of whether the corresponding parameterized problem is in the class para-AC^0. It is crucial for our results that the FO-sentences have access to built-in addition and multiplication (and constants for an initial segment of natural numbers whose length depends only on k). It is known that then FO corresponds to the circuit complexity class uniform AC^0. We explore the connection between the quantifier rank of FO-sentences and the depth of AC^0-circuits, and prove that FO_q is strictly contained in FO_{q+1} for structures with built-in addition and multiplication.

We demonstrate some lower bounds for parameterized problems via parameterized classes corresponding to the classical AC^0. Among others, we derive such a lower bound for all fpt-approximations of the parameterized clique problem and for a parameterized halting problem, which recently turned out to link problems of computational complexity, descriptive complexity, and proof theory. To show the first lower bound, we prove a strong AC^0 version of the planted clique conjecture: AC^0-circuits asymptotically almost surely can not distinguish between a random graph and this graph with a randomly planted clique of any size <= n^xi (where 0 <= xi < 1).

It is well-known that least fixed-point logic LFP captures the complexity class PTIME on ordered structures. The ordered conjecture claims that LFP is more expressive than first-order logic FO on every infinite class O of finite ordered structures. We present two methods which yield that LFP is more expressive than FO on various types of classes of ordered structures. The first method, the model-checking method, among others, can be applied for all such classes O of bounded cliquewidth. By the second method, the padding method, we show that for classes O of ``bounded treewidth,'' more precisely, for classes O such that there is a bound for the treewidth of the successor structures associated with the members of O, even DTC is more expressive than FO on O, where DTC denotes the deterministic transitive closure logic, a logic that captures the complexity class L on ordered structures. Furthermore, with the padding method we get that for every infinite class of ordered structures O we have that DTC is more expressive than FO on the class of all ordered sums of pairs of structures in O. Under some complexity theoretic assumption, we prove the existence of a class O of ordered structures such that on O not only LFP is more expressive than FO, but also LFP has the expressive power of existential second-order logic. Furthermore, we characterize those classes of structures whose corresponding class of all ordered versions has bounded treewidth.

Let C denote one of the complexity classes “polynomial time,” “logspace,” or “nondeterministic logspace.” We introduce a logic L (C) inv and show generalizations and variants of the equivalence ( L (C) inv captures C if and only if there is an almost C-optimal algorithm in C for the set Taut of tautologies of propositional logic). These statements are also equivalent to the existence of a listing of subsets in C of Taut by corresponding Turing machines and equivalent to the fact that a certain parameterized halting problem is in the parameterized complexity class XC uni .

There are standard logics DTC, TC, and LFP capturing the complexity classes L, NL, and P on ordered structures, respectively. In we have shown that LFPinv, the "order-invariant least fixed-point logic LFP," captures P (on all finite structures) if and only if there is a listing of the P subsets of the set TAUT of propositional tautologies. We are able to extend the result to listings of the L-subsets (NL-subsets) of TAUT and the logic DTCinv(TCinv). As a byproduct we get that LFPinvcaptures P if DTCinvcaptures L. Furthermore, we show that the existence of a listing of the L-subsets of TAUT is equivalent to the existence of an almost space optimal algorithm for TAUT. To obtain this result we have to derive a space version of a theorem of Levin on optimal inverters.

Abstract We give the first systematic study of strong isomorphism reductions, a notion of reduction more appropriate than polynomial time reduction when, for example, comparing the computational complexity of the isomorphim problem for different classes of structures. We show that the partial ordering of its degrees is quite rich. We analyze its relationship to a further type of reduction between classes of structures based on purely comparing for everynthe number of nonisomorphic structures of cardinality at mostnin both classes. Furthermore, in a more general setting we address the question of the existence of a maximal element in the partial ordering of the degrees.

Abstract The undecidability of first-order logic implies that there is no computable bound on the length of shortest proofs of valid sentences of first-order logic. Some valid sentences can only have quite long proofs. How hard is it to prove such “hard” valid sentences? The polynomial time tractability of this problem would imply the fixed-parameter tractability of the parameterized problem that, given a natural number n in unary as input and a first-order sentence φ as parameter, asks whether φ has a proof of length ≤ n. As the underlying classical problem has been considered by Gödel we denote this problem by p-Gödel. We show that p-Gödel is not fixed-parameter tractable if DTIME(hO(1)) ≠ NTIME(hO(1)) for all time constructible and increasing functions h. Moreover we analyze the complexity of the construction problem associated with p-Gödel.

Recently it has been shown that the miniaturization mapping ℳ faithfully translates bexponential parameterized complexity into (unbounded) parameterized complexity. We determine the pre-images under ℳ of various (classes of) problems. For many parameterized problems whose underlying classical problem is in NP we show that the pre-images coincide with natural reparameterizations that take into account the amount of non-determinism needed to solve them.

We study the parameterized complexity of various path (and cycle) problems, the parameter being the length of the path. For example, we show that the problem of the existence of a maximal path of length k in a graph G is fixed-parameter tractable, while its counting version is #W[1]- complete. The corresponding problems for chordless (or induced) paths are W[2]-complete and #W[2]-complete respectively. With the tools developed in this paper we derive the NP-completeness of a related classical problem, thereby solving a problem due to Hedetniemi.

Abstract We observe that the W*-hierarchy, a variant (introduced by Downey, Fellows, and Taylor [7]) of the better known W-hierarchy, coincides with the W-hierarchy, though not level wise, but just as a whole hierarchy. More precisely, we prove that W[t] ⊆ W* [t] ⊆ W[2t − 2] for each t ≥ 2. It was known before that W[1] = W*[1] and W[2] = W*[2]. Our second main result is a new logical characterization of the W*-hierarchy in terms of “Fagin-definable problems.” As a by-product, we also obtain an improvement of our earlier characterization of the hierarchy in terms of model-checking problems. Furthermore, we obtain new complete problems for the classes W[3] and W*[3].

Most parameterized complexity classes are defined in terms of a parameterized version of the Boolean satisfiability problem (the so-called weighted satisfiability problem). For example, Downey and Fellow's W-hierarchy is of this form. But there are also classes, for example, the A-hierarchy, that are more naturally characterised in terms of model-checking problems for certain fragments of first-order logic. Downey, Fellows, and Regan were the first to establish a connection between the two formalisms by giving a characterisation of the W-hierarchy in terms of first-order model-checking problems. We improve their result and then prove a similar correspondence between weighted satisfiability and model-checking problems for the A-hierarchy and the W^*-hierarchy. Thus we obtain very uniform characterisations of many of the most important parameterized complexity classes in both formalisms. Our results can be used to give new, simple proofs of some of the core results of structural parameterized complexity theory.

Most parameterized complexity classes are defined in terms of a parameterized version of the Boolean satisfiability problem (the so-called weighted satisfiability problem. For example, Downey and Fellow's W-hierarchy is of this form. But there are also classes, for example, the A-hierarchy, that are more naturally characterised in terms of model-checking problems for fragments of first-order logic. R. G. Downey et al. (1998) were the first to establish a connection between the two formalisms by giving a characterisation of the W-hierarchy in terms of first-order model-checking problems. We improve their result and then prove a similar correspondence between weighted satisfiability and model-checking problems for the A-hierarchy and the W-hierarchy. Thus we obtain very uniform characterisations of many of the most important parameterized complexity classes in both formalisms. Our results can be used to give new, simple proofs of some of the core results of structural parameterized complexity theory.

We develop a parameterized complexity theory for counting problems. As the basis of this theory, we introduce a hierarchy of parameterized counting complexity classes #W$[t]$, for $t\ge 1$, that corresponds to Downey and Fellows's W-hierarchy [R. G. Downey and M. R. Fellows, Parameterized Complexity, Springer-Verlag, New York, 1999] and we show that a few central W-completeness results for decision problems translate to #W-completeness results for the corresponding counting problems. Counting complexity gets interesting with problems whose decision version is tractable, but whose counting version is hard. Our main result states that counting cycles and paths of length k in both directed and undirected graphs, parameterized by k, is #W$[1]-complete. This makes it highly unlikely that these problems are fixed-parameter tractable, even though their decision versions are fixed-parameter tractable. More explicitly, our result shows that most likely there is no $f(k) \cdot n^c$-algorithm for counting cycles or paths of length k in a graph of size n for any computable function $f: \mathbb{N} \to \mathbb{N}$ and constant c, even though there is a $2^{O(k)} \cdot n^{2.376}$ algorithm for finding a cycle or path of length k [N. Alon, R. Yuster, and U. Zwick, J. ACM, 42 (1995), pp. 844--856].

We give machine characterisations and logical descriptions of a number of parameterized complexity classes. The focus of our attention is the class W[P], which we characterise as the class of all parameterized problems decidable by a nondeterministic fixed-parameter tractable algorithm, whose use of nondeterminism is bounded in terms of the parameter. We give similar characterisations for AW[P], the "alternating version of W[P]", and various other parameterized complexity classes. We also give logical characterisations of the classes W[P] and AW[P] in terms of fragments of least fixed-point logic, thereby putting these two classes into a uniform framework that we have developed in earlier work. Furthermore, we investigate the relation between alternation and space in parameterized complexity theory. We prove that the compact Turing machine computation problem, shown to be hard for the class AW[SAT] in (K. A. Abrahamson et al., 1995) is complete for the class uniform-XNL.

We develop a parameterized complexity theory for counting problems. As the basis of this theory, we introduce a hierarchy of parameterized counting complexity classes #W[t], for t/spl ges/1, that corresponds to Downey and Fellows' (1999) W-hierarchy and show that a few central W-completeness results for decision problems translate to #W-completeness results for the corresponding counting problems. Counting complexity gets interesting with problems whose decision version is tractable, but whose counting version is hard. Our main result states that counting cycles and paths of length k in both directed and undirected graphs, parameterized by k, are #W[1]-complete. This makes it highly unlikely that any of these problems is fixed-parameter tractable, even though their decision versions are. More explicitly, our result shows that most likely there is no f(k)/spl middot/n/sup c/-algorithm for counting cycles or paths of length k in a graph of size n for any computable function f:/spl Nopf//spl rarr//spl Nopf/ and constant c, even though there is a 2/sup O(k)//spl middot/n/sup 2.376/ algorithm for finding a cycle or path of length k (2).

A number of efficient methods for evaluating first-order and monadic-second order queries on finite relational structures are based on tree-decompositions of structures or queries. We systematically study these methods.In the first part of the article, we consider arbitrary formulas on tree-like structures. We generalize a theorem of Courcelle [1990] by showing that on structures of bounded tree-width a monadic second-order formula (with free first- and second-order variables) can be evaluated in time linear in the structure size plus the size of the output.In the second part, we study tree-like formulas on arbitrary structures. We generalize the notions of acyclicity and bounded tree-width from conjunctive queries to arbitrary first-order formulas in a straightforward way and analyze the complexity of evaluating formulas of these fragments. Moreover, we show that the acyclic and bounded tree-width fragments have the same expressive power as the well-known guarded fragment and the finite-variable fragments of first-order logic, respectively.

In this article, we study parameterized complexity theory from the perspective of logic, or more specifically, descriptive complexity theory. We propose to consider parameterized model-checking problems for various fragments of first-order logic as generic parameterized problems and show how this approach can be useful in studying both fixed-parameter tractability and intractability. For example, we establish the equivalence between the model-checking for existential first-order logic, the homomorphism problem for relational structures, and the substructure isomorphism problem. Our main tractability result shows that model-checking for first-order formulas is fixed-parameter tractable when restricted to a class of input structures with an excluded minor. On the intractability side, for every $t\ge 0$ we prove an equivalence between model-checking for first-order formulas with t quantifier alternations and the parameterized halting problem for alternating Turing machines with t alternations. We discuss the close connection between this alternation hierarchy and Downey and Fellows' W-hierarchy. On a more abstract level, we consider two forms of definability, called Fagin definability and slicewise definability, that are appropriate for describing parameterized problems. We give a characterization of the class FPT of all fixed-parameter tractable problems in terms of slicewise definability in finite variable least fixed-point logic, which is reminiscent of the Immerman--Vardi theorem characterizing the class PTIME in terms of definability in least fixed-point logic.

One of the fundamental results of descriptive complexity theory, due to Immerman [13] and Vardi [18], says that a class of ordered finite structures is definable in fixed-point logic if, and only if, it is computable in polynomial time. Much effort has been spent on the problem of capturing polynomial time, that is, describing all polynomial time computable classes of not necessarily ordered finite structures by a logic in a similar way. The most obvious shortcoming of fixed-point logic itself on unordered structures is that it cannot count. Immerman [14] responded to this by adding counting constructs to fixed-point logic. Although it has been proved by Cai, Fürer, and Immerman [1] that the resulting fixed-point logic with counting, denoted by IFP+C, still does not capture all of polynomial time, it does capture polynomial time on several important classes of structures (on trees, planar graphs, structures of bounded tree-width [15, 9, 10]). The main motivation for such capturing results is that they may give a better understanding of polynomial time. But of course this requires that the logical side is well understood. We hope that our analysis of IFP+C-formulas will help to clarify the expressive power of IFP+C; in particular, we derive a normal form. Moreover, we obtain a problem complete for IFP+C under first-order reductions.

Abstract When analyzing database query languages a roperty, of theories, the pseudo-finite homogeneity property, has been introduced and applied (cf. [3]). We show that a stable theory has the pseudo-finite homogeneity property just in case its expressive power for finite states is bounded. Moreover, we introduce the corresponding pseudo-finite saturation property and show that a theory fails to have the finite cover property if and only if it has the pseudo-finite saturation property.

Abstract Let L be one of the topological languages Lt, (L∞ω)t and (Lκω)t. We characterize the topological spaces which are models of the L-theory of the class of ordinals equipped with the order topology. The results show that the role played in classical model theory by the property of being well-ordered is taken over in the topological context by the property of being locally compact and scattered.

Much effort has been spent to prove that the reduced product operation preserves, and sometimes even strengthens the L-equivalence of structures, where L is some infinitary language. A similar result is suggested by the following well-known fact: Assume D is a nonprincipal ultrafilter on ω and, for n Є ω, Cn is a set. If the ultra-product ΠωCn/D is infinite, it has a cardinality ≥ Hence, by Łos' theorem, (i) if and φ(x) is a first-order formula, then iff where Q is the unary quantifier “there are many.” We shall prove some generalizations of (i). In particular, we show (ii) if D is a nonprincipal ultrafilter over I = ω, and then where L(Q) is the language obtained from the first-order language by adding the quantifier Q. (ii) remains true, if D is an ω-regular or an atomless filter over a set I. Lipner [7] proved that if is regular, then the L(Q)-equivalence is preserved under direct products. We show that the assumption “ is regular” is necessary.

In his paper [1] Chang provides among other things answers to questions of the following type: Given two models and of powers α and β, respectively, what is the least λ such that implies His proofs are by induction on the quantifier rank of formulas and they use an idea which in the case of ordinary first-order language goes back to Ehrenfeucht and Fraïssé. But, as we show, one can easily prove that if λ is big compared with κ and with the cardinality of the universe of the structure , then every L∞κ-formula is equivalent modulo the set of all Lλκ-sentences which hold in to a Lλκ-formula. From this, Chang's results follow immediately. The same method can be applied to similar problems concerning generalized languages.