Choiceless Polynomial Time (CPT) is one of the few remaining candidate logics for capturing PTIME. In this paper, we make progress towards separating CPT from polynomial time by firstly establishing a connection between the expressive power of CPT and the existence of certain symmetric circuit families, and secondly, proving lower bounds against these circuits. We focus on the isomorphism problem of unordered Cai-F\"urer-Immerman-graphs (the CFI-query) as a potential candidate for separating CPT from P. Results by Dawar, Richerby and Rossman, and subsequently by Pakusa, Schalth\"ofer and Selman show that the CFI-query is CPT-definable on linearly ordered and preordered base graphs with small colour classes. We define a class of CPT-algorithms, that we call "CFI-symmetric algorithms", which generalises all the known ones, and show that such algorithms can only define the CFI-query on a given class of base graphs if there exists a family of symmetric XOR-circuits with certain properties. These properties include that the circuits have the same symmetries as the base graphs, are of polynomial size, and satisfy certain fan-in restrictions. Then we prove that such circuits with slightly strengthened requirements (i.e. stronger symmetry and fan-in and fan-out restrictions) do not exist for the n-dimensional hypercubes as base graphs. This almost separates the CFI-symmetric algorithms from polynomial time - up to the gap that remains between the circuits whose existence we can currently disprove and the circuits whose existence is necessary for the definability of the CFI-query by a CFI-symmetric algorithm.

翻译：无选择多项式时间（CPT）是目前少数几个可能刻画PTIME的逻辑候选之一。本文通过首先建立CPT表达能力与特定对称电路族存在性之间的联系，其次证明这些电路的下界，从而在分离CPT与多项式时间的研究中取得进展。我们聚焦于无序Cai-Fürer-Immerman图（CFI查询）的同构问题，作为分离CPT与P的潜在候选。Dawar、Richerby和Rossman以及后续Pakusa、Schalthöfer和Selman的研究结果表明，CFI查询在具有小颜色类的线性有序和预有序基图上可被CPT定义。我们定义了一类称为“CFI对称算法”的CPT算法，该算法推广了所有已知算法，并证明此类算法仅当存在具有特定性质的对称XOR电路族时，才能在给定的基图类上定义CFI查询。这些性质包括：电路具有与基图相同的对称性、多项式大小，并满足特定的扇入限制。随后我们证明，对于n维超立方体作为基图，不存在满足稍强要求（即更强的对称性以及扇入和扇出限制）的此类电路。这几乎实现了CFI对称算法与多项式时间的分离——仅剩的差距在于我们当前能证否其存在的电路与CFI对称算法定义CFI查询所需存在的电路之间。