Graphs Identified by Logics with Counting

• Published in: ACM transactions on computational logic 2022-01, Vol.23 (1), p.1-31
• Main Authors: Kiefer, Sandra, Schweitzer, Pascal, Selman, Erkal
• Format: Article
• Language: English
• ISSN: 1529-3785; 1557-945X
• DOI: 10.1145/3417515

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 .