  Choiceless Polynomial Time (CPT) is currently the only candidate logic for
capturing PTIME (that is, it is contained in PTIME and has not been separated
from it). A prominent example of a decision problem in PTIME that is not known
to be CPT-definable is the isomorphism problem on unordered
Cai-F\"urer-Immerman graphs (the CFI-query). We study the expressive power of
CPT with respect to this problem and develop a partial characterisation of
solvable instances in terms of properties of symmetric XOR-circuits over the
CFI-graphs: The CFI-query is CPT-definable on a given class of graphs only if:
For each graph $G$, there exists an XOR-circuit $C$, whose input gates are
labelled with edges of $G$, such that $C$ is sufficiently symmetric with
respect to the automorphisms of $G$ and satisfies certain other circuit
properties. We also give a sufficient condition for CFI being solvable in CPT
and develop a new CPT-algorithm for the CFI-query. It takes as input structures
which contain, along with the CFI-graph, an XOR-circuit with suitable
properties. The strongest known CPT-algorithm for this problem can solve
instances equipped with a preorder with colour classes of logarithmic size. Our
result implicitly extends this to preorders with colour classes of
polylogarithmic size (plus some unordered additional structure). Finally, our
work provides new insights regarding a much more general problem: The existence
of a solution to an unordered linear equation system $A \cdot x = b$ over a
finite field is CPT-definable if the matrix $A$ has at most logarithmic rank
(with respect to the size of the structure that encodes the equation system).
This is another example that separates CPT from fixed-point logic with
counting.

Logic in Computer Science;Computational Complexity