In this post, I will discuss Schaefer’s Theorem for Graphs by Bodirsky and Pinsker, which Michael Pinsker presented at STOC 2011. I love the main proof technique of this paper: start with a finite object, blow it up to an infinite object, use techniques from infinitary Ramsey Theory to show that the infinite object must possess regularities, use those regularities to get complexity bounds in P and NP.
The standard version of Schaefer’s Theorem is a statement about the complexity of finding satisfying assignments for a set of Boolean relations. It is a dichotomy theorem: either the set of relations falls under one of six cases, in which case it is solvable in ; or it doesn’t, in which case finding satisfying assignments is -complete. As an “obvious” example, if the set of relations is not always false, but is always true if all its variables are set to TRUE, then finding a solution is (clearly) polynomial-time computable. As a less obvious example, a set of relations that is equivalent to a conjunction of binary clauses can be solved in polynomial time.
In a sense, then, one can consider Schaefer’s Theorem to be a “ramification” of SAT-type phenomena: it explains more precisely when -completeness will arise. The intent of the paper by Bodirsky and Pinsker is to obtain a similar ramification in the setting where relations are defined over the universe of graphs, instead of being arbitrary Boolean relations. Sure enough, they uncover a similar dichotomy — either sets of relations are tractably solvable, or they are -complete.
Without my defining it formally, let’s suppose we have a first-order logic that can express facts about vertices and edges — a language of graphs. Let be a finite set of formulas in this language of graphs. The authors define the following satisfiability problem.
INSTANCE: Given a set of variables W and a formula in the language of graphs of form where each for is obtained from one of the formulas in by substituting the variables from by variables from W,
QUESTION: Is satisfiable?
The main theorem the authors prove is a Shaefer’s Theorem version of Graph-SAT.
Theorem: For all that are finite sets of formulas in the language of graphs, the problem Graph-SAT() is either -complete, or solvable in polynomial time.
These finite sets of formulas can be considered to be constraint satisfaction problems (CSP’s) over graphs, so we can consider this theorem to answer the question, “Given a set of criteria we would like a graph to satisfy, is it feasible to construct a graph that satisfies those criteria, or is it intractably hard (as long as -completeness is intractably hard)?”
Very sketchy proof sketch
To sketch the proof for real, I would have to introduce several definitions from universal algebra, and, well, I’m not gonna. I will limit myself to the following quote from the paper, and a few remarks of my own.
For every set of formulas we present a relational structure such that Graph-SAT() is equivalent [in a certain sense]…. The relational structure has a first-order definition in…the unique countably infinite universal homogeneous graph….This perspective allows us to use the so-called universal-algebraic approach, and in particular polymorphisms to classify the computational complexity of Graph-SAT problems…. Our proof relies crucially on strong results from structural Ramsey theory; we use such results to find regular patterns in the behavior of polymorphisms on the structure of [the universal graph], which in turn allows us to find analogies with structures on Boolean domains.
The algorithm to determine whether a set of graph formulas is satisfiable does the following: it determines which clone (roughly, set of operations in the algebra of the countable universal graph) the set belongs to. There are finitely many clones, and they are all classified in the paper as either polynomial-time solvable or -complete. (See Figure 5 of the paper I linked, or Figure 1 of the STOC version, for a diagram of the clones, and the dividing line between tractable and intractable.)
UPDATE: Alexander Ovsov has translated this blog entry into Romanian and posted it on his own blog.
Manuel Bodirsky, & Michael Pinsker (2011). Schaefer’s Theorem for Graphs Proceedings of 43rd Annual ACM Symposium on the Theory of Computing