Definability of Cai-Fürer-Immerman Problems in Choiceless Polynomial Time

Authors Wied Pakusa, Svenja Schalthöfer, Erkal Selman

Thumbnail PDF


  • Filesize: 0.52 MB
  • 17 pages

Document Identifiers

Author Details

Wied Pakusa
Svenja Schalthöfer
Erkal Selman

Cite AsGet BibTex

Wied Pakusa, Svenja Schalthöfer, and Erkal Selman. Definability of Cai-Fürer-Immerman Problems in Choiceless Polynomial Time. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


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.
  • finite model theory
  • descriptive complexity
  • logic for textsc{Ptime}
  • Choiceless Polynomial Time
  • Cai-Fürer-Immerman


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. F. Abu Zaid, E. Grädel, M. Grohe, and W. Pakusa. Choiceless Polynomial Time on structures with small Abelian colour classes. In MFCS 2014, volume 8634 of LNCS, pages 50-62. Springer, 2014. Google Scholar
  2. A. Blass. Why sets? In Pillars of Computer Science, volume 4800 of LNCS, pages 179-198. Springer, 2008. URL:
  3. A. Blass, Y. Gurevich, and S. Shelah. Choiceless polynomial time. Annals of Pure and Applied Logic, 100(1):141-187, 1999. Google Scholar
  4. A. Blass, Y. Gurevich, and S. Shelah. On polynomial time computation over unordered structures. J. Symb. Logic, 67(3):1093-1125, 2002. Google Scholar
  5. Andreas Blass, Yuri Gurevich, and Jan Van den Bussche. Abstract state machines and computationally complete query languages. In International Workshop on Abstract State Machines, pages 22-33. Springer, 2000. Google Scholar
  6. J. Cai, M. Fürer, and N. Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12(4):389-410, 1992. Google Scholar
  7. A. Chandra and D. Harel. Structure and complexity for relational queries. Journal of Computer and System Sciences, 25:99-128, 1982. Google Scholar
  8. A. Dawar. The nature and power of fixed-point logic with counting. ACM SIGLOG News, pages 8-21, 2015. Google Scholar
  9. A. Dawar, M. Grohe, B. Holm, and B. Laubner. Logics with rank operators. In LICS 2009, pages 113-122, 2009. Google Scholar
  10. A. Dawar, D. Richerby, and B. Rossman. Choiceless polynomial time, counting and the Cai-Fürer-Immerman graphs. Ann. Pure Appl. Logic, 152(1), 2008. Google Scholar
  11. E. Grädel and M. Grohe. Is Polynomial Time Choiceless? In Fields of Logic and Computation II., volume 9300 of LNCS, pages 193-209. Springer, 2015. Google Scholar
  12. E. Grädel, Ł. Kaiser, W. Pakusa, and S. Schalthöfer. Characterising Choiceless Polynomial Time with First-Order Interpretations. In LICS, 2015. Google Scholar
  13. E. Grädel and W. Pakusa. Rank logic is dead, long live rank logic! CoRR (a conference version appeared in the proceedings of CSL'15), abs/1503.05423, 2015. Google Scholar
  14. M. Grohe. The quest for a logic capturing PTIME. In Logic in Computer Science, 2008, (LICS'08), pages 267-271. IEEE, 2008. Google Scholar
  15. Y. Gurevich. Logic and the challenge of computer science. In Current Trends in Theoretical Computer Science. Computer Science Press, 1988. Google Scholar
  16. N. Immerman. Relational queries computable in polynomial time. Inf. and Control, 68:86-104, 1986. Google Scholar
  17. B. Laubner. The Structure of Graphs and New Logics for the Characterization of Polynomial Time. PhD thesis, HU Berlin, 2011. Google Scholar
  18. B. Rossman. Choiceless computation and symmetry. In Fields of Logic and Computation, LNCS, pages 565-580. Springer, 2010. Google Scholar
  19. M. Y. Vardi. The complexity of relational query languages. In STOC'82, pages 137-146. ACM Press, 1982. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail