The field of constraint satisfaction problems (CSPs) studies homomorphism problems between relational structures where the target structure is fixed. Classifying the complexity of these problems has been a central quest of the field, notably when both sides are finite structures. In this paper, we study the generalization where the input is an automatic structure -- potentially infinite, but describable by finite automata. We prove a striking dichotomy: homomorphism problems over automatic structures are either decidable in non-deterministic logarithmic space (NL), or undecidable. We show that structures for which the problem is decidable are exactly those with finite duality, which is a classical property of target structures asserting that the existence of a homomorphism into them can be characterized by the absence of a finite set of obstructions in the source structure. Notably, this property precisely characterizes target structures whose homomorphism problem is definable in first-order logic, which is well-known to be decidable over automatic structures. We also consider a natural variant of the problem. While automatic structures are finitely describable, homomorphisms from them into finite structures need not be. This leads to the notion of regular homomorphism, where the homomorphism itself must be describable by finite automata. Remarkably, we prove that this variant exhibits the same dichotomy, with the same characterization for decidability.
翻译:约束满足问题(CSP)领域研究关系结构间的同态问题,其中目标结构是固定的。对这些问题的复杂性进行分类一直是该领域的核心课题,尤其是在双方均为有限结构的情形下。本文研究其推广形式:输入为自动结构——可能是无限的,但可由有限自动机描述。我们证明了一个显著的二分性:自动结构上的同态问题要么可在非确定性对数空间(NL)内判定,要么是不可判定的。我们证明,问题可判定的结构恰好是具有有限对偶性的结构,这是目标结构的一种经典性质,断言存在到该结构的同态可由源结构中不存在有限障碍集来刻画。值得注意的是,该性质精确刻画了那些同态问题可在一阶逻辑中定义的目标结构,而众所周知,一阶逻辑公式在自动结构上是可判定的。我们还考虑了该问题的一个自然变体。虽然自动结构是有限可描述的,但从其到有限结构的同态本身未必可有限描述。这引出了正则同态的概念,即同态本身必须可由有限自动机描述。值得注意的是,我们证明该变体呈现相同的二分性,且可判定性的刻画条件也完全一致。