Temporal Constraint Satisfaction Problems in Fixed-Point Logic

Proceedings - Symposium on Logic in Computer Science, pp. 237–251

Abstract

Finite-domain constraint satisfaction problems are either solvable by Datalog, or not even expressible in fixed-point logic with counting. The border between the two regimes can be described by a strong height-one Maltsev condition. For infinite-domain CSPs, the situation is more complicated even if the template structure of the CSP is model-theoretically tame. We prove that there is no Maltsev condition that characterizes Datalog already for the CSPs of first-order reducts of (Q; <); such CSPs are called temporal CSPs and are of fundamental importance in infinite-domain constraint satisfaction. Our main result is a complete classification of temporal CSPs that can be expressed in one of the following logical formalisms: Datalog, fixed-point logic (with or without counting), or fixed-point logic with the Boolean rank operator. The classification shows that many of the equivalent conditions in the finite fail to capture expressibility in Datalog or fixed-point logic already for temporal CSPs.

Authors 3

1. Manuel Bodirsky

   Technische Universität Dresden

   Affiliation as printed

   TU Dresden

   TU, Dresden,

2. Wied Pakusa Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

   Rwth Aachen

3. Jakub Rydval

   Technische Universität Dresden

   Affiliation as printed

   TU Dresden

   TU, Dresden,