Authors: Manuel Bodirsky ; Johannes Greiner ; Jakub Rydval
0000-0001-8228-3611##NULL##NULL
Manuel Bodirsky;Johannes Greiner;Jakub Rydval
The constraint satisfaction problem (CSP) of a first-order theory T is the
computational problem of deciding whether a given conjunction of atomic
formulas is satisfiable in some model of T. We study the computational
complexity of CSP(T1∪T2) where T1 and T2 are theories with
disjoint finite relational signatures. We prove that if T1 and T2 are the
theories of temporal structures, i.e., structures where all relations have a
first-order definition in (Q;<), then CSP(T1∪T2) is in P or
NP-complete. To this end we prove a purely algebraic statement about the
structure of the lattice of locally closed clones over the domain Q that
contain Aut(Q;<).