Pakusa, Wied ;
Schalthöfer, Svenja ;
Selman, Erkal
Definability of CaiFürerImmerman Problems in Choiceless Polynomial Time
Abstract
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 polynomialtime 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 isomorphisminvariant 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 CaiFürerImmerman (CFI) query.
The CFI query is particularly interesting because it separates fixedpoint 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 CFIgraphs that can be partitioned into exactly two isomorphism classes called odd and even CFIgraphs. The problem is to decide, given a CFIgraph, 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 CPTdefinable. However, the CFI query over general graphs remains one of the few known examples for which CPTdefinability 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 CPTdefinability using only sets of small, constant rank, which is known to be impossible for the general case.
In our CFIrecognising 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 "sequencelike objects" based on the structure of the graphs' symmetry groups, and we show that no CPTprogram which 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 isomorphisminvariant machine models (for polynomial time) to a setting with counting.
BibTeX  Entry
@InProceedings{pakusa_et_al:LIPIcs:2016:6559,
author = {Wied Pakusa and Svenja Schalth{\"o}fer and Erkal Selman},
title = {{Definability of CaiF{\"u}rerImmerman Problems in Choiceless Polynomial Time}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {19:119:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770224},
ISSN = {18688969},
year = {2016},
volume = {62},
editor = {JeanMarc Talbot and Laurent Regnier},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6559},
URN = {urn:nbn:de:0030drops65595},
doi = {10.4230/LIPIcs.CSL.2016.19},
annote = {Keywords: finite model theory, descriptive complexity, logic for textsc{Ptime}, Choiceless Polynomial Time, CaiF{\"u}rerImmerman}
}
29.08.2016
Keywords: 

finite model theory, descriptive complexity, logic for textsc{Ptime}, Choiceless Polynomial Time, CaiFürerImmerman 
Seminar: 

25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Issue date: 

2016 
Date of publication: 

29.08.2016 