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.
翻译:约束满足问题(以关系结构为参数)为表达计算决策问题提供了通用框架。仅关注有限结构类本身已构成一个有趣的微观世界,但要在时态推理中表达决策问题,必须超越有限域范畴。在此背景下,时态结构(即定义在$\mathbb{Q}$上、其关系通过通常的无端点可数稠密线性序一阶可定义的结构)是一类重要的模板。在仅允许对输入变量进行存在量化的标准设定下,有限约束与时态约束的复杂性已被完全分类。而在允许全称量词的量化设定下,目前仅有少量部分分类结果,且存在许多复杂性未知的具体案例。本文在理解时态结构的量化约束满足问题复杂性方面取得了重要进展:我们给出了Ord-Horn片段上量化约束的复杂性二分定理——该片段在理解时态结构与Allen区间代数的约束复杂性中均发挥关键作用。研究表明,所有待研究问题均属于P类或coNP-难问题。特别地,我们确定了$(\mathbb{Q};x=y\Rightarrow x\geq z)$的量化约束满足问题复杂性,从而解决了悬置逾十年的开放问题。