With Jan Kára. Journal of the ACM, 57(2). An extended abstract appeared in the proceedings of STOC'08.
A temporal constraint language is a set of relations that has a first-order definition in (Q,<), the dense linear order of the rational numbers. We present a complete complexity classification of the constraint satisfaction problem (CSP) for temporal constraint languages: if the constraint language is contained in one out of nine temporal constraint languages, then the CSP can be solved in polynomial time; otherwise, the CSP is NP-complete. Our proof combines model-theoretic concepts with techniques from universal algebra, and also applies the so-called product Ramsey theorem, which we believe will be useful in similar contexts of constraint satisfaction complexity classification.
Conference version and complete version.
Jan Kára and I started this project at the end of Jan's stay at Humboldt-University as a Marie-Curie fellow in 2005. We were working on this project ever since, more or less intensively, with occasional meetings (I was once in Prague, he was twice in Berlin), and over one thousend emails in each direction. Along the way, we first found a classification result for the fundamental class of equality constraint languages, which we published first.
I like the result because it gives an elegant unifying explanation of tractability and hardness of temporal constraint satisfaction problems. But more importantly, I believe that the proof structure will be prototypical for other classification results about infinite-domain constraint satisfaction problems. It uses polymorphisms and the algebraic approach to constraint satisfaction complexity, which is currently a major research focus in universal algebra, finite model theory, and graph homomorphism combinatorics (also see the other constraint satisfaction paper at STOC'08). To generalize the algebraic approach to infinite domain constraint satisfaction problems we need a couple of model-theoretic concepts and results. We then show how to use the product Ramsey theorem in such universal-algebraic classification proofs (we apply it to show that the polymorphisms of temporal constraint languages must behave in a `regular' way on large subsets of the domain; another application of this principle can be found in this paper).
The algorithmic contributions of the paper are intersting as well. To show the tractability of the constraint languages in the nine classes mentioned in the abstract, we introduce essentially 4 new algorithms (one of which is presented separately). There is a vague analogy to the four polynomial-time algorithms in boolean constraint satisfaction (the ones for affine, horn, dual-horn, and bijunctive clauses in the input), but the analogy is delusive. The tractable constraint languages in our classification result can definitely not be solved by local consistency techniques (this is formalized and shown in this paper, too), which is the standard algorithmic tool that dominates the literature about constraint satisfaction in Artificial Intelligence.
Even though the entire proof is quite long, we hope that the most important insights are sampled into the conference version of the paper. For more about constraint satisfaction with infinite domains, see my survey Constraint Satisfaction Problems with Infinite Templates.