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 formulas of mathematical logic. 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. Logics based on least fixed point operators allow more general predicates over tuples of vertices, but these predicates can only be constructed through fixed-point operators, restricting their power to an intermediate level between first order and monadic second order.
A sentence may be true for some graphs, and false for others; a graph is said to model, written, if is true of the vertices and adjacency relation of. The algorithmic problem of model checking concerns testing whether a given graph models a given sentence. The algorithmic problem of satisfiability concerns testing whether there exists a graph that models a given sentence.
Although both model checking and satisfiability are hard in general, several major algorithmic meta-theorems show that properties expressed in this way can be tested efficiently for important classes of graphs.
Other topics of research in the logic of graphs include investigations of the probability that a random graph has a property specified within a particular type of logic, and methods for data compression based on finding logical formulae that are modeled by a unique graph.

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.

Examples

For instance, the condition that a graph does not have any isolated vertices may be expressed by the sentence
where the symbol indicates the undirected adjacency relation between two vertices. This sentence can be interpreted as meaning that for every vertex there is another vertex that is adjacent to.
The subgraph isomorphism problem for a fixed subgraph H asks whether H appears as a subgraph of a larger graph G. It may be expressed by a sentence that states the existence of vertices such that, for each edge of H, the corresponding pair of vertices are adjacent; see picture. As a special case the clique problem may be expressed by a sentence that states the existence of a number of vertices equal to the clique size all of which are adjacent.

Axioms

For simple undirected graphs, the first order theory of graphs includes the axioms
Other types of graphs, such as directed graphs, may involve different axioms, and logical formulations of multigraph properties require having separate variables for vertices and edges.

Zero-one law

and, independently,
proved a zero–one law for first-order graph logic; Fagin's proof used the compactness theorem. According to this 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, let be a fixed first-order sentence, and choose a random -vertex graph uniformly at random among all graphs on a set of labeled vertices. Then in the limit as tends to infinity the probability that models 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:
For random graphs in which each edge is included independently of the others with a fixed probability, the same result is true, with the same sentences having probabilities tending to zero or to one.
The computational complexity of determining whether a given sentence has probability tending to zero or to one is high: the problem is PSPACE-complete.
If a first order graph property has probability tending to one on random graphs, then it is possible to list all the -vertex graphs that model the property, with polynomial delay per graph.
A similar analysis can be performed for non-uniform random graphs, where the probability of including an edge is a function of the number of vertices, and where the decision to include or exclude an edge is made independently with equal probability for all edges. However, for these graphs the situation is more complicated.
In this case, a first-order property may have one or more thresholds, such that when the edge inclusion probability is bounded away from the threshold then the probability of having the given property tends to zero or one. These thresholds can never be an irrational power of, so random graphs where the edge inclusion probability is an irrational power obey a zero-one law analogous to the one for uniformly random graphs. A similar zero-one law holds for very sparse random graphs that have an edge inclusion probability of with, as long as is not a superparticular ratio. If is superparticular, the probability of having a given property may tend to a limit that is not zero or one, but this limit can be calculated efficiently. There exist first-order sentences that have infinitely many thresholds.

Parameterized complexity

If a first-order sentence includes distinct variables, then the property it describes can be tested in graphs of vertices by examining all -tuples of vertices; however, this brute force search algorithm is not particularly efficient, taking time.
The problem of checking whether a graph models a given first-order sentence includes as special cases the subgraph isomorphism problem and the clique problem.
The clique problem is hard for W, 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 for a function and constant that are independent of and.
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 whose exponent is proportional to.
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. Conversely, if model checking is fixed-parameter tractable for any hereditary family of graphs, that family must be nowhere-dense.

Data compression and graph isomorphism

A first order sentence in the logic of graphs is said to define a graph if is the only graph that models. Every graph may be defined by at least one sentence; for instance, one can define an -vertex graph by a sentence with variables, one for each vertex of the graph, and one more to state the condition that there is no vertex other than the vertices of the graph. Additional clauses of the sentence can be used to ensure that no two vertex variables are equal, that each edge of is present, and no edge exists between a pair of non-adjacent vertices of. However, for some graphs there exist significantly shorter formulas that define the graph.
Several different graph invariants can be defined from the simplest sentences that define a given graph. In particular the logical depth of a graph is defined to be the minimum level of nesting of quantifiers in a sentence defining the graph. The sentence outlined above nests the quantifiers for all of its variables, so it has logical depth. The logical width of a graph is the minimum number of variables in a sentence that defines it. In the sentence outlined above, this number of variables is again. Both the logical depth and logical width can be bounded in terms of the treewidth of the given graph. The logical length, analogously, is defined as the length of the shortest formula describing the graph. The sentence described above has length proportional to the square of the number of vertices, but it is possible to define any graph by a formula with length proportional to its number of edges.
All trees, and most graphs, can be described by first order sentences with only two variables, but extended by counting predicates. For graphs that can be described by sentences in this logic with a fixed constant number of variables, it is possible to find a graph canonization in polynomial time. By comparing canonizations, it is possible to solve the graph isomorphism problem for these graphs in polynomial time.

Satisfiability

It is undecidable whether a given first-order sentence can be realized by a finite undirected graph.
There exist first-order sentences that are modeled by infinite graphs but not by any finite graph. For instance, the property of having exactly one vertex of degree one, with all other vertices having degree exactly two, can be expressed by a first order sentence. It is modeled by an infinite ray, but violates Euler's handshaking lemma for finite graphs. However, it follows from the negative solution to the Entscheidungsproblem that satisfiability of first-order sentences for graphs that are not constrained to be finite remains undecidable. It is also undecidable to distinguish between the first-order sentences that are true for all graphs and the ones that are true of finite graphs but false for some infinite graphs.

Fixed point

based logics of graphs extend the first order logic of graphs by allowing predicates defined by special fixed-point operators, which define a predicate as the fixed point of a formula that relates values of the predicate to other values of the same predicate. For instance, if is a predicate that determines whether two vertices are connected by a path in a given graph, then is the least fixed point of the formula
meaning that the formula becomes a valid implication and that the
pairs of vertices for which it is true are a subset of the pairs of vertices for which any other fixed point of the same formula is true.
In least fixed point logic, the right hand side of the defining formula must use the predicate only positively in order to make the least fixed point well defined.
In an equivalent variant, inflationary fixed point logic, the formula need not be monotone but the resulting fixed point is defined as the one obtained by repeatedly applying implications derived from the defining formula starting from the all-false predicate.
Other variants, allowing negative implications or multiple simultaneously-defined predicates, are also possible, but provide no additional definitional power.
A predicate, defined in one of these ways, can then be applied to a tuple of vertices as part of a larger logical formula.
Fixed point logics, and extensions of these logics that also allow integer counting variables whose values range from 0 to the number of vertices, have been used in descriptive complexity in an attempt to provide a logical description of decision problems in graph theory that can be decided in polynomial time. The fixed point of a logical formula can be constructed in polynomial time, by an algorithm that repeatedly adds tuples to the set of values for which the predicate is true until reaching a fixed point, so deciding whether a graph models a formula in this logic can always be decided in polynomial time. Not every polynomial time graph property can be modeled by a formula in a logic that uses only fixed points and counting. However, for some special classes of graphs the polynomial time properties are the same as the properties expressible in fixed point logic with counting. These include random graphs, interval graphs, and every class of graphs characterized by forbidden minors.

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: MSO1 in which only vertex and vertex set variables are allowed, and MSO2 in which all four types of variables are allowed. The predicates on these variables include equality testing, membership testing, and either vertex-edge incidence or adjacency between pairs of vertices. Additional variations in the definition allow additional predicates such as modular counting predicates.

Examples

As an example, the connectivity of an undirected graph can be expressed in MSO1 as the statement that, for every partition of the vertices into two nonempty subsets, there exists an edge from one subset to the other. A partition of the vertices can be described by the subset S of vertices on one side of the partition, and each such subset should either describe a trivial partition or be crossed by an edge. That is, a graph is connected when it models the MSO1 formula
However, connectivity cannot be expressed in first-order graph logic, nor can it be expressed in existential MSO1 nor even existential MSO2.
Hamiltonicity can be expressed in MSO2 by the existence of a set of edges that forms a connected 2-regular graph on all the vertices, with connectivity expressed as above and 2-regularity expressed as the incidence of two but not three distinct edges at each vertex. However, Hamiltonicity is not expressible in MSO1, because MSO1 is not capable of distinguishing complete bipartite graphs with equal numbers of vertices on each side of the bipartition from unbalanced complete bipartite graphs.
Although not part of the definition of MSO2, orientations of undirected graphs can be represented by a technique involving Trémaux trees. This allows other graph properties involving orientations to be expressed as well.

Courcelle's theorem

According to Courcelle's theorem, every fixed MSO2 property can be tested in linear time on graphs of bounded treewidth, and every fixed MSO1 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

The satisfiability problem for a formula of monadic second-order logic is the problem of determining whether there exists at least one graph for which the formula is true. For arbitrary graph families, and arbitrary formulas, this problem is undecidable. However, satisfiability of MSO2 formulas is decidable for the graphs of bounded treewidth, and satisfiability of MSO1 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, proved that, whenever a family of graphs has a decidable MSO2 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 MSO1 satisfiability problem must have bounded clique-width; this has not been proven, but a weakening of the conjecture that extends MSO1 with modular counting predicates is true.