Informatik, TU Wien

Schaefer's Theorem for Graphs

Schaefer's theorem is a complexity classification result for Boolean constraint satisfaction problems.

The theory and logic group (institute of computer languages) cordially invites you to the following talk:

Abstract

Schaefer's theorem is a complexity classification result for Boolean constraint satisfaction problems: depending on the allowed set of constraints, a Boolean constraint satisfaction problem is either contained in one out of six classes and can be solved in polynomial time, or is NP-complete.

We present an analog of this result for first-order logic of graphs instead of Boolean logic. In this generalization of Schaefer's result, the input consists of a conjunction of formulas that are obtained from a finite set X of formulas over graphs by variable substitution, and the question is whether there exists a finite graph satisfying all the constraints.

Depending on X, this problem is either contained in one out of 17 classes and can be solved in polynomial time, or is NP-complete. We prove this result by a universal-algebraic approach, which allows us to use structural Ramsey theory. To apply the universal-algebraic approach, we formulate the computational problems under consideration as constraint satisfaction problems (CSPs) whose templates are first-order definable in the countably infinite random graph. Our method to classify the computational complexity of those CSPs produces many statements about the random graph that are of independent mathematical interest.

(Joint work with Michael Pinsker)