# A Gentle Introduction to Applications of Algorithmic Metatheorems for Space and Circuit Classes
## 3 An Algorithmic Metatheorem for Logspace and Its Applications
### Applications: High-Hanging Fruits II--A Refined Version of Fagin's Theorem
Similarly to our argument for the even cycle problem, the authors also distinguish two cases, namely graphs of large tree width, where special algorithms are applied, and graphs of small tree width, where [PERSON]'s Theorem is applied. However, the special algorithms are now somewhat more involved, and it takes considerably more work to use the logspace version of [PERSON]'s Theorem to prove the following:  
**Theorem 8** ([20]). : _Let \(\phi=\exists R_{1}\cdots\exists R_{n}\,\forall x\exists y\,\psi\), where \(\psi\) is quantifier-free and contains no relational, function, or constant symbols other than the binary edge relation symbol \(E\). Then, the set \(\{G\mid G\text{ is an undirected, self-loop-free graph with }G\models\phi\}\) can be decided in logarithmic space._  
To better appreciate the power of this theorem, consider the formula  
\[\exists C_{1}\cdots\exists C_{m}\forall x\exists y\Big{(}E(x,y)\wedge\bigvee _{i=1}^{m}\big{(}C_{i}(x)\wedge\bigwedge_{j\
eq i}\
eg C_{j}(x)\wedge C_{(i \bmod m)+1}(y)\big{)}\Big{)}\]  
\"Read aloud\" this formula asks whether \"we can color the vertices of the graph using \(m\) colors such that for each vertex \(x\) an edge leads to a 'next' vertex \(y\) with the 'next' color\". When a graph satisfies this formula, if we start at any vertex and repeatedly move to the \"next\" vertex, we will run into a cycle and along this cycle the colors will also \"cycle\", which means that the length of the cycle must be a multiple of \(m\). Using this observation, it is not hard to show that a connected undirected graph will satisfy this formula if, and only if, it contains a cycle whose length is a multiple of \(m\) for \(m\geq 3\). Since the formula has the prefix required in the theorem, it tells us that all cycle modularity problems for undirected graphs for \(m\geq 3\) and \(x=0\) can be solved in logarithmic space. Thus, we can prove the earlier observations concerning these problems purely by having a look at the syntax of the formula describing them! Proof Ideas. : The proof of the claim for polynomial time is spread over the 35 pages of Sections 4-6 of [19] and consists of two kinds of arguments: Arguments of a graph-theoretic nature and arguments showing how certain graph problems can be solved in polynomial time. Since the graph-theoretic arguments are independent of complexity-theoretic questions, one only needs to show how the algorithms described in [19] can be implemented in logarithmic space rather than polynomial time. Here, as in the argument for the even cycle problem, two basic cases are distinguished: either the input graph has sufficiently small tree width (the exact number depends on the formula \(\phi\)), in which case one can decide whether \(G\models\phi\) holds using the logspace version of Courcelle's Theorem, or the tree width is high. In the latter case, we first preprocess the input graph by removing extra copies of \"similar\" vertices. Two vertices are \"similar\" when their neighborhoods are identical, and, if there is a large number of similar vertices, the formula \(\phi\) cannot distinguish between them any longer and will hold (or not hold) also for the reduced graph. After this preprocessing, we check whether the graph contains some fixed graphs as induced subgraphs (the list of to-be-checked graphs only depends on \(\phi\)) and can accept, if the graph contains one of them. The above theorem handles \"just\" one of the possible quantifier prefixes an eso-formula can have (albeit the most difficult one) and this prefix yields the class L. What about other prefixes? They can only yield classes inside NP by Fagin's Theorem, but do some of them yield, say, P? Or NL? Or NC? These questions are answered in [20], where it is shown that each prefix yields one of the classes NP, NL, L, or FO (first-order logic) and nothing else. In particular, _no_ prefix yields P, unless NP = P or P = NL.