1: \documentclass{article}
2:
3: \usepackage[latin1]{inputenc}
4: \usepackage{times}
5: \usepackage{latexsym}
6: \usepackage{amsmath}
7: \usepackage{amssymb}
8: \usepackage{graphicx}
9: \usepackage{a4wide}
10: \usepackage{ifthen}
11:
12: \newcommand{\nc}{\newcommand}
13: \nc{\rnc}{\renewcommand}
14: \nc{\nev}{\newenvironment}
15:
16: \rnc{\subsection}{\secdef\ssa\ssb}
17: \nc{\ssa}[2][default]{\par\vspace{2ex}\refstepcounter{subsection}\noindent\textbf{\thesubsection. #1. }}
18: \nc{\ssb}[1]{\par\bigskip\noindent\textbf{#1. }}
19:
20: \makeatletter
21: \rnc{\@seccntformat}[1]{{\normalfont\bfseries{\csname the#1\endcsname}\hspace{1pt}.\hspace{0.4em}}}
22: \rnc{\section}{\@startsection
23: {section}%
24: {1}%
25: {0mm}%
26: {-1.5\baselineskip}%
27: {\baselineskip}%
28: {\normalfont\normalsize\bfseries\centering}%
29: }
30: \renewcommand{\@makecaption}[2]{\begin{center}#1. #2\end{center}}
31: \makeatother
32:
33: \newcounter{theo}[section]
34: \rnc{\thetheo}{\thesection.\arabic{theo}}
35:
36: \nev{defform}[2]{\refstepcounter{theo}\begin{list}{}{%
37: \setlength{\labelwidth}{0em}%
38: \setlength{\leftmargin}{0em}%
39: \setlength{\itemindent}{\labelsep}%
40: \setlength{\listparindent}{1.5em}
41: \setlength{\parsep}{0em}}%
42: \item[\textbf{#2 \thetheo\ifthenelse{\equal{#1}{}}{}{ (#1)}.}]}%
43: {\end{list}}
44:
45: \nev{satzform}[2]{\begin{defform}{#1}{#2}\itshape}{\end{defform}}
46:
47: \nev{theorem}[1][]{\begin{satzform}{#1}{Theorem}}{\end{satzform}}
48: \nev{lemma}[1][]{\begin{satzform}{#1}{Lemma}}{\end{satzform}}
49: \nev{corollary}[1][]{\begin{satzform}{#1}{Corollary}}{\end{satzform}}
50: \nev{proposition}[1][]{\begin{satzform}{#1}{Proposition}{}}{\end{satzform}}
51: \nev{fact}[1][]{\begin{satzform}{#1}{Fact}}{\end{satzform}}
52: \nev{example}[1][]{\begin{defform}{#1}{Example}}{\end{defform}}
53: \nev{definition}[1][]{\begin{defform}{#1}{Definition}}{\end{defform}}
54: \nev{remark}[1][]{\begin{defform}{#1}{Remark}}{\end{defform}}
55:
56: \nc{\proof}{\medskip\noindent\textit{Proof: }}
57: \nc{\proofend}{\hfill$\Box$\vspace{\topsep}\par}
58:
59: \nc{\FOR}{\textbf{for}}
60: \nc{\FORALL}{\textbf{for all}}
61: \nc{\TO}{\textbf{to}}
62: \nc{\DO}{\textbf{do}}
63: \nc{\OD}{\textbf{od}}
64: \nc{\IF}{\textbf{if}}
65: \nc{\FI}{\textbf{fi}}
66: \nc{\THEN}{\textbf{then}}
67: \nc{\ELSE}{\textbf{else}}
68: \nc{\WHILE}{\textbf{while}}
69: \nc{\REPEAT}{\textbf{repeat}}
70: \nc{\UNTIL}{\textbf{until}}
71: \nc{\OR}{\textbf{or}}
72: \nc{\AND}{\textbf{and}}
73: \nc{\ACCEPT}{\textnormal{ACCEPT}}
74: \nc{\REJECT}{\textnormal{REJECT}}
75:
76: \nc{\im}[1]{\item\hspace{#1cm}}
77: \nev{algorithm}{\begin{enumerate}\rnc{\labelenumi}{\textit{\small \arabic{enumi}.}}\rnc{\itemsep}{0ex}}{\end{enumerate}}
78: \renewcommand{\fboxsep}{2mm}
79:
80: \nc{\prob}[3][9]{\begin{center}\normalfont\fbox{\begin{tabular}[t]{rp{#1cm}}\textit{Input:}.\\\textit{Problem:}.\end{tabular}}\end{center}}
81:
82: \rnc{\labelenumi}{(\arabic{enumi})}
83: \rnc{\labelitemi}{\text{--}}
84: \rnc{\phi}{\varphi}
85: \nc{\bigmid}{\;\big|\;}
86: \nc{\Bigmid}{\;\Big|\;}
87:
88: \nc{\FO}{\textup{FO}}
89: \nc{\tp}{\textup{tp}}
90: \nc{\tw}{\textup{tw}}
91: \nc{\ltw}{\textup{ltw}}
92: \nc{\diam}{\textup{diam}}
93: \rnc{\max}{\textup{max}}
94: \rnc{\min}{\textup{min}}
95: \nc{\true}{\textup{true}}
96: \nc{\false}{\textup{false}}
97: \nc{\val}{\textup{val}}
98: \nc{\CC}{\textup{C}}
99:
100: \pagestyle{plain}
101:
102: \begin{document}
103:
104: \title{\large\bf Deciding first-order properties of locally tree-decomposable structures}
105: \author{\normalsize Markus Frick\hspace{2cm}\normalsize Martin Grohe\\
106: \small Institut f\"ur Mathematische Logik, Eckerstr.~1, 79104
107: Freiburg, Germany\\
108: \small Email: \{frick,grohe\}@logik.mathematik.uni-freiburg.de}
109: \date{\normalsize\today}
110: \maketitle
111:
112: {\rnc{\thefootnote}{}\footnotetext{A preliminary version appeared in
113: \emph{Proceedings of the 26th International Colloquium on
114: Automata, Languages, and Programming}, Lecture Notes in Computer
115: Science 1644, pp.331-340. \copyright\ Springer-Verlag 1999}}
116:
117: \begin{abstract}
118: We introduce the concept of a class of graphs, or more generally,
119: relational structures, being \emph{locally
120: tree-decom\-posable}. There are numerous examples of locally
121: tree-decomposable classes, among them the class of planar graphs and
122: all classes of bounded valence or of bounded tree-width. We also
123: consider a slightly more general concept of a class of structures
124: having \emph{bounded local tree-width}.
125:
126: We show that for each property $\phi$ of structures that is
127: definable in first-order logic and for each locally
128: tree-decomposable class $\CC$ of graphs, there is a
129: linear time algorithm deciding whether a given structure $\mathcal
130: A\in \CC$ has property $\phi$. For classes $\CC$ of
131: bounded local tree-width, we show that for every $k\ge 1$ there is an
132: algorithm that solves the same problem in time $O(n^{1+(1/k)})$ (where
133: $n$ is the cardinality of the input structure).
134: \end{abstract}
135:
136: \section{Introduction}
137: It is an important task in the theory of algorithms to find feasible
138: instances of otherwise intractable algorithmic problems. A notion that
139: has turned out to be extremely useful in this context is that of
140: \emph{tree-width} of a graph. \textsc{3-Colorabil\-ity},
141: \textsc{Hamiltonicity}, and many other NP-complete properties of
142: graphs can be decided in linear time when restricted to graphs whose
143: tree-width is bounded by a fixed constant (see \cite{bod97} for a
144: survey).
145:
146: Courcelle \cite{cou90} proved a meta-theorem, which easily implies
147: numerous results of the abovementioned type: \emph{Let $w\ge 1$ and
148: $\phi$ be a property of graphs that is definable in monadic
149: second-order logic. Then $\phi$ can be decided in linear time on
150: graphs of tree-width at most $w$.} As a matter of fact, this result
151: does not only hold for graphs, but for arbitrary relational
152: structures. Although Courcelle's theorem does
153: not give practical algorithms, because the hidden constants are too
154: big, it is still useful since it gives a simple way to recognize a
155: property as being linear time decidable on graphs of bounded
156: tree-width. Once this has been done, a more refined analysis using the
157: combinatorics of the particular property may yield a practical
158: algorithm.
159:
160: Though maybe the most successful, bounded tree-width is not the
161: only restriction on graphs that makes algorithmic tasks easier. Other
162: useful restrictions are \emph{planarity} or \emph{bounded
163: valence}.
164: For example, consider the problem \textsc{$k$-Dominating Set} for a
165: fixed $k$. (Given a graph $\mathcal G$, is there a set $D$ of at most $k$
166: vertices of $\mathcal G$ such that every vertex of $\mathcal G$ is either equal or
167: adjacent to a vertex in $D$?) To solve \textsc{$k$-Dominating Set} in general,
168: we do not know much better than just trying all $O(n^k)$ candidate
169: sets ($n$ always denotes the number of vertices of the input
170: graph). However, on planar graphs \textsc{$k$-Dominating Set} can be
171: solved in time $O(11^kn)$, and on graphs of valence at most $l$, it
172: can be solved in time $O((l+1)^kn)$ \cite{dowfel99}.
173:
174: Unfortunately, the analogue of Courcelle's theorem does not hold for
175: planar graphs or classes of bounded valence; \textsc{3-Colorability}
176: is a monadic second-order definable property that remains NP-complete
177: when restricted to the class of planar graphs of valence at most 4
178: \cite{garjohsto76}. Instead of monadic second-order, we study the
179: complexity of first-order definable properties.
180:
181: Seese was the first to give a meta-theorem in the style of Courcelle's
182: theorem for a more general class of structures; in \cite{see96} he
183: proved that for every $l\ge 1$ and for every first-order definable
184: property of structures there is a linear time algorithm that decides
185: whether a given structure of valence at most $l$ has this property.
186:
187: An observation that has been used for various algorithms on planar
188: graphs (essentially it goes back to Baker \cite{bak94}) is that there
189: is a bound on the tree-width of a planar graph only depending on its
190: diameter. A different way to see this is that a local neighborhood of
191: a vertex in a planar graph has tree-width bounded by a number only
192: depending on the radius of this neighborhood. As a matter of fact,
193: given a planar graph $\mathcal G$ we can compute in linear time a family of
194: subgraphs of bounded tree-width such that a suitably big neighborhood
195: of every vertex of $\mathcal G$ is completely contained in one of these
196: subgraphs.
197:
198: We call classes of graphs admitting such a covering algorithm
199: \emph{locally tree-decomposable} (a precise definition is given in
200: Section \ref{sec:tc}). Examples of locally tree-decomposable classes
201: of graphs are all classes of bounded genus, bounded valence, and
202: bounded tree-width. The concept easily generalizes to arbitrary
203: relational structures.
204:
205: Eppstein \cite{epp99} considered a closely related, though slightly
206: weaker concept he called the \emph{diameter-treewidth property} (we
207: call this property \emph{bounded local tree-width} and refer the
208: reader to Section \ref{sec:ltw} for the definition). Eppstein proved
209: that the subgraph isomorphism problem for a fixed subgraph $\mathcal
210: H$, asking whether a given graph $\mathcal G$ contains $\mathcal H$,
211: is solvable in linear time when restricted to graphs $\mathcal G$
212: contained in a class of graphs that is closed under taking minors and
213: has bounded local tree-width. It is not hard to see that every class
214: $\CC$ of graphs that is closed under taking minors and has bounded local
215: tree-width is locally tree-decomposable (cf.\ Lemma \ref{lem:mintc}).
216:
217: Thus our main result goes much further:
218:
219: \begin{theorem}\label{theo:mt1}
220: Let $\CC$ be a class of relational structures that is locally
221: tree-decomposable and $\phi$ a property definable in
222: first-order logic. Then there is a linear time algorithm deciding
223: whether a given structure $\mathcal A\in \CC$ has property $\phi$.
224: \end{theorem}
225:
226: It may be worth mentioning that in the terminology of \cite{var82},
227: our result can be rephrased as follows: When restricted to a locally
228: tree-decomposable class of structures, the \emph{data complexity} of
229: first-order logic is in linear time.
230:
231: Examples of first-order definable properties are
232: \textsc{$k$-Dominating-Set} and \textsc{$k$-Indepen\-dent-Set} for a
233: fixed $k$, \textsc{$\mathcal H$-Subgraph-Isomorphism} (Given $\mathcal
234: G$, is $\mathcal H\subseteq \mathcal G$?) and \textsc{$\mathcal
235: H$-Homo\-morphism} (Given $\mathcal G$, is there a homomorphism
236: $h:\mathcal H\rightarrow \mathcal G$?) for a fixed $H$,
237: \textsc{$(\mathcal H,\mathcal K)$-Extension} (Given $\mathcal G$, is
238: every $\mathcal H\subseteq \mathcal G$ contained in some $\mathcal
239: K\subseteq \mathcal G$?) for fixed $\mathcal H\subseteq \mathcal K$.
240: Let us also give a few examples of a problems defined on other
241: relational structures than graphs. For $k\ge 1$,
242: \textsc{$k$-Set-Cover} is the problem of deciding whether a given
243: family $\mathcal F$ of sets has a subfamily $\mathcal S$ of size at
244: most $k$ such that $\bigcup\mathcal S=\bigcup\mathcal F$. For $d\ge
245: 1$, \textsc{$(k,d)$-Circuit-Satisfiability} is the problem of deciding
246: whether a given Boolean circuit of depth at most $d$ has a satisfying
247: assignment in which at most $k$ input gates are set to `\true'. Both
248: \textsc{$k$-Set-Cover} and \textsc{$(k,d)$-Circuit-Satisfiability} can
249: be seen as first-order definable problems on certain relational
250: structures. Thus our theorem implies, for example, that
251: \textsc{$k$-Set-Cover} can be solved in linear time for set systems
252: where each element is only contained in a bounded number of sets, and
253: that \textsc{$(k,d)$-Circuit-Satisfiability} can be solved in linear
254: time for circuits whose underlying graph is planar. Of course
255: problems like \textsc{Subgraph-Isomorphism}, \textsc{Homo\-morphism},
256: \textsc{Extension} can be generalized arbitrary relational structures.
257:
258: As a last example, let us consider the problem of evaluating a
259: (Boolean) database query formulated in the relational calculus against
260: a relational database. Since relational calculus is the same as
261: first-order logic, and relational databases are just finite relational
262: structures, our theorem applies and shows, for example, that
263: Boolean relational calculus queries can be evaluated in linear time on
264: databases whose underlying graph is planar. As a matter of fact, this last
265: example was one of our main motivation for starting this research. It
266: seems that when storing geographical data such as road maps, planar
267: structures come up quite naturally.
268:
269: Thus our theorem gives a unifying framework for various results
270: solving concrete problems on specific locally tree-decom\-posable
271: classes such as the class of planar graphs. In addition, it yields a
272: number of new results of this type.
273:
274: Using the same techniques, we prove another theorem that applies to the
275: even more general context of classes of structures of bounded local
276: tree-width:
277:
278: \begin{theorem}\label{theo:mt2}
279: Let $\CC$ be a class of relational structures of bounded local
280: tree-width and $\phi$ a first-order definable property. Then for
281: every $k\ge 1$ there is an algorithm deciding whether a given
282: structure $\mathcal A\in \CC$ has property $\phi$ in time $O(n^{1+(1/k)})$.
283: \end{theorem}
284:
285: The complexity of first-order properties of relational structures has
286: been studied under various aspects. It is long known that every
287: first-order property of graphs can be decided in polynomial time,
288: actually in $\textrm{AC}_0$ \cite{ahoull79,imm82}. A question closer
289: to our theorem is whether deciding first-order properties is
290: \emph{fixed-parameter tractable}, that is, whether there is a fixed
291: $c$ such that every first-order property of finite relational
292: structures can be decided in time $O(n^c)$. This question has been
293: brought up by Yannakakis \cite{yan95}. The theory of fixed-parameter
294: tractability gives some evidence that the answer is no, as has been
295: independently proved by Downey, Fellows, Taylor \cite{dowfeltay96} and
296: Papadimitriou, Yannakakis \cite{papyan97} (deciding first-order
297: properties is $\textrm{AW}[1]$-complete). Theorem \ref{theo:mt2} shows
298: that deciding first-order properties of structures in a class of
299: bounded local tree-width is fixed-parameter tractable. Furthermore, it
300: has been used in \cite{flugro99} to show that for every class $\CC$ of
301: graphs such that there is some graph that is not a minor of any graph
302: in $\CC$, deciding first-order properties of graphs in $\CC$ is
303: fixed-parameter tractable.
304:
305: The proofs of our results combine three main ingredients: a
306: refinement of Courcelle's Theorem \cite{cou90} mentioned above,
307: Gaifman's Theorem \cite{gai81} stating that first-order properties are
308: local, and algorithmic techniques based on ideas of Baker \cite{bak94}
309: and Eppstein \cite{epp99}. To prove Theorem \ref{theo:mt2}, we also
310: use covering techniques due to Awerbuch and Peleg \cite{awepel90,pel93}.
311:
312:
313: \section{Preliminaries}
314:
315: A \emph{vocabulary} is a finite set of relation symbols. Associated
316: with every relation symbol $R$ is a positive integer called the
317: \emph{arity} of $R$. In the following, $E$ always denotes a binary relation
318: symbol and $\tau$ a vocabulary.
319:
320: A {\em $\tau$-structure} $\mathcal A$ consists of a non-empty set $A$, called
321: the {\em universe} of $\mathcal A$, and a relation $R^{\mathcal
322: A}\subseteq A^r$ for each $r$-ary relation symbol $R\in\tau$.
323: If $\mathcal A$ is a $\tau$-structure and $B\subseteq A$, then
324: $\langle B\rangle^{\mathcal A}$ denotes the substructure induced by
325: $\mathcal A$ on $B$, that is, the $\tau$-structure $\mathcal B$ with
326: universe $B$ and $R^{\mathcal B}:=R^{\mathcal A}\cap B^r$ for every
327: $r$-ary $R\in\tau$.
328:
329: For instance, we consider \emph{graphs} as $\{E\}$-structures $\mathcal
330: G=(G,E^{\mathcal G})$, where the binary relation $E^{\mathcal G}$ is
331: symmetric and anti-reflexive (i.e.\ graphs are undirected and
332: loop-free). As another example, we can view hypergraphs as
333: $\{E,P\}$-structures, where $E$ is binary and $P$ unary. A hypergraph
334: with vertices $V$ and hyperedges $\mathcal H\subseteq\text{Pow}(V)$ is
335: modeled by the $\{E,P\}$-structure $\big(V\cup\mathcal H,\{(v,H)\mid v\in H\},V\big)$.
336:
337: \emph{In this paper we only consider finite structures.} Let us remark
338: that all the results of this paper remain true if we also admit
339: constants in our structures. We restrict our attention to the
340: relational case because constants would not give us additional
341: insights.
342:
343: \medskip
344: The formulas of \emph{first-order logic} \FO\ are build up in the usual way
345: from an infinite supply of variables denoted by $x,y,x_1,\ldots$, the
346: equality symbol $=$ and relation symbols of a vocabulary $\tau$, the connectives
347: $\wedge,\vee,\neg,\rightarrow$, and the quantifiers $\forall,\exists$
348: ranging over the universe of the structure. For example, the
349: first-order sentence
350: \[
351: \phi:=\forall x_1\forall x_2\forall x_3\big((Ex_1x_2\wedge Ex_1x_3\wedge
352: Ex_2x_3)\rightarrow\exists y(Ex_1y\wedge Ex_2y\wedge Ex_3y)\big)
353: \]
354: says that every triangle of a graph is contained in a $K_4$ (a
355: complete graph on four vertices). The formula
356: \[
357: Px\wedge\neg\exists y\exists z(\neg y= z\wedge Exy\wedge Exz)
358: \]
359: defines the set of all vertices $x$ of a hypergraph that are contained in
360: at most one hyperedge.
361:
362: A \emph{free variable} in a
363: first-order formula is a variable $x$ not in the scope of a quantifier
364: $\exists x$ or $\forall x$. A \emph{sentence} is a formula without free
365: variables. The notation $\phi(x_1,\ldots,x_k)$ indicates that all
366: free variables of the formula $\phi$ are among $x_1,\ldots,x_k$; it
367: does not necessarily mean that the variables $x_1,\ldots,x_k$ all
368: appear in $\phi$. For a
369: formula $\phi(x_1,\ldots,x_k)$, a structure $\mathcal A$, and
370: $a_1,\ldots,a_k\in A$ we write $\mathcal A\models
371: \phi(a_1,\ldots,a_k)$ to say that $\mathcal A$
372: satisfies $\phi$ if the variables $x_1,\ldots,x_k$ are interpreted by
373: the vertices $a_1,\ldots,a_k$, respectively.
374:
375: \begin{example}
376: In this example we show how to model the \textsc{$k$-Set-Cover}
377: problem mentioned in the introduction by a first-order definable
378: problem. We can view a family $\mathcal F$ of a sets as the hypergraph
379: whith vertex set $\bigcup\mathcal F$ and edge set $\mathcal F$.
380:
381: Let
382: \[
383: \phi_k:=\exists x_1\ldots x_k\forall
384: y\Big(Py\to\big(Eyx_1\vee\ldots\vee Eyx_k\big)\Big).
385: \]
386: Then the hypergraph corresponding to the family $\mathcal F$ satisfies
387: $\phi_k$ if and only if there exists an $\mathcal S\subseteq\mathcal
388: F$ of cardinality $|\mathcal S|=k$ such that $\bigcup\mathcal
389: S=\bigcup\mathcal F$.
390: \end{example}
391:
392: \medskip
393: We often denote tuples $(a_1,\ldots,a_k)$ of elements
394: of a set $A$ by $\bar a$, and we write $\bar a\in A$ instead of $\bar
395: a\in A^k$. Similarly, we denote tuples of variables by
396: $\bar x$.
397:
398: \medskip
399: Our underlying model of computation is the standard RAM-model with
400: addition and subtraction as arithmetic operations (cf.\
401: \cite{ahohopull74, emd90}). In our complexity analysis we use the
402: uniform cost measure.
403: Structures are represented on a RAM in a straightforward way by
404: listing all elements of the universe and then all tuples in the
405: relations. For details we refer the reader to \cite{flufrigro00}.
406: We define the \emph{size} of a $\tau$-structure $\mathcal A$ to be
407: $||\mathcal A||:=|A|+\sum_{R\in\tau\;r\text{-ary}}r\cdot|R^{\mathcal
408: A}|$; this is the length of a reasonable representation of $\mathcal A$
409: (if we suppress details that are inessential for us).
410:
411:
412: \section{Gaifman's Theorem}
413: The \emph{Gaifman graph} of a $\tau$-structure $\mathcal
414: A$ is the graph $\mathcal G_{\mathcal A}$ with vertex set $G_{\mathcal
415: A}:=A$ and an edge between two vertices $a,b\in A$ if there exists
416: an $R\in\tau$ and a tuple $(a_1,\ldots,a_k)\in R^{\mathcal A}$ such
417: that $a,b\in\{a_1,\ldots,a_k\}$. The \emph{distance} $d^{\mathcal
418: A}(a,b)$ between two elements $a,b\in A$ of a structure $\mathcal A$
419: is the length of the shortest path in $\mathcal G_{\mathcal A}$
420: connecting $a$ and $b$. For $r \ge 1$ and $a \in A$ we define the
421: \emph{$r$-neighborhood} of $a$ in $\mathcal A$ to be $N^{\mathcal
422: A}_r(a) := \{ b \in A\mid d^{\mathcal A}(a,b) \le r \}$. For a
423: subset $B\subseteq A$ we let $N_r^{\mathcal A}(B):=\bigcup_{b\in
424: B}N_r^{\mathcal A}(b)$.
425:
426: For every $r\ge 0$ there is a first-order formula $\delta_r(x,y)$ such
427: that for all $\tau$-structures $\mathcal A$ and $a,b\in A$ we have $\mathcal
428: A\models\delta_r(a,b)\iff d^{\mathcal A}(a,b)\le r$. For example, if
429: $\tau=\{E,T\}$ consists of a binary and a ternary relation symbol, we let
430: \begin{align*}
431: \delta_0(x,y):=&(x=y)\\
432: \delta_1(x,y):=&\delta_0(x,y)\vee Exy\vee Eyx\vee\exists z\big(Txyz\vee
433: Tyxz\vee Txzy\vee Tyzx\vee Tzxy\vee Tzyx\big)\\
434: \delta_2(x,y):=&\delta_0(x,y)\vee\delta_1(x,y)\vee\exists z\big(\delta_1(x,z)\wedge\delta_1(z,y)\big)
435: \end{align*}
436: In the following, we write $d(x,y)\le r$ instead of $\delta_r(x,y)$
437: and $d(x,y)> r$ instead of $\neg\delta_r(x,y)$.
438:
439: If $\phi(x)$ is a first-order formula, then $\phi^{N_r(x)}(x)$ is the
440: formula obtained from $\phi(x)$ by relativizing all quantifiers to
441: $N_r(x)$, that is, by replacing every subformula of the form $\exists
442: y\psi(x,y,\bar z)$ by $\exists y(d(x,y)\le r\wedge\psi(x,y,\bar z))$
443: and every subformula of the form $\forall y\psi(x,y,\bar z)$ by
444: $\forall y(d(x,y)\le r\rightarrow\psi(x,y,\bar z))$. A formula
445: $\psi(x)$ of the form $\phi^{N_r(x)}(x)$, for some $\phi(x)$, is
446: called \emph{$r$-local}. The basic property of $r$-local formulas
447: $\psi(x)$ is that it only depends on the $r$-neighborhood of $x$
448: whether they hold at $x$ or not, that is, for all structures $\mathcal
449: A$ and $a\in A$ we have $\mathcal A\models\psi(a)\iff\big\langle
450: N_r^{\mathcal A}(a)\big\rangle\models\psi(a)$.
451:
452: \begin{theorem}[Gaifman \cite{gai81}]\label{gaifman}
453: Every first-order sentence is equivalent to a Boolean combination of
454: sentences of the form
455: \[
456: \exists x_1\ldots\exists x_k\big(\bigwedge_{1\le i<j\le
457: k}d(x_i,x_j)>2r\wedge \bigwedge_{1\le i\le
458: k}\psi(x_i)\big),
459: \]
460: for suitable $r,k\ge 1$ and an $r$-local $\psi(x)$.
461: \end{theorem}
462:
463: \section{Tree-width}\label{seccou}
464: A \emph{tree} is an acyclic graph.
465: A \emph{tree-decomposition} of a $\tau$-structure ${\mathcal A}$ is a
466: pair $(\mathcal T,(B_t)_{t\in T})$, where $\mathcal T$ is a tree and
467: $(B_t)_{t\in T}$ a family of subsets of $A$ (called the \emph{blocks}
468: of the decomposition) such that
469: \begin{enumerate}
470: \item For every $a\in A$, the set $\{t\in T\mid a\in B_t \}$
471: is non-empty and connected in $\mathcal T$ (that is, induces a subtree).
472: \item For every $R\in\tau$ and all $\bar a\in R^{\mathcal A}$ there
473: is a $t\in T$ such that $\bar a\in B_t$.
474: \end{enumerate}
475: The \emph{width} of a tree-decomposition $(\mathcal T,(B_t)_{t\in T})$
476: is $\max\{|B_t|\mid t\in T \}-1$. The \emph{tree-width} $\tw({\mathcal
477: A})$ of ${\mathcal A}$ is the minimal width of a tree-decomposition
478: of ${\mathcal A}$.
479:
480: We occasionally use the following simple fact (cf.\ \cite{GMXIII}).
481:
482: \begin{lemma}\label{lem:linsize}
483: Let $w\ge 1$ and $\tau$ a vocabulary. Then there is a constant $c$
484: such that for every $\tau$-structure $\mathcal A$ of tree-width at
485: most $w$ we have $||\mathcal A||\le c|A|$.
486: \end{lemma}
487:
488: Bodlaender \cite{bod96} proved that for each $w\ge 1$ there is a
489: linear time algorithm that, given a graph $\mathcal G$, either
490: computes a tree-decomposition of $\mathcal G$ of width at most $w$, or
491: rejects $\mathcal G$ if $\tw(\mathcal G)>w$. This result is underlying
492: most of the linear time algorithms on graphs of bounded tree-width.
493: Using the well-known fact that a structure $\mathcal
494: A$ has the same tree-width as its Gaifman graph $\mathcal G_{\mathcal
495: A}$, Bodlaender's result can easily be extended to arbitrary
496: relational structures.
497:
498: Recall Courcelle's theorem that we mentioned in the introduction:
499:
500: \begin{theorem}[Courcelle \cite{cou90}]\label{theo:cou}
501: Let $w\ge 1$. Then for every sentence $\phi$ of monadic second-order
502: logic there is a linear time algorithm that decides whether a given
503: structure $\mathcal A$ of tree-width at most $w$ satisfies $\phi$.
504: \end{theorem}
505:
506: Monadic second-order logic is an extension of first-order logic that
507: also allows quantification over sets.
508:
509: Using known techniques for algorithms on graphs of bounded tree-width,
510: it is not hard to prove the following lemma (see \cite{flufrigro00}).
511: We are only going to use the first-order version of the lemma later.
512:
513: \begin{lemma}\label{lem:cou}
514: Let $w\ge 1$. Then for every formula $\phi(x)$ of monadic
515: second-order logic there is a linear time algorithm that, given a
516: graph $G$ of tree-width at most $w$, computes the set $\phi(\mathcal A):=\{a\in
517: V^G\mid G\models\phi(a)\}$.
518: \end{lemma}
519:
520: \section{Local Tree-Width}\label{sec:ltw}
521:
522: \begin{definition}
523: \begin{enumerate}
524: \item
525: The \emph{local tree-width} of a structure ${\mathcal A}$ is the function $\ltw^{\mathcal A}:\mathbb N\rightarrow\mathbb N$ defined by
526: \[
527: \ltw^{\mathcal A}(r):=\max\big\{\tw(\langle N^{\mathcal
528: A}_r(a)\rangle)\bigmid a\in A\big\}.
529: \]
530:
531: \item
532: A class $\CC$ of structures has \emph{bounded local tree-width} if
533: there is a function $f:\mathbb N\rightarrow\mathbb N$ such that
534: $\ltw^{{\mathcal A}}(r)\le f(r)$ for all ${\mathcal A}\in\mathcal \CC$, $r\in\mathbb N$.
535: \end{enumerate}
536: \end{definition}
537:
538: \begin{example}\emph{Structures of bounded tree-width.}
539: Let ${\mathcal A}$ be a structure of tree-width at most $k$. Then
540: $\ltw^{\mathcal A}(r)\le k$ for all $r\in\mathbb N$.
541: \end{example}
542:
543: The \emph{valence} of a structure $\mathcal A$ is the maximal number
544: of neighbors of a vertex $a\in A$ in the Gaifman graph $\mathcal
545: G_{\mathcal A}$, i.e.\ $\max_{a\in A}|\{b\mid(a,b)\in E^{\mathcal
546: G_{\mathcal A}}\}|$.
547:
548: \begin{example}\label{ex:val}\emph{Structures of bounded valence.}
549: Let ${\mathcal A}$ be a structure of valence at most $l$, for an
550: $l\ge 1$. Then $\ltw^{\mathcal A}(r)\le l(l-1)^{r-1}$ for all
551: $r\in\mathbb N$.
552: \end{example}
553:
554: \begin{example}[Robertson and Seymour \cite{GMIII}]\label{ex:planar}\emph{Planar Graphs.}
555: The class of planar graphs has bounded local tree-width. More
556: precisely, for every planar graph $G$ and $r\ge 1$ we have
557: $\ltw^G(r)\le 3r$.
558: \end{example}
559:
560: \begin{example}[Eppstein \cite{epp99}]\label{ex:genus}\emph{Graphs of bounded genus.}
561: Let $S$ be a surface. Then the class of all graphs embeddable in $S$
562: has bounded local tree-width. More precisely, there is a constant $c$
563: such that for all graphs $G$ embeddable in $S$ and for all $r\ge 0$ we
564: have $\ltw^G(r)\le c\cdot g(S)\cdot r$.
565: \end{example}
566:
567: \begin{example}
568: We can view a simplicial complex as a hypergraph whose vertices are
569: the corners of the complex. Then it is easy to see that the class of
570: all simplicial complexes homeomorphic to a 2-manifold has bounded local
571: tree-width.
572: \end{example}
573:
574: Recall that a \emph{minor} of a graph $\mathcal G$ is a graph
575: $\mathcal H$ that is obtained from a subgraph of $\mathcal G$ by
576: contracting edges. The class of planar graphs, and, more generally,
577: the classes of graphs of bounded genus are examples of classes of
578: graphs that are closed under taking minors. Eppstein gave
579: the following nice characterization of all classes of graphs of
580: bounded loocal tree-width that are closed under taking minors.
581: An \emph{apex graph} is a graph $G$ that has a
582: vertex $v\in V^G$ such that $G\setminus\{v\}$ is planar.
583:
584: \begin{theorem}[Eppstein \cite{epp99a,epp99}]\label{theo:apex}
585: Let $\CC$ be a minor-closed class of graphs. Then $\CC$ has bounded local tree-width if, and only if, $\CC$ does
586: not contain all apex graphs.
587: \end{theorem}
588:
589: This yields further examples of classes of graphs of bounded local
590: tree-width. For example, for every $n\ge 1$, the class of all graphs
591: that do not contain the graph $K_{3,n}$ as a minor has bounded local tree-width. ($K_{m,n}$
592: denotes the complete bipartite graph with parts of size $m$ and $n$,
593: respectively.)
594:
595: \medskip
596: Note that a structure has the same local tree-width as its Gaifman
597: graph, so Examples \ref{ex:planar} and \ref{ex:genus} and Theorem
598: \ref{theo:apex} also give rise to examples of classes of structures of
599: arbitrary vocabularies that have bounded local tree-width.
600:
601: \medskip
602: One of the nice things about bounded local tree-width is that the
603: notion is quite flexible. Think of a structure modeling a subway
604: map. The Gaifman graph of this structure will probably be close to
605: planar, but there may be some edges crossing. Therefore, it may be the
606: case that planar graph algorithms do not apply, although the graph is
607: almost planar. On the other hand, the local tree-width of the graph is
608: probably very close to that of a planar graph, and we can still use our
609: algorithms for graphs of bounded local tree-width.
610:
611:
612: \section{Neighborhood and tree covers}\label{sec:tc}
613: To explore the local tree-likeness of structures of bounded local
614: tree-width we need to cover them by structures of small tree-width in
615: a suitable way. The most general approach is to use \emph{sparse
616: neighborhood covers}, as they have been studied, for instance, in
617: \cite{awepel90,awebercowpel93,pel93}.
618:
619: \begin{definition}
620: Let $r,s\ge 0$. An \emph{$(r,s)$-neighborhood cover} of a structure $\mathcal
621: A$ is a family $\mathcal N$ of subsets of $A$ with the following
622: properties:
623: \begin{enumerate}
624: \item
625: For every $a\in A$ there exists a $N\in\mathcal N$ such that
626: $N_r^{\mathcal A}(a)\subseteq N$.
627: \item
628: For every $N\in\mathcal N$ there exists an $a\in A$ such that
629: $N\subseteq N_s^{\mathcal A}(a)$.
630: \end{enumerate}
631: \end{definition}
632:
633: We define the \emph{size} of a family $\mathcal N$ of sets to be
634: $||\mathcal N||:=\sum_{N\in\mathcal N}|N|$. Recall that the size of a
635: $\tau$-structure $\mathcal A$ is $||\mathcal
636: A||=|A|+\sum_{R\in\tau\;r-\text{ary}}r|R^{\mathcal A}|$. The algorithm of the
637: following lemma is an adaptation of an algorithm due to Peleg \cite{pel93} to
638: our situation. We think it is worthwhile to present our version of
639: the algorithm in some detail.
640:
641: \begin{lemma}[Peleg \cite{pel93}]\label{lem:pel}
642: Let $k\ge 1$. Then there is an algorithm
643: that, given a graph $\mathcal G$ and an $r\ge 1$, computes an
644: $(r,2kr)$-neighborhood cover $\mathcal N$ of $\mathcal G$ of size
645: $||\mathcal N||=O(|G|^{1+(1/k)})$ in time $O\big(\sum_{N\in\mathcal N}||\langle
646: N\rangle^{\mathcal G}||\big)$.
647: \end{lemma}
648:
649: \proof
650: The algorithm is described in Figure \ref{fig:alg1}. It iteratively
651: computes a neighborhood cover $\mathcal N$, maintaining a set $H$ of
652: vertices whose $r$-neighborhood has not yet been covered by a set in
653: $\mathcal N$. In each iteration step of the main loop in Lines 3--13,
654: the algorithm picks an arbitrary vertex $a\in H$ and starts to compute
655: increasing neighborhoods of $a$ (in Lines 6--10) until a certain threshold is reached
656: (cf.\ Line 10). Then it adds the computed set $N$ to the cover
657: $\mathcal N$ and removes all points whose neighborhood has now been
658: covered from $H$, before it goes to the next iteration of the main
659: loop. This process is repeated until $H$ is empty.
660: \begin{figure}[ht]
661:
662: \begin{center}
663: \fbox{\parbox{10cm}{
664: \textbf{Input:} Graph $\mathcal G$, $r\ge 1$
665:
666: \begin{algorithm}
667: \im{0}
668: $H:=G$
669: \im{0}
670: $\mathcal N:=\emptyset$
671: \im{0}
672: \WHILE\ $H\neq\emptyset$ \DO
673: \im{1}
674: choose arbitrary $a\in H$
675: \im{1}
676: $N:=\{a\}$
677: \im{1}
678: \DO
679: \im{2}
680: $M:=N$
681: \im{2}
682: $L:=N_r^{\mathcal G}(M)\cap H$
683: \im{2}
684: $N:=N_r^{\mathcal G}(L)$
685: \im{1}
686: \WHILE\ $|N|>n^{1/k}|M|$ \OD
687: \im{1}
688: $\mathcal N:=\mathcal N\cup\{N\}$
689: \im{1}
690: $H:=H\setminus L$
691: \im{0}
692: \OD
693: \end{algorithm}
694:
695: \textbf{Output:} $\mathcal N$
696: }}
697: \end{center}
698: \caption{}\label{fig:alg1}
699: \end{figure}
700:
701: Now let $\mathcal G$ be a graph, $n:=|G|$, and $r\ge 1$. Let $\mathcal
702: N$ be the cover computed by the algorithm.
703:
704: \medskip
705: \textit{Claim 1. }
706: For every $a\in G$ there exists a $N\in\mathcal N$ such that
707: $N_r(a)\subseteq N$.
708:
709: \smallskip
710: \textit{Proof: }An element $a$ is removed from the set $H$ of
711: uncovered elements in Line 12 if it belongs to a set $L$ such that
712: $N=N_r^{\mathcal G}(L)$ has been added to $\mathcal N$. Of course this
713: $N$ contains $N_r^{\mathcal G}(a)$.
714: This proves Claim 1.
715:
716: \medskip
717: \textit{Claim 2. }
718: For every $N\in\mathcal N$ there exists an $a\in G$ such that
719: $N\subseteq N_{2kr}^{\mathcal G}(a)$.
720:
721: \smallskip
722: \textit{Proof: }We consider the iteration of the main loop that leads
723: to the definition of $N$. Let $a$ be the element chosen in Line 4, and
724: let $N_0:=\{a\}$. Let $l\ge 1$ be the number of times the loop in
725: Lines 6--10 is repeated. For $1\le i\le l$, let $N_i$ be the value of
726: $N$ after the $i$th iteration. Then for $1\le i\le l-1$ we have
727: $|N_i|>n^{1/k}|N_{i-1}|$, and therefore $|N_i|>n^{i/k}$. Thus $l\le
728: k$.
729:
730: Furthermore, it is easy to see that for $1\le i\le l$ we have
731: $N_i\subseteq N_{2ir}^{\mathcal G}(a)$. This implies Claim 2.
732:
733: \medskip
734: Claims 1 and 2 show that $\mathcal N$ is indeed an
735: $(r,2kr)$-neighborhood cover of $\mathcal G$. The following Claim 3
736: shows that the cover is not too large.
737:
738: \medskip
739: \textit{Claim 3. }
740: $||\mathcal N||\le n^{1+(1/k)}$.
741:
742: \smallskip
743: \textit{Proof: }
744: For $N\in\mathcal N$, and let $M$ be the corresponding set that is
745: computed in the last iteration of the loop in Lines 6--10 that let to
746: $N$ (i.e.\ $M$ is the value of $N$ after the second but last
747: iteration of the loop).
748:
749: We first show that for distinct $N_1,N_2\in\mathcal N$ we have
750: $M_1\cap M_2=\emptyset$. To see this, suppose that $N_1$ is computed
751: first. Let $H_1$ be the value of $H$ after the iteration of the main
752: loop in which $N_1$ has been computed. Note that for every $a\in M_1$ and
753: $b\in H_1$ we have $d^{\mathcal G}(a,b)>r$. Moreover, $M_2\subseteq
754: N_2\subseteq N_r^{\mathcal G}(H_1)$. Thus $M_1\cap M_2=\emptyset$.
755:
756: Noting that by the condition of Line 10, for all $N\in\mathcal N$ we
757: have $|N|\le n^{1/k}|M|$, we obtain
758: \[
759: ||\mathcal N||=\sum_{N\in\mathcal N}|N|\le n^{1/k}\sum_{N\in\mathcal
760: N}|M|\le n^{1/k}\cdot n.
761: \]
762: The last inequality holds because the $M$ are disjoint subsets of
763: $G$. This proves Claim 3.
764:
765: \medskip
766: It remains to estimate the running time of the algorithm. We claim
767: that each iteration of the main loop requires time $O(\langle
768: N\rangle^{\mathcal G})$, for the $N$ added to $\mathcal N$ in
769: this iteration. To see this, note that essentially we have to do a
770: breadth-first search on $N$ starting in $a$. To compute $L$ in Line 8, we may have to explore some
771: edges not contained in $\langle L\rangle$. However, all these edges belong to
772: $\langle N_r^{\mathcal G}(L)\rangle=\langle N\rangle$.
773:
774: It may seem that to check the condition of Line 10 we need
775: multiplication, which is not available as basic operation of a
776: standard RAM. However, before we start the main computation we can
777: produce tables that store the values $m^l$ and $m^l\cdot n$ for $1\le
778: l\le k$, $1\le m\le n$ in linear time on a standard RAM. (We use the
779: fact that
780: \[
781: (m+1)^l=\sum_{(\epsilon_1,\ldots,\epsilon_l)\in\{0,1\}^l}m^{\sum_{i=1}^l\epsilon_i}
782: \]
783: to inductively compute the tables. Remember that we treat $k$ as a
784: constant.) Then we can use these tables to check the condition of
785: Line 10 in constant time.
786: \proofend
787:
788: \begin{corollary}\label{cor:ncov}
789: Let $k,r\ge 1$, $\tau$ a vocabulary, and $\CC$ a class of $\tau$-structures of
790: bounded local tree-width. Then there is an algorithm that, given a structure
791: $\mathcal A\in \CC$, computes an $(r,2kr)$-neighborhood cover $\mathcal N$ of
792: $\mathcal A$ of size $||\mathcal N||=O(|A|^{1+(1/k)})$ in time
793: $O(|A|^{1+(1/k)})$.
794: \end{corollary}
795:
796: \proof Since neighborhoods of radius $2kr$ in structures in $\CC$ have bounded tree-width, by Lemma \ref{lem:linsize} there is a constant
797: $c$ such that for every structure $\mathcal A\in \CC$, every
798: $(r,2kr)$-neighborhood cover $\mathcal N$ of $\mathcal A$, and every
799: $N\in\mathcal N$ we have
800: \begin{equation}\label{eq:nc1}
801: ||\langle N\rangle^{\mathcal A}||\le c|N|.
802: \end{equation}
803: This implies $||\mathcal A||\le c||\mathcal N||$.
804:
805: Our algorithm first computes the Gaifman graph $\mathcal G_{\mathcal
806: A}$ of the input structure $\mathcal A$, which is possible in time
807: $O(||\mathcal A||)$. Then it computes an an $(r,2kr)$-neighborhood
808: cover $\mathcal N$ of $\mathcal A$ of size $||\mathcal
809: N||=O(|A|^{1+(1/k)})$. By Lemma \ref{lem:pel} and \eqref{eq:nc1}, this is
810: possible in time $O(||\mathcal N||)=O(|A|^{1+(1/k)})$.
811: \proofend
812:
813: The following consequence of the proof of the previous corollary is
814: worth being noted:
815:
816: \begin{corollary}\label{cor:avdegbltw}
817: Let $\tau$ be a vocabulary and $\CC$ be a class of $\tau$-structures of
818: bounded local tree-width. Then for every $k\ge1$ there is a constant
819: $c$ such that for all structures $\mathcal A\in \CC$ we have $||\mathcal
820: A||\le c|A|^{1+(1/k)}$.
821: \end{corollary}
822:
823: As a matter of fact, a neighborhood cover is more than we need. Often, the
824: following weaker notion of a \emph{tree cover} leads to better results.
825:
826: \begin{definition}
827: Let $r,w\ge 0$. An \emph{$(r,w)$-tree cover} of a structure $\mathcal
828: A$ is a family $\mathcal T$ of subsets of $A$ with the following
829: properties:
830: \begin{enumerate}
831: \item
832: For every $a\in A$ there exists a $T\in\mathcal T$ such that
833: $N_r^{\mathcal A}(a)\subseteq T$.
834: \item
835: For every $T\in\mathcal T$ we have $\tw(\langle T\rangle^{\mathcal A})\le w$.
836: \end{enumerate}
837: \end{definition}
838:
839: Note that an $(r,s)$-neighborhood cover of a structure $\mathcal A$ is an
840: $(r,\ltw^{\mathcal A}(s))$-tree cover of $\mathcal A$. The following lemma is
841: implicit in \cite{epp99}:
842:
843: \begin{lemma}[Eppstein \cite{epp99}]\label{lem:mintc}
844: Let $r\ge 0$ and $\CC$ be a class of graphs that is closed under taking minors
845: and has bounded local tree-width. Let $f:\mathbb N\rightarrow\mathbb N$ be a
846: function bounding the local tree-width of the graphs in $\CC$.
847:
848: Then there is an algorithm that, given a graph $\mathcal G\in \CC$, computes an $(r,f(2r+1))$-tree cover $\mathcal T$ of $\mathcal G$ of
849: size $||\mathcal T||=O(|G|)$ in time $O(|G|)$.
850: \end{lemma}
851:
852: \proof
853: Let $\mathcal G\in \CC$ and choose an arbitrary vertex $a_0\in G$. For
854: $0\le i\le j$, let $G[i,j]:=\{a\in G\mid i\le
855: d^G(a_0,a)\le j\}$.
856:
857: We claim that $\tw(\langle G[i,j]\rangle)\le
858: f(j-i+1)$. This is immediate if $i=0$ or $i=1$, because then
859: $G[i,j]\subseteq N_{j}^{\mathcal G}(a_0)$. If $i>1$, we simply contract the
860: connected subgraph $\langle G[0,i-1]\rangle^{\mathcal G}$ to a single vertex $b_0$. We obtain a minor
861: $\mathcal G'$ of $\mathcal G$, which is also an element of $\CC$ by our
862: assumption that $\CC$ is closed under taking minors. $\mathcal G'$ still
863: contains the set $G[i,j]$ as it is, but this set is contained in
864: $N_{j-i+1}^{\mathcal G'}(b_0)$. This proves the claim.
865:
866: The claim implies that for all $r\ge 0$, the family $\mathcal
867: T:=\{G[i,i+2r]\mid i\ge 0\}$ is an $(r,f(2r+1))$-tree cover of
868: $\mathcal G$ of size at most $(2r+1)|G|$.
869: On input $\mathcal G$, we can choose an arbitrary $a_0$ and then compute this
870: tree cover in linear time by breadth-first search.
871: \proofend
872:
873: The existence of a tree-cover of size linear in the size of the structure and
874: a linear time algorithm computing such a cover is exactly what we need in our
875: algorithms of the next section. This justifies the following definition:
876:
877: \begin{definition}
878: A class $\CC$ of graphs is \emph{locally tree-decomposable} if there is a
879: function $g:\mathbb N\to\mathbb N$ and an algorithm that, given a structure
880: $\mathcal A\in \CC$ and an $r\in\mathbb N$, computes an $(r,g(r))$-tree cover of
881: $\mathcal A$ of size $O(|A|)$ in time $O(|A|)$.\footnote{The hidden constants
882: in the $O(\cdot)$-notation may depend on $r$.}
883: \end{definition}
884:
885: \begin{satzform}{}{Examples}
886: All examples of classes of structures of bounded local tree-width that we gave
887: in Section \ref{sec:ltw} are actually locally tree-decomposable.
888:
889: For Example \ref{ex:val}, classes of structures of bounded valence,
890: this is trivial: If $\mathcal A$ is a structure of valence $l$ and
891: $r\ge 0$, then the family $\{N_r^{\mathcal A}(a)\mid a\in A\}$ is an
892: $(r,l(l-1)^{r-1})$-tree cover of $\mathcal A$.
893:
894: For all other examples, it follows from Lemma \ref{lem:mintc}.
895: \end{satzform}
896:
897: The following proposition is an immediate consequence of the
898: definition of locally tree-decomposable classes of structures:
899:
900: \begin{proposition}\label{prop:avdegltd}
901: Let $\tau$ be a vocabulary and $\CC$ be a locally tree-decomposable class of $\tau$-structures. Then there is a constant
902: $c$ such that for all structures $\mathcal A\in \CC$ we have $||\mathcal
903: A||\le c|A|$.
904: \end{proposition}
905:
906: We close this section with an example showing that the analogue of
907: Proposition \ref{prop:avdegltd} for classes of bounded local
908: tree-width is wrong. Remember Corollary \ref{cor:avdegbltw}, though.
909:
910: \begin{example}\label{ex:bltwsize}
911: We construct a class $\CC$ of graphs of bounded local tree-width such
912: that for every constant $c$ there is a graph $\mathcal G\in \CC$ with
913: $||\mathcal G||\ge c|G|$.
914:
915: We use the following theorem due to Erd\"os \cite{erd59}: \emph{For
916: all $g,k\ge 1$ there exists a graph of girth greater than $g$ and
917: chromatic number greater than $k$.} Remember that the \emph{girth}
918: $g(\mathcal G)$ of a graph $\mathcal G$ is the length of the
919: shortest cycle in $\mathcal G$ and the chromatic number
920: $\chi(\mathcal G)$ of $\mathcal G$ is the least number of colors
921: needed to color the vertices of $\mathcal G$ in such a way that no
922: two adjacent vertices have the same color. It is easy to see that every
923: graph $\mathcal G$ with $\chi(\mathcal G)\ge k$ has a connected subgraph
924: $\mathcal H$ with average degree
925: \[
926: \frac{2|E^{\mathcal H}|}{\mathcal V^{\mathcal H}}\ge k-1
927: \]
928: (cf.\ \cite{die00}, p.~98).
929:
930: The \emph{diameter} of a connected graph $\mathcal G$ is the number
931: $\diam(\mathcal G):=\max\{d^{\mathcal G}(a,b)\mid a,b\in G\}$.
932:
933: We inductively construct a family $(\mathcal G_i)_{i\ge 1}$ of
934: graphs as follows: $\mathcal G_1$ is the graph consisting of two
935: vertices and an edge between them. Suppose now that $\mathcal G_i$
936: is already defined. Let $\mathcal G_{i+1}'$ be a graph with
937: $g(\mathcal G_{i+1}')\ge 2\diam(\mathcal G_i)+1$ and $\chi(\mathcal
938: G'_{i+1})\ge 2i+3$. Let $\mathcal G_{i+1}$ be a connected subgraph of
939: $\mathcal G_{i+1}'$ with
940: \[
941: \frac{2|E^{\mathcal G_{i+1}}|}{\mathcal
942: V^{\mathcal G_{i+1}}}\ge 2i+2.
943: \]
944: Clearly, $g(\mathcal G_{i+1})\ge
945: g(\mathcal G'_{i+1})\ge2\diam(\mathcal G_i)+1$.
946:
947: Observe that for every $r\ge 1$ and every graph $\mathcal G$, if
948: $2r+1< g(\mathcal G)$ then $\ltw^{\mathcal G}(r)\le1$. Moreover,
949: if $\mathcal G$ is connected then
950: $\ltw^{\mathcal G}(r)= \tw(\mathcal G)$ for all $r\ge\diam(\mathcal
951: G)$. For every $i\ge 1$ and $\diam(\mathcal G_i)\le
952: r<\diam(\mathcal G_{i+1})$, we let $f(r):=\max\{\tw(\mathcal
953: G_i),\ltw^{\mathcal G_{i+1}}(r)\}$. We claim that $\ltw^{\mathcal
954: G_i}(r)\le f(r)$ for all $i,r\ge 1$. This is obvious for $i=1$. For
955: $i\ge 2$, we have to
956: distinguish between three cases: If $r<\diam(\mathcal
957: G_{i-1})\le\frac{1}{2}(g(\mathcal G_i)-1)$, then $\ltw^{\mathcal
958: G_{i}}(r)\le1\le f(r)$. If $\diam(\mathcal
959: G_{i-1})\le r<\diam(\mathcal G_i)$, then $\ltw^{\mathcal
960: G_i}(r)\le f(r)$ immediately by the definition of $f$. If
961: $r\ge\diam(\mathcal G_i)$, then $\ltw^{\mathcal G_i}(r)=\tw(\mathcal
962: G_i)\ge f(r)$.
963:
964: Thus the class $\CC:=\{\mathcal G_i\mid i\ge 1\}$ has bounded local
965: tree-width. On the other hand, for every $i\ge 2$ we have
966: $
967: ||\mathcal G_i||\ge|E^{\mathcal G_i}|\ge i|G_i|.
968: $
969: \end{example}
970:
971: \section{The main algorithm}
972: Throughout this section, we fix a vocabulary $\tau$. We shall first prove two lemmas.
973:
974: \begin{lemma}\label{lem:ma1}
975: Let $\CC$ be a class of $\tau$-structures of bounded local tree-width and $r,w\ge
976: 1$. Then there is an algorithm that solves the
977: following problem in time $O(||\mathcal T||)$:
978:
979: \prob{Structure $\mathcal A\in \CC$, $(r,w)$-tree cover $\mathcal T$ of $\mathcal
980: A$}{Compute $K_T:=\{a\in A\mid N_r^{\mathcal A}(a)\subseteq T\}$ for
981: all $T\in\mathcal T$}
982: \end{lemma}
983:
984: \proof Observe that $||\mathcal A||=O(||\mathcal T||)$, because by
985: Lemma \ref{lem:linsize}, for all $T\in\mathcal T$ we have $||\langle
986: T\rangle^{\mathcal A}||=O(|T|)$.
987:
988: Without loss of generality we can assume that $\mathcal A$ is a graph;
989: if not we first compute its Gaifman graph. This is possible in time
990: $O(||\mathcal A||)$. Furthermore, we can assume that the universe $A$ of
991: $\mathcal A$ is the set
992: $\{1,\ldots,n\}$ (see the appendix of \cite{flufrigro00} for details).
993:
994: Let $T\in\mathcal T$, we show how to compute $K_T$ in time $O(|T|)$.
995: We suppose that $T$ is given as a list $a_1,\ldots,a_m$ of its
996: elements. Our algorithm is displayed in Figure \ref{fig:alg3}. $K_T$
997: is computed iteratively, during the computation the current state of
998: the set is stored in an array $K$ of length $n$. Note that we do not
999: initialize the array to 0 in the beginning (we do not have the time to
1000: do that). Instead, we maintain a second ``control array'' $\Gamma$ of
1001: length $m$. The $j$th entry of $\Gamma$ is $a_j$, for $j=1$ to
1002: $m$. $\Gamma$ is initialized to these values in Line 1.
1003: Then at every stage in the computation, the set of all elements
1004: represented by the array $K$ is
1005: \[
1006: S(K):=\{a\in A\mid K[a]\in\{1,\ldots,m\}\text{ and }\Gamma[K[a]]=a\}.
1007: \]
1008: After Line 2 is executed, we have $S(K)=T$.
1009:
1010: Now the main loop in Lines 3--13 iteratively removes those elements
1011: from $S(K)$ whose neighbors are not all contained in $S(K)$. Thus
1012: after the $i$th iteration we have
1013: \[
1014: S(K)=\{a\in T\mid N_i^{\mathcal A}(a)\not\subseteq T\}.
1015: \]
1016: So once we enter Line 15, we have $S(K)=K_T$. Lines 15--17 retrieve
1017: this set from the array $K$.
1018: \begin{figure}[ht]
1019: \begin{center}
1020: \fbox{\parbox{12cm}{
1021: \textbf{Input: }${\mathcal A}$,
1022: $T=\{a_1,\ldots,a_m\}\subseteq A$
1023: \begin{algorithm}
1024: \im{0}
1025: \FOR\ $j=1$ \TO\ $m$ \DO\ $\Gamma[j]:=a_j$ \OD
1026: \im{0}
1027: \FOR\ $j=1$ \TO\ $m$ \DO\
1028: $K[a_j]:=j$
1029: \OD
1030: \im{0}
1031: \FOR\ $i=1$ \TO\ $r$ \DO
1032: \im{1}
1033: $\text{temp}:=\emptyset$
1034: \im{1}
1035: \FOR\ $j=1$ \TO\ $m$ \DO
1036: \im{2}
1037: \IF\ $a_j$ has a neighbor $b$ such that
1038: \im{4}
1039: $\Big(\hspace{5mm}K[b]\not\in\{1,\ldots,m\}$
1040: \im{4.2}
1041: \OR\ $\big(K[b]\in\{1,\ldots,m\}$
1042: \AND\ $\Gamma[K[b]]\neq b\big)\Big)$ \THEN
1043: \im{3}
1044: $\text{temp}:=\text{temp}\cup\{a_j\}$
1045: \im{2}
1046: \FI
1047: \im{1}
1048: \OD
1049: \im{1}
1050: \FORALL\ $a\in\text{temp}$ \DO
1051: \im{2}
1052: $K[a]:=0$
1053: \im{1}
1054: \OD
1055: \im{0}
1056: \OD
1057: \im{0}
1058: $K_T:=\emptyset$
1059: \im{0}
1060: \FOR\ $j=1$ \TO\ $m$ \DO
1061: \im{1}
1062: \IF\ $K[a_j]=j$ \THEN\ $K_T:=K_T\cup\{a_j\}$ \FI
1063: \im{0}
1064: \OD
1065: \end{algorithm}
1066: \textbf{Output: }$K_T$
1067: }}
1068: \end{center}
1069: \caption{}\label{fig:alg3}
1070: \end{figure}
1071:
1072: Let us analyze the running time of the algorithm. Lines 1 and 2
1073: require time $O(m)$. To test the condition of Lines 7--8 requires
1074: constant time for each $b$. To test the condition of Lines 6--8, we
1075: have to step through the list of vertices adjacent to $a_j$ until
1076: either we find a $b$ that does not satisfy the condition or we have
1077: checked all neighbors. This requires a constant amount of work for
1078: every edge with one endpoint $a_j$ and the other endpoint in $S(K)$
1079: and an additional constant amount of work in case we find a neighbor
1080: not in $S(K)$. Thus the execution of the loop in lines 5--11 requires
1081: time $O(m+|E^{{\mathcal A}}\cap T^2|)\le O(||\langle
1082: T\rangle^{\mathcal A}||)=O(m)$. The loop in Lines 12--14 also requires
1083: time $O(m)$. Thus every iteration of the main loop requires time
1084: $O(m)$. Since we treat the number $r$ of iterations as constant, the
1085: overall time required by Lines 3--15 is $O(m)$. Since $K_T\subseteq
1086: T$, Lines 16--19 also require time $O(m)$. \proofend
1087:
1088: \begin{lemma}\label{lem:ma2}
1089: Let $\CC$ be a class of structures of bounded local tree-width and $r,m\ge
1090: 1$. Then the following problem can be solved in time $O(|A|)$:
1091:
1092: \prob{Structure $\mathcal A\in \CC$, set $P\subseteq A$}{Decide if there
1093: exist $a_1,\ldots,a_m\in P$ such that $d^{\mathcal A}(a_i,a_j)>r$}
1094: \end{lemma}
1095:
1096: \proof
1097: Let $f:\mathbb N\rightarrow\mathbb N$ be a function bounding
1098: the local tree-width of the structures in $\CC$.
1099:
1100: Let $\mathcal A\in \CC$ and $P\subseteq A$. Our algorithm is displayed
1101: in Figure \ref{fig:alg4}. It proceeds in two phases.
1102: \begin{figure}[ht]
1103: \begin{center}
1104: \fbox{\parbox{12cm}{
1105: \textbf{Input: }${\mathcal A}\in \CC$, $P\subseteq A$
1106:
1107: \begin{algorithm}
1108: \im{0}
1109: $Q:=P$
1110: \im{0}
1111: $l:=0$
1112: \im{0}
1113: \WHILE\ $Q\neq\emptyset$ \AND\ $l<m$ \DO
1114: \im{1}
1115: $l:=l+1$
1116: \im{1}
1117: choose $a_l\in Q$ arbitrarily
1118: \im{1}
1119: $Q:=Q\setminus N_r^{\mathcal A}(a_l)$
1120: \im{0}
1121: \OD
1122: \im{0}
1123: \IF\ $l=m$ \THEN\
1124: \im{1}
1125: \ACCEPT
1126: \im{0}
1127: \ELSE\
1128: \im{1}
1129: \IF\ $l=0$ \THEN\ \REJECT\ \FI
1130: \im{0}
1131: \FI
1132:
1133: \medskip
1134: \im{0}
1135: compute $H:=N_{2r}^{\mathcal A}(\{a_1,\ldots,a_l\})$
1136: \im{0}
1137: \IF\ $\big(\langle H\rangle^{\mathcal A},P\big)\models\exists x_1\ldots\exists
1138: x_m\Big(\bigwedge_{i=1}^m Px_i\wedge\bigwedge_{1\le i<j\le m}d(x_i,x_j)>r\Big)$ \THEN
1139: \im{1}
1140: \ACCEPT
1141: \im{0}
1142: \ELSE
1143: \im{1}
1144: \REJECT
1145: \im{0}
1146: \FI
1147: \end{algorithm}
1148: }}
1149: \end{center}
1150: \caption{}\label{fig:alg4}
1151: \end{figure}
1152:
1153: In the first phase (Lines 1--12) it iteratively computes
1154: elements $a_1,\ldots,a_i\in P$, for some $i\le m$, such that
1155: $d^{\mathcal A}(a_i,a_j)>r$ for $1\le i<j\le l$ and either $l=m$ or
1156: for all $b\in P$ there is an $i\le l$ such that $b\in N_r^{\mathcal
1157: A}(a_i)$. If $l=m$, the algorithm accepts. If $l=0$, i.e.\
1158: $P=\emptyset$, then it rejects. Otherwise, it goes into the second
1159: phase (Lines 13--18).
1160:
1161: When the algorithm enters Line 13, we have $P\subseteq N_{r}^{\mathcal
1162: A}(\{a_1,\ldots, a_l\})$. Let $\mathcal H:=\langle N_{2r}^{\mathcal
1163: A}(\{a_1,\ldots,a_l\})$. Then for all $b,b'\in P$ we have
1164: $d^{\mathcal A}(b,b')\le r\iff d^{\mathcal H}(b,b')\le r$, because
1165: $P\subseteq N_r^{\mathcal A}(\{a_1,\ldots, a_l\})$ and thus every
1166: path of length at most $r$ between two elements of $P$ must be
1167: contained in $H$. Thus there
1168: exist $b_1,\ldots,b_m\in P$ such that $d^{\mathcal A}(b_i,b_j)>r$ if,
1169: and only if, there exist $b_1,\ldots,b_m\in P$ such that $d^{\mathcal
1170: H}(b_i,b_j)>r$, i.e.\ if the condition in Line 14 is satisfied.
1171: Thus the algorithm is correct
1172:
1173: To estimate the running time, we note that $||\langle N_{r}^{\mathcal
1174: A}(a_i)\rangle^{\mathcal A}||=O(|N_r^{\mathcal A}(a_i)|)$, because
1175: $\CC$ is a class of bounded local tree-width. Since we treat $r$ and $m$
1176: as constants, Lines 1--13 require time $O(|A|)$. It is easy to see
1177: that $\tw(\mathcal H)\le \ltw^{\mathcal A}(2lr)\le f(2lr)$. Thus the
1178: condition in Line 14 can also be checked in time $O(|A|)$ by
1179: Courcelle's Theorem \ref{theo:cou}.
1180: \proofend
1181:
1182:
1183: We are now ready to prove our main results, Theorems \ref{theo:mt1} and
1184: \ref{theo:mt2}. Recall the statements:
1185:
1186: \begin{quote}\itshape
1187: Let $\CC$ be a class of structures of bounded local tree-width and $\phi$ a
1188: sentence of first-order logic.
1189:
1190: \begin{enumerate}
1191: \item
1192: For every $k\ge 1$ there is an algorithm that decides whether a given structure
1193: $\mathcal A\in \CC$ satisfies $\phi$ in time $O(|A|^{1+(1/k)})$.
1194: \item
1195: If $\CC$ is locally tree-decomposable, then there is an algorithm that
1196: solves the problem in time $O(|A|)$.
1197: \end{enumerate}
1198: \end{quote}
1199:
1200:
1201: \proof
1202: We describe the algorithm for (1) and then explain how it has to be
1203: modified to obtain (2).
1204:
1205: By Gaifman's Theorem \ref{gaifman}, without loss of generality we can
1206: assume that $\phi$ is of the form
1207: \[
1208: \exists x_1\ldots\exists x_m\big(\bigwedge_{1\le i<j\le
1209: m}d(x_i,x_j)>2r\wedge \bigwedge_{1\le i\le
1210: m}\psi(x_i)\big),
1211: \]
1212: for suitably chosen $r,m\ge1$ and an $r$-local $\psi$.
1213:
1214: Let $k\ge 1$ and $f:\mathbb N\to\mathbb N$ be a function bounding the local
1215: tree-width of the structures in $\CC$. Let $\tau$ be the vocabulary of
1216: the sentence $\phi$; without loss of generality we can assume that all
1217: structures in $\CC$ are $\tau$-structures.
1218:
1219: Figure \ref{fig:alg2} shows our algorithm.
1220: \begin{figure}[ht]
1221: \begin{center}
1222: \fbox{\parbox{12cm}{
1223: \textbf{Input:} Structure $\mathcal A\in \CC$
1224:
1225: \begin{algorithm}
1226: \im{0}
1227: compute an $(r,2kr)$-neighborhood cover $\mathcal N$ of $\mathcal A$
1228: of size $O(A^{1+(1/k)})$
1229: \im{0}
1230: \FORALL\ $N\in\mathcal N$ \DO
1231: \im{1}
1232: compute $K_N:=\{a\in N\mid N_r^{\mathcal A}(a)\subseteq N\}$
1233: \im{0}
1234: \OD
1235: \im{0}
1236: \FORALL\ $N\in\mathcal N$ \DO
1237: \im{1}
1238: compute $P_N:=\big\{a\in K_N\bigmid \langle N\rangle^{\mathcal
1239: A}\models\psi(a)\big\}$.
1240: \im{0}
1241: \OD
1242: \im{0}
1243: compute $P:=\bigcup_{N\in\mathcal N}P_N$
1244: \im{0}
1245: \IF\ there are $a_1,\ldots,a_m\in P$ such that $d(a_i,a_j)>2r$ for
1246: $1\le i<j\le k$ \THEN\
1247: \im{1}
1248: \ACCEPT
1249: \im{0}
1250: \ELSE
1251: \im{1}
1252: \REJECT
1253: \im{0}
1254: \FI
1255: \end{algorithm}
1256: }}
1257: \end{center}
1258: \caption{}\label{fig:alg2}
1259: \end{figure}
1260:
1261: To see that the algorithm is correct, note that since $\psi(x)$ is
1262: $r$-local we have $P=\{a\in A\mid \mathcal A\models\psi(a)\}$.
1263:
1264: \medskip
1265: So we shall prove that the algorithm can be implemented as an
1266: $O(n^{1+(1/k)})$-algorithm, where $n:=|A|$ is the cardinality of the
1267: input structure.
1268:
1269: Line 1 requires time $O(n^{1+(1/k)})$ by Corollary \ref{cor:ncov}.
1270: Lines 2--4 require time $O(||\mathcal N||)$ by Lemma \ref{lem:ma1}. For
1271: every $N\in\mathcal N$, Line 6 requires time $O(|N|)$ by Lemma
1272: \ref{lem:cou}. Thus the loop in Lines 5--7 also requires time $O(||\mathcal
1273: N||)$. Clearly, Line 8 can be performed in time $O(||\mathcal N||)$,
1274: and the condition in Line 9 can be checked in time $O(|A|)$ by Lemma
1275: \ref{lem:ma2}. Thus the overall running time is $O(||\mathcal
1276: N||)=O(n^{1+(1/k)})$.
1277:
1278: \medskip
1279: It remains to prove (2), but this is very easy now. Instead of a
1280: neighborhood cover, in Line 1 of the algorithm we compute tree cover
1281: of linear size. This can be done in linear time by the definition of a
1282: locally tree-decomposable class of graphs. Since the running time of
1283: the rest of the algorithm is linear in the size of the cover, we
1284: obtain a linear time algorithm.
1285: \proofend
1286:
1287: \section{Concluding remarks}
1288:
1289: \subsection*{Uniformity} A close look at our
1290: proofs shows that actually for each locally tree-decomposable class
1291: $\CC$ of structures there is a recursive function $f:\mathbb
1292: N\to\mathbb N$ and an algorithm that decides, given a
1293: first-order sentence $\phi$ and a structure $\mathcal A\in \CC$,
1294: whether $\mathcal A\models\phi$ in time $O(f(||\phi||)|A|)$,
1295: where $||\phi||$ denotes the length of the
1296: sentence $\phi$. We can obtain an anlogous uniform version of Theorem
1297: \ref{theo:mt2}.
1298:
1299: We stated and proved non-uniform versions of the theorems for the sake
1300: of a clearer presentation.
1301:
1302: \subsection*{Dependence on the formula size}
1303: Our algorithm heavily depends on the size of the formula $\phi$,
1304: roughly the hidden multiplicative constant is $k$-fold
1305: exponential in the length of $\phi$, where $k$ is the number of
1306: quantifier-alternations in $\phi$.
1307:
1308: \subsection*{Practical Considerations}
1309: The large hidden constants seem to make our algorithms useless for
1310: practical purposes. Nevertheless, let us briefly discuss a few more practical
1311: aspects.
1312:
1313: The main factor contributing to the large constants is the complexity
1314: of the formulas, in particular the number of quantifier alternations.
1315: However, if we think of a database application, we will usually only
1316: have to handle very simple formulas. As matter of fact, most database
1317: queries are so called \emph{conjunctive queries}; they can be
1318: defined by first-order formulas of the form $\exists x_1\ldots\exists
1319: x_k(\alpha_1\wedge\ldots\wedge\alpha_m)$. Such formulas do not have
1320: any quantifier alternation. Moreover, when handling conjunctive
1321: queries we can avoid the second very costly part hidden in our
1322: algorithms, namely the transformation of a formula according to Gaifman's
1323: theorem. For all we know, such a transformation may blow up the
1324: formula size by a non-elementary factor. For conjunctive queries, we
1325: can avoid Gaifman's theorem and instead use algorithmic techniques
1326: similar to those in \cite{epp99a}. With these techniques, the
1327: dependence on the formula size can be reduced to a singly exponential
1328: factor, which seems acceptable because usually in practice we have to
1329: evaluate small formulas (queries) in large structures (databases). The
1330: third costly factor is to compute tree-decompositions. Bodlaender's
1331: linear time algorithm is only of theoretical interest due to
1332: very large hidden constants. More promising seems to be an algorithm
1333: due to Reed \cite{ree92} (improving an earlier algorithm due to Robertson
1334: and Seymour \cite{GMXIII}). For an input graph of tree-width $w$ and
1335: size $n$, this algorithm only computes a
1336: tree-decomposition of width at most $4w$. Its running time is not
1337: linear in $n$ (as Bodlaenders), but $O(n\log(n))$. However, the
1338: algorithm is simple and the hidden constants, though exponentially
1339: depending on $w$, do not seem too large for small values of $w$.
1340: Let us also remark that there are much more efficient algorithms for
1341: computing small width tree-decompositions of planar graphs of small
1342: radius \cite{epp99}.
1343:
1344: Nevertheless, as they stand our results are mostly
1345: theoretical. Similarly to Courcelle's Theorem \cite{cou90}, their main
1346: benefit is to provide a quick and simple way to recognize a
1347: property as being linear time computable on certain classes of graphs.
1348: Analyzing the combinatorics of the specific property then, one may
1349: also find a practical algorithm.
1350:
1351: \subsection*{Further Research}
1352: Although Example \ref{ex:bltwsize} shows that for classes $\CC$ of
1353: bounded local tree-width we cannot expect an
1354: algorithm deciding a first-order property of structures $\mathcal
1355: A\in\CC$ in time $O(|A|)$, it does not rule out an $O(||\mathcal
1356: A||)$-algorithm. To obtain such an algorithm, it would be sufficient
1357: to find, for every $r\ge 1$, a $w\ge 1$ and an $O(||\mathcal
1358: A||)$-algorithm that computes an $(r,w)$-tree cover of a structure
1359: $\mathcal A\in\CC$.
1360:
1361: As we mentioned, one of the main factors contributing to the heavy
1362: dependence of the running time of our algorithms on the size of the
1363: formula is the transformation into a ``local formula'' according to
1364: Gaifman's theorem. Though this transformation is clearly effective, as
1365: far as we know its complexity has not been studied. We do expect this
1366: complexity to be non-elementary, but this does not rule out the
1367: existence of more efficient algorithms for particular classes of
1368: formulas (such as existential formulas) or the existence of good
1369: heuristics.
1370:
1371: In general, we consider it as one of the main challenges for further
1372: research to reduce the dependence on the formula size (not only in our
1373: results, but also in Courcelle's theorem). For example, is
1374: there an algorithm that decides, given a first-order sentence $\phi$
1375: and a planar graph $\mathcal G$ (or a tree, or just a word), whether
1376: $\mathcal G\models\phi$ in time $O(2^{|\phi|}n^c)$ for some
1377: fixed-constant $c$?
1378:
1379: %\bibliographystyle{plain}
1380: %\bibliography{endlmod}
1381: \begin{thebibliography}{10}
1382:
1383: \bibitem{ahohopull74}
1384: A.V. Aho, J.E. Hopcroft, and J.D. Ullman.
1385: \newblock {\em The Design and Analysis of Computer Algorithms}.
1386: \newblock Addison-Wesley, 1974.
1387:
1388: \bibitem{ahoull79}
1389: A.V. Aho and J.D. Ullman.
1390: \newblock The universality of data retrieval languages.
1391: \newblock In {\em Conference Record of the Sixth Annual ACM Symposium on
1392: Principles of Programming Languages}, pages 110--120, 1979.
1393:
1394: \bibitem{awebercowpel93}
1395: B.~Awerbuch, B.~Berger, L.~Cowen, and D.~Peleg.
1396: \newblock Near-linear cost sequential and distributed constructions of sparse
1397: neighborhood covers.
1398: \newblock In {\em Proceedings of the 34th Annual IEEE Symposium on Foundations
1399: of Computer Science}, pages 638--647, 1993.
1400:
1401: \bibitem{awepel90}
1402: B.~Awerbuch and D.~Peleg.
1403: \newblock Sparse partitions.
1404: \newblock In {\em Proceedings of the 31st Annual IEEE Symposium on Foundations
1405: of Computer Science}, pages 503--513, 1990.
1406:
1407: \bibitem{bak94}
1408: B.S. Baker.
1409: \newblock Approximation algorithms for {NP}-complete problems on planar graphs.
1410: \newblock {\em Journal of the ACM}, 41:153--180, 1994.
1411:
1412: \bibitem{bod96}
1413: H.L. Bodlaender.
1414: \newblock A linear-time algorithm for finding tree-decompositions of small
1415: treewidth.
1416: \newblock {\em {SIAM} Journal on Computing}, 25:1305--1317, 1996.
1417:
1418: \bibitem{bod97}
1419: H.L. Bodlaender.
1420: \newblock Treewidth: Algorithmic techniques and results.
1421: \newblock In I.~Privara and P.~Ruzicka, editors, {\em Proceedings 22nd
1422: International Symposium on Mathematical Foundations of Computer Science,
1423: MFCS'97}, volume 1295 of {\em Lecture Notes in Computer Science}, pages
1424: 29--36. Springer-Verlag, 1997.
1425:
1426: \bibitem{cou90}
1427: B.~Courcelle.
1428: \newblock Graph rewriting: An algebraic and logic approach.
1429: \newblock In J.~van Leeuwen, editor, {\em Handbook of Theoretical Computer
1430: Science}, volume~2, pages 194--242. Elsevier Science Publishers, 1990.
1431:
1432: \bibitem{die00}
1433: R.~Diestel.
1434: \newblock {\em Graph Theory}.
1435: \newblock Springer-Verlag, second edition, 2000.
1436:
1437: \bibitem{dowfel99}
1438: R.G. Downey and M.R. Fellows.
1439: \newblock {\em Parameterized Complexity}.
1440: \newblock Springer-Verlag, 1999.
1441:
1442: \bibitem{dowfeltay96}
1443: R.G. Downey, M.R. Fellows, and U.~Taylor.
1444: \newblock The parameterized complexity of relational database queries and an
1445: improved characterization of ${W}[1]$.
1446: \newblock In Bridges, Calude, Gibbons, Reeves, and Witten, editors, {\em
1447: Combinatorics, Complexity, and Logic -- Proceedings of DMTCS '96}, pages
1448: 194--213. Springer-Verlag, 1996.
1449:
1450: \bibitem{epp99}
1451: D.~Eppstein.
1452: \newblock Diameter and treewidth in minor-closed graph families.
1453: \newblock {\em Algorithmica}.
1454: \newblock To appear.
1455:
1456: \bibitem{epp99a}
1457: D.~Eppstein.
1458: \newblock Subgraph isomorphism in planar graphs and related problems.
1459: \newblock {\em Journal of Graph Algorithms and Applications}, 3:1--27, 1999.
1460:
1461: \bibitem{erd59}
1462: P.~Erd\"os.
1463: \newblock Graph theory and probability.
1464: \newblock {\em Canadian Journal of Mathematics}, 11:34--38, 1959.
1465:
1466: \bibitem{flufrigro00}
1467: J.~Flum, M.~Frick, and M.~Grohe.
1468: \newblock Query-evaluation via tree-decompositions.
1469: \newblock Available at
1470: http://sunpool.mathematik.uni-freiburg.de/home/grohe/pub.html, 2000.
1471: \newblock Submitted for publication.
1472:
1473: \bibitem{flugro99}
1474: J.~Flum and M.~Grohe.
1475: \newblock Fixed-parameter tractability and logic.\\
1476: \newblock Available at http://xxx.lanl.gov/abs/cs.CC/9910001, 1999.
1477: \newblock Submitted for publication.
1478:
1479: \bibitem{gai81}
1480: H.~Gaifman.
1481: \newblock On local and non-local properties.
1482: \newblock In {\em Proceedings of the Herbrand Symposium, Logic Colloquium '81}.
1483: North Holland, 1982.
1484:
1485: \bibitem{garjohsto76}
1486: M.R. Garey, D.S. Johnson, and L.~Stockmeyer.
1487: \newblock Some simplified {NP}-complete graph problems.
1488: \newblock {\em Theoretical Computer Science}, 1:237--267, 1976.
1489:
1490: \bibitem{imm82}
1491: N.~Immerman.
1492: \newblock Upper and lower bounds for first-order expressibility.
1493: \newblock {\em Journal of Computer and System Sciences}, 25:76--98, 1982.
1494:
1495: \bibitem{papyan97}
1496: C.H. Papadimitriou and M.~Yannakakis.
1497: \newblock On the complexity of database queries.
1498: \newblock In {\em Proceedings of the 16th ACM Symposium on Principles of
1499: Database Systems}, pages 12--19, 1997.
1500:
1501: \bibitem{pel93}
1502: D.~Peleg.
1503: \newblock Distance-dependent distributed directories.
1504: \newblock {\em Information and Computation}, 103:270--298, 1993.
1505:
1506: \bibitem{ree92}
1507: B.~Reed.
1508: \newblock Finding approximate separators an computing tree-width quickly.
1509: \newblock In {\em Proceedings of the 24th ACM Symposium on Theory of
1510: Computing}, pages 221--228, 1992.
1511:
1512: \bibitem{GMIII}
1513: N.~Robertson and P.D. Seymour.
1514: \newblock Graph minors {I}{I}{I}. {P}lanar tree-width.
1515: \newblock {\em Journal of Combinatorial Theory, Series B}, 36:49--64, 1984.
1516:
1517: \bibitem{GMXIII}
1518: N.~Robertson and P.D. Seymour.
1519: \newblock Graph minors {XIII}. {T}he disjoint paths problem.
1520: \newblock {\em Journal of Combinatorial Theory, Series B}, 63:65--110, 1995.
1521:
1522: \bibitem{see96}
1523: D.~Seese.
1524: \newblock Linear time computable problems and first-order descriptions.
1525: \newblock {\em Mathematical Structures in Computer Science}, 6:505--526, 1996.
1526:
1527: \bibitem{emd90}
1528: P.~van Emde~Boas.
1529: \newblock Machine models and simulations.
1530: \newblock In J.~van Leeuwen, editor, {\em Handbook of Theoretical Computer
1531: Science}, volume~1, pages 1--66. Elsevier Science Publishers, 1990.
1532:
1533: \bibitem{var82}
1534: M.~Y. Vardi.
1535: \newblock The complexity of relational query languages.
1536: \newblock In {\em Proceedings of the 14th ACM Symposium on Theory of
1537: Computing}, pages 137--146, 1982.
1538:
1539: \bibitem{yan95}
1540: M.~Yannakakis.
1541: \newblock Perspectives on database theory.
1542: \newblock In {\em Proceedings of the 36th Annual IEEE Symposium on Foundations
1543: of Computer Science}, pages 224--246, 1995.
1544:
1545: \end{thebibliography}
1546:
1547: \end{document}
1548: