Identifying Tractable Quantified Temporal Constraints within Ord-Horn
Jakub Rydval, Žaneta Semanišinová, Michał Wrona
TL;DR
The paper advances the understanding of quantified temporal constraints by proving a dichotomy for QCSPs over the OH fragment: polynomial-time solvable when the template is GOH or preserved by $oldsymbol{ ext{ππ}}$ (or its dual), and coNP-hard otherwise. It introduces a fixed-point inspired algorithm that reducingly expands instances using short pp-definitions, with a CSP oracle over $(Q;M^+,<)$ driving the tractable cases, and it leverages intricate reductions to show hardness, including PSPACE-hardness when $ ext{D}$ is pp-definable. The results yield a comprehensive classification for OHQCSPs, including resolving the $ ext{QCSP}(Q;M^+)$ question, and offer structural insight that could extend to other temporal fragments. The practical impact lies in a clear, implementable dichotomy and a blueprint for tractability proofs in quantified temporal reasoning.
Abstract
The constraint satisfaction problem, parameterized by a relational structure, provides a general framework for expressing computational decision problems. Already the restriction to the class of all finite structures forms an interesting microcosm on its own, but to express decision problems in temporal reasoning one has to take a step beyond the finite-domain realm. An important class of templates used in this context are temporal structures, i.e., structures over $\mathbb{Q}$ whose relations are first-order definable using the usual countable dense linear order without endpoints. In the standard setting, which allows only existential quantification over input variables, the complexity of finite and temporal constraints has been fully classified. In the quantified setting, i.e., when one also allows universal quantifiers, there is only a handful of partial classification results and many concrete cases of unknown complexity. This paper presents a significant progress towards understanding the complexity of the quantified constraint satisfaction problem for temporal structures. We provide a complexity dichotomy for quantified constraints over the Ord-Horn fragment, which played an important role in understanding the complexity of constraints both over temporal structures and in Allen's interval algebra. We show that all problems under consideration are in P or coNP-hard. In particular, we determine the complexity of the quantified constraint satisfaction problem for $(\mathbb{Q};x=y\Rightarrow x\geq z)$, hereby settling a question open for more than ten years.