无选择多项式时间、对称电路与 Cai-F"urer-Immerman 图

无选择多项式时间(CPT)目前是唯一用于捕获 PTIME 的候选逻辑(即它包含于 PTIME 且尚未被证明与之分离)。一个已知的属于 PTIME 但不知是否为 CPT 可定义的决策问题的突出例子是无序 Cai-F"urer-Immerman 图上的同构问题(CFI-查询)。我们针对此问题研究 CPT 的表达能力，并基于 CFI-图上的对称 XOR-电路的性质给出可解实例的部分刻画：CFI-查询在给定图类上是 CPT 可定义的，仅当：对每个图 $G$，存在一个 XOR-电路 $C$，其输入门用 $G$ 的边标记，使得 $C$ 关于 $G$ 的自同构充分对称并满足某些其他电路性质。我们也给出 CFI 在 CPT 中可解的一个充分条件，并开发了一个用于 CFI-查询的新 CPT 算法。它以包含 CFI-图及具有合适性质的 XOR-电路的结构为输入。对此问题已知最强的 CPT 算法能求解配备了对数大小色类的预序的实例。我们的结果隐式地将此扩展到具有多对数大小色类(加上某些无序附加结构)的预序。最后，我们的工作为更广泛的问题提供了新见解：有限域上无序线性方程组 $A \cdot x = b$ 的解的存在性是 CPT 可定义的，如果矩阵 $A$ 的秩至多为对数秩(相对于编码该方程系统的结构的大小)。这是将 CPT 与带计数的不动点逻辑区分开的又一个例子。