2021/07/08 by Benedikt Pago, Pago, Benedikt
Computer Science · #Advanced Graph Theory Research #Complexity and Algorithms in Graphs #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2107.03778
openalex publication_date 2021/07/08 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
Choiceless Polynomial Time (CPT) is currently the only candidate logic for\ncapturing PTIME (that is, it is contained in PTIME and has not been separated\nfrom it). A prominent example of a decision problem in PTIME that is not known\nto be CPT-definable is the isomorphism problem on unordered\nCai-F "urer-Immerman graphs (the CFI-query). We study the expressive power of\nCPT with respect to this problem and develop a partial characterisation of\nsolvable instances in terms of properties of symmetric XOR-circuits over the\nCFI-graphs: The CFI-query is CPT-definable on a given class of graphs only if:\nFor each graph G, there exists an XOR-circuit C, whose input gates are\nlabelled with edges of G, such that C is sufficiently symmetric with\nrespect to the automorphisms of G and satisfies certain other circuit\nproperties. We also give a sufficient condition for CFI being solvable in CPT\nand develop a new CPT-algorithm for the CFI-query. It takes as input structures\nwhich contain, along with the CFI-graph, an XOR-circuit with suitable\nproperties. The strongest known CPT-algorithm for this problem can solve\ninstances equipped with a preorder with colour classes of logarithmic size. Our\nresult implicitly extends this to preorders with colour classes of\npolylogarithmic size (plus some unordered additional structure). Finally, our\nwork provides new insights regarding a much more general problem: The existence\nof a solution to an unordered linear equation system A \⋅ x = b over a\nfinite field is CPT-definable if the matrix A has at most logarithmic rank\n(with respect to the size of the structure that encodes the equation system).\nThis is another example that separates CPT from fixed-point logic with\ncounting.\n