Logic of graphs

In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using logical formulas. There are several variations in the types of logical operation that can be used in these formulas. The first order logic of graphs concerns formulas in which the variables and predicates concern individual vertices and edges of a graph, while monadic second order graph logic allows quantification over sets of vertices or edges. Several major algorithmic meta-theorems show that properties expressed in this way can be tested efficiently for several important classes of graphs.

First order

In the first-order logic of graphs, a graph property is expressed as a quantified logical formula whose variables represent graph vertices, with predicates for equality and adjacency testing. For instance, the condition that a graph does not have any isolated vertices may be expressed by the sentence

$\forall u:\exists v:u\sim v$

where the $\sim$ symbol indicates the adjacency relation between two vertices. This sentence $S$ is true for some graphs, and false for others; a graph $G$ is said to model $S$, written $G\models S$, if $S$ is true of the vertices and adjacency relation of $G$.

Zero-one law

Main article: Rado graph § Model theory and 0-1 laws

Fagin (1976) proved a zero–one law for first-order graph logic using the compactness theorem. According to Fagin's result, every first-order sentence is either almost always true or almost always false for random graphs in the Erdős–Rényi model. That is, if one chooses a fixed sentence S, and computes the probability that a random n-vertex graph (choosen uniformly at random among all graphs on a set of n labeled vertices) models S, then in the limit as n tends to infinity this probability will tend either to zero or to one. Moreover, there is a specific infinite graph, the Rado graph, such that the sentences modeled by the Rado graph are exactly the ones for which the probability of being modeled by a random finite graph tends to one. However, the computational complexity of determining whether the Rado graph models a given sentence is high: the problem is PSPACE-complete.

Parameterized complexity

Main article: Clique problem § Fixed-parameter intractability

If a first-order sentence includes k distinct variables, then the property it describes can be tested in graphs of n vertices by examining all k-tuples of vertices; however, this brute force search algorithm is not particularly efficient, taking time O(n^k). The problem of checking whether a graph models a given first-order sentence includes as special cases the subgraph isomorphism problem (in which the sentence describes the graphs that contain a fixed subgraph) and the clique problem (in which the sentence describes graphs that contain complete subgraphs of a fixed size). The clique problem is hard for W(1), the first level of a hierarchy of hard problems from the point of view of parameterized complexity. Therefore, it is unlikely to have a fixed-parameter tractable algorithm, one whose running time takes the form O(f(k) n^c) for a function f and constant c that are independent of k and c. More strongly, if the exponential time hypothesis is true, then clique-finding and first-order model checking would necessarily take time proportional to a power of n whose exponent is proportional to k.

Sparse graphs

Main article: Bounded expansion § Algorithmic applications

On restricted classes of graphs, model checking of first-order sentences can be much more efficient. In particular, every graph property expressible as a first-order sentence can be tested in linear time for the graphs of bounded expansion. These are the graphs in which all shallow minors are sparse graphs, with a ratio of edges to vertices bounded by a function of the depth of the minor. Even more generally, first-order model checking can be performed in near-linear time for nowhere-dense graphs, classes of graphs for which, at each possible depth, there is at least one forbidden shallow minor.

Second order

In the monadic second-order logic of graphs, the variables represent objects of up to four types: vertices, edges, sets of vertices, and sets of edges. There are two main variations of monadic second-order graph logic: MSO₁ in which only vertex and vertex set variables are allowed, and MSO₂ in which all four types of variables are allowed The predicates on these variables include equality testing, membership testing, and either vertex-edge incidence (if both vertex and edge variables are allowed) or adjacency between pairs of vertices (if only vertex variables are allowed). Additional variations in the definition allow additional predicates such as modular counting predicates.

Courcelle's theorem

Main article: Courcelle's theorem

According to Courcelle's theorem, every fixed MSO₂ property can be tested in linear time on graphs of bounded treewidth, and every fixed MSO₁ property can be tested in linear time on graphs of bounded clique-width. The version of this result for graphs of bounded treewidth can also be implemented in logarithmic space. Applications of this result include a fixed-parameter tractable algorithm for computing the crossing number of a graph.

Seese's theorem

Main article: Courcelle's theorem § Seese's theorem

The satisfiability problem for a formula of monadic second-order logic is the problem of determining whether there exists at least one graph (possibly within a restricted family of graphs) for which the formula is true. For arbitrary graph families, and arbitrary formulas, this problem is undecidable. However, satisfiability of MSO₂ formulas is decidable for the graphs of bounded treewidth, and satisfiability of MSO₁ formulas is decidable for graphs of bounded clique-width. The proof involves using Courcelle's theorem to build an automaton that can test the property, and then examining the automaton to determine whether there is any graph it can accept.

As a partial converse, Seese (1991) proved that, whenever a family of graphs has a decidable MSO₂ satisfiability problem, the family must have bounded treewidth. The proof is based on a theorem of Robertson and Seymour that the families of graphs with unbounded treewidth have arbitrarily large grid minors. Seese also conjectured that every family of graphs with a decidable MSO₁ satisfiability problem must have bounded clique-width; this has not been proven, but a weakening of the conjecture that extends MSO₁ with modular counting predicates is true.

References

• Chen, Jianer; Huang, Xiuzhen; Kanj, Iyad A.; Xia, Ge (2006), "Strong computational lower bounds via parameterized complexity", J. Comput. Syst. Sci., 72 (8): 1346–1367, doi:10.1016/j.jcss.2006.04.007
• Courcelle, Bruno; Engelfriet, Joost (2012), Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, Encyclopedia of Mathematics and its Applications, vol. 138, Cambridge University Press, ISBN 9781139644006, Zbl 1257.68006.
• Courcelle, Bruno; Oum, Sang-il (2007), "Vertex-minors, monadic second-order logic, and a conjecture by Seese" (PDF), Journal of Combinatorial Theory, Series B, 97 (1): 91–126, doi:10.1016/j.jctb.2006.04.003, MR 2278126.
• Downey, R. G.; Fellows, M. R. (1995), "Fixed-parameter tractability and completeness. II. On completeness for W[1]", Theoretical Computer Science, 141 (1–2): 109–131, doi:10.1016/0304-3975(94)00097-3.
• Dvořák, Zdeněk; Kráľ, Daniel; Thomas, Robin (2010), "Deciding first-order properties for sparse graphs", Proc. 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2010), IEEE Computer Soc., Los Alamitos, CA, pp. 133–142, MR 3024787.
• Elberfeld, Michael; Jakoby, Andreas; Tantau, Till (October 2010), "Logspace Versions of the Theorems of Bodlaender and Courcelle" (PDF), Proc. 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2010), pp. 143–152, doi:10.1109/FOCS.2010.21.
• Fagin, Ronald (1976), "Probabilities on finite models" (PDF), The Journal of Symbolic Logic, 41 (1): 50–58, doi:10.1017/s0022481200051756, MR 0476480.
• Grandjean, Étienne (1983), "Complexity of the first-order theory of almost all finite structures", Information and Control, 57 (2–3): 180–204, doi:10.1016/S0019-9958(83)80043-6, MR 0742707.
• Grohe, Martin (2001), "Computing crossing numbers in quadratic time", Proceedings of the Thirty-third Annual ACM Symposium on Theory of Computing (STOC '01), pp. 231–236, doi:10.1145/380752.380805.
• Kawarabayashi, Ken-ichi; Reed, Buce (2007), "Computing crossing number in linear time", Proceedings of the Thirty-ninth Annual ACM Symposium on Theory of Computing (STOC '07), pp. 382–390, doi:10.1145/1250790.1250848.
• Nešetřil, Jaroslav; Ossona de Mendez, Patrice (2012), Sparsity: Graphs, Structures, and Algorithms, Algorithms and Combinatorics, vol. 28, Springer, doi:10.1007/978-3-642-27875-4, ISBN 978-3-642-27874-7, MR 2920058.
• Seese, D. (1991), "The structure of the models of decidable monadic theories of graphs", Annals of Pure and Applied Logic, 53 (2): 169–195, doi:10.1016/0168-0072(91)90054-P, MR 1114848.