We classify graphs and, more generally, finite relational structures that are identified by C^2 , that is, two-variable first-order logic with counting. Using this classification, we show that it can be decided in almost linear time whether a structure is identified by C^2 . Our classification implies that for every graph identified by this logic, all vertex-colored versions of it are also identified. A similar statement is true for finite relational structures. We provide constructions that solve the inversion problem for finite relational structures in linear time. By a result due to Otto, this problem has been known to be polynomial-time solvable. For graphs, we conclude that every C^2 -equivalence class contains a representative whose orbits are exactly the classes of the C^2 -partition of its vertex set and which has a single automorphism witnessing this fact. We show that such statements are not true for general k by providing examples of graphs of order linear in k which are identified by C^3 , but for which the orbit partition is strictly finer than the C^k -partition. We also construct identified graphs which have vertex-colored versions that are not identified by C^k .

Choiceless Polynomial Time (CPT) is one of the most promising candidates in the search for a logic capturing P time . The question whether there is a logic that expresses exactly the polynomial-time computable properties of finite structures, which has been open for more than 30 years, is one of the most important and challenging problems in finite model theory. The strength of Choiceless Polynomial Time is its ability to perform isomorphism-invariant computations over structures, using hereditarily finite sets as data structures. But, because of isomorphism-invariance, it is choiceless in the sense that it cannot select an arbitrary element of a set—an operation that is crucial for many classical algorithms. CPT can define many interesting P time queries, including (a certain version of) the Cai-Fürer-Immerman (CFI) query. The CFI-query is particularly interesting, because it separates fixed-point logic with counting from P time and has since remained the main benchmark for the expressibility of logics within P time . The CFI-construction associates with each connected graph a set of CFI-graphs that can be partitioned into exactly two isomorphism classes called odd and even CFI-graphs. The problem is to decide, given a CFI-graph, whether it is odd or even. For the case where the CFI-graphs arise from ordered graphs, Dawar, Richerby, and Rossman proved that the CFI-query is CPT-definable. However, definability of the CFI-query over general graphs remains open. Our first contribution generalises the result by Dawar, Richerby, and Rossman to the variant of the CFI-query derived from graphs with colour classes of logarithmic size, instead of colour class size one. Second, we consider the CFI-query over graph classes where the maximal degree is linear in the size of the graphs. For the latter, we establish CPT-definability using only sets of small, constant rank, which is known to be impossible for the general case. In our CFI-recognising procedures we strongly make use of the ability of CPT to create sets, rather than tuples only, and we further prove that, if CPT worked over tuples instead, then no such procedure would be definable. We introduce a notion of “sequencelike objects” based on the structure of the graphs’ symmetry groups, and we show that no CPT-program that only uses sequencelike objects can decide the CFI-query over complete graphs, which have linear maximal degree. From a broader perspective, this generalises a result by Blass, Gurevich, and van den Bussche about the power of isomorphism-invariant machine models (for polynomial time) to a setting with counting.

Choiceless Polynomial Time (CPT) is one of the most promising candidates in the search for a logic capturing Ptime. The question whether there is a logic that expresses exactly the polynomial-time computable properties of finite structures, which has been open for more than 30 years, is one of the most important and challenging problems in finite model theory. The strength of Choiceless Polynomial Time is its ability to perform isomorphism-invariant computations over structures, using hereditarily finite sets as data structures. But, as it preserves symmetries, it is choiceless in the sense that it cannot select an arbitrary element of a set - an operation which is crucial for many classical algorithms. CPT can define many interesting Ptime queries, including (the original version of) the Cai-Fürer-Immerman (CFI) query. The CFI query is particularly interesting because it separates fixed-point logic with counting from Ptime, and has since remained the main benchmark for the expressibility of logics within Ptime. The CFI construction associates with each connected graph a set of CFI-graphs that can be partitioned into exactly two isomorphism classes called odd and even CFI-graphs. The problem is to decide, given a CFI-graph, whether it is odd or even. In the original version, the underlying graphs are linearly ordered, and for this case, Dawar, Richerby and Rossman proved that the CFI query is CPT-definable. However, the CFI query over general graphs remains one of the few known examples for which CPT-definability is open. Our first contribution generalises the result by Dawar, Richerby and Rossman to the variant of the CFI query where the underlying graphs have colour classes of logarithmic size, instead of colour class size one. Secondly, we consider the CFI query over graph classes where the maximal degree is linear in the size of the graphs. For these classes, we establish CPT-definability using only sets of small, constant rank, which is known to be impossible for the general case. In our CFI-recognising procedures we strongly make use of the ability of CPT to create sets, rather than tuples only, and we further prove that, if CPT worked over tuples instead, no such procedure would be definable. We introduce a notion of "sequence-like objects" based on the structure of the graphs' symmetry groups, and we show that no CPT-program which only uses sequence-like objects can decide the CFI query over complete graphs, which have linear maximal degree. From a broader perspective, this generalises a result by Blass, Gurevich, and van den Bussche about the power of isomorphism-invariant machine models (for polynomial time) to a setting with counting.