The search for a logic capturing PTIME is a long standing open problem in finite model theory. One of the most promising candidate logics for this is Choiceless Polynomial Time with counting (CPT). Abstractly speaking, CPT is an isomorphism-invariant computation model working with hereditarily finite sets as data structures. While it is easy to check that the evaluation of CPT-sentences is possible in polynomial time, the converse has been open for more than 20 years: Can every PTIME-decidable property of finite structures be expressed in CPT? We attempt to make progress towards a negative answer and show that Choiceless Polynomial Time cannot compute a preorder with colour classes of logarithmic size in every hypercube. The reason is that such preorders have super-polynomially many automorphic images, which makes it impossible for CPT to define them. While the computation of such a preorder is not a decision problem that would immediately separate P and CPT, it is significant for the following reason: The so-called Cai-F\"urer-Immerman (CFI) problem is one of the standard benchmarks for logics and maybe best known for separating fixed-point logic with counting (FPC) from P. Hence, it is natural to consider this also a potential candidate for the separation of CPT and P. The strongest known positive result in this regard says that CPT is able to solve CFI if a preorder with logarithmically sized colour classes is present in the input structure. Our result implies that this approach cannot be generalised to unordered inputs. In other words, CFI on unordered hypercubes is a PTIME-problem which provably cannot be tackled with the state-of-the-art choiceless algorithmic techniques.
翻译:捕捉PTIME的逻辑是有限模型理论中长期悬而未决的开放问题。其中最有望成为该逻辑的候选者之一是带计数的无选择多项式时间逻辑(CPT)。抽象而言,CPT是一种同构不变的运算模型,以遗传有限集作为数据结构。虽然很容易验证CPT语句的求值能在多项式时间内完成,但其逆命题在二十余年间始终悬而未决:是否每个有限结构的PTIME可判定性质都能用CPT表达?我们试图向否定答案推进,并证明无选择多项式时间无法在任意超立方体中计算具有对数规模颜色类的预序。其原因在于此类预序具有超多项式数量的自同构像,导致CPT无法定义它们。虽然此类预序的计算并非能立即分离P和CPT的判定问题,但其重要性在于:所谓蔡-菲雷尔-伊默曼(CFI)问题是对数逻辑的标准基准之一,最著名的结果或许是其分离了带计数的不动点逻辑(FPC)与P。因此,自然也将此视为分离CPT与P的潜在候选。这方面已知最强正面结果表明:若输入结构中存在具有对数规模颜色类的预序,则CPT能求解CFI问题。我们的结果意味着这一方法无法推广至无序输入。换言之,无序超立方体上的CFI问题是一个PTIME问题,现有无选择算法技术确凿无法解决它。