Logic of graphs

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.

[1] For instance, the condition that a graph does not have any isolated vertices may be expressed by the sentence

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.

[8] The computational complexity of determining whether a given sentence has probability tending to zero or to one is high: the problem is PSPACE-complete.

A similar zero-one law holds for very sparse random graphs that have an edge inclusion probability of

-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 (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).

[14] On restricted classes of graphs, model checking of first-order sentences can be much more efficient.

Additional clauses of the sentence can be used to ensure that no two vertex variables are equal, that each edge of

[17] 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.

[17] 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 (with the exponent of the polynomial equal to the number of variables).

[19] As a special case of Trakhtenbrot's theorem, it is undecidable whether a given first-order sentence can be realized by a finite undirected graph.

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 (by Alonzo Church and Alan Turing in the 1930s) that satisfiability of first-order sentences for graphs that are not constrained to be finite remains undecidable.

[21] Least fixed point based logics of graphs extend the first-order logic of graphs by allowing predicates (properties of vertices or tuples of vertices) defined by special fixed-point operators.

In another variant with equivalent logical power, 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 sentence.

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 sentence in this logic can always be decided in polynomial time.

Not every polynomial time graph property can be modeled by a sentence in a logic that uses only fixed points and counting.

[29] Although not part of the definition of MSO2, orientations of undirected graphs can be represented by a technique involving Trémaux trees.

[30] 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.

[31] The version of this result for graphs of bounded treewidth can also be implemented in logarithmic space.

[32] Applications of this result include a fixed-parameter tractable algorithm for computing the crossing number of a graph.

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.

[35] This has not been proven, but a weakening of the conjecture that extends MSO1 with modular counting predicates is true.