Tractable Combinations of Temporal CSPs

2020 
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 $\mathrm{CSP}(T_1 \cup T_2)$ where $T_1$ and $T_2$ are theories with disjoint finite relational signatures. We prove that if $T_1$ and $T_2$ are the theories of temporal structures, i.e., structures where all relations have a first-order definition in $(\mathbb{Q},<)$, then $\mathrm{CSP}(T_1 \cup T_2)$ is in P or NP-complete. To this end we prove a new algebraic dichotomy about the lattice of locally closed clones over the domain ${\mathbb{Q}}$ that contain $\mathrm{Aut}(\mathbb{Q};<)$.
    • Correction
    • Source
    • Cite
    • Save
    • Machine Reading By IdeaReader
    38
    References
    0
    Citations
    NaN
    KQI
    []