Limitations of choiceless computation

Pago, Benedikt Thomas; Grädel, Erich; Dawar, Anuj

doi:10.18154/RWTH-2023-08153

Limitations of choiceless computation

Pago, Benedikt Thomas^RWTH*

2023

Verantwortlichkeitsangabevorgelegt von Benedikt Pago, M.Sc.

ImpressumAachen : RWTH Aachen University 2023

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2023

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor)^RWTH* ; Dawar, Anuj (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2023-07-12

Online
DOI: 10.18154/RWTH-2023-08153
URL: https://publications.rwth-aachen.de/record/964180/files/964180.pdf

Einrichtungen

Projekte

DFG project 405342984 - Logik, Symmetrie und Komplexität (405342984) (405342984)

Inhaltliche Beschreibung (Schlagwörter)
descriptive complexity (frei) ; finite model theory (frei) ; graph isomorphism (frei) ; logic in computer science (frei) ; logics for PTIME (frei) ; proof complexity (frei)

Thematische Einordnung (Klassifikation)
DDC: 510

Kurzfassung
Eines der zentralen Probleme der endlichen Modelltheorie ist die Frage nach der Existenz einer Logik für Polynomialzeit. Eine negative Antwort würde wegen des Satzes von Fagin sofort die Komplexitätsklassen P und NP trennen. Tatsächlich vermutete Yuri Gurevich, der die Frage als erster in der Form formulierte, dass es keine Logik für P gibt. Dies motiviert die Forschung an unteren Schranken für Logiken, die in P enthalten sind. Eine der wenigen solchen Logiken, die bisher nicht von P getrennt werden konnte, ist Choiceless Polynomial Time (CPT), ein symmetrieinvariantes Berechnungsmodell, das 1999 von Blass, Gurevich und Shelah eingeführt wurde. Diese Arbeit ist vor allem dem Ziel gewidmet, die Grenzen der Ausdrucksstärke von CPT besser zu verstehen. Zu diesem Zweck betrachten wir hauptsächlich das Isomorphieproblem auf Cai-Fürer- Immerman (CFI) Graphen. Varianten dieses Problems sind bereits verwendet worden, um Fixpunktlogik mit Zählen und Ranglogik von P zu trennen. Resultate von Dawar, Richerby und Rossman, und darauf aufbauend von Pakusa, Schalthöfer und Selman zeigen, dass folgende Varianten des CFI-Problems in CPT definierbar sind: CFI über linear geordneten Basisgraphen, über prägeordneten Basisgraphen mit logarithmisch großen Farbklassen und Basisgraphen mit linearem Grad. Der allgemeine, ungeordnete Fall ist allerdings noch offen. In Kapitel 7 beweisen wir, dass eine Familie von ungeordneten Basisgraphen (nämlich Hyperwürfel) existiert, die sublinearen Grad haben und keine CPT-definierbaren Präordnungen mit logarithmischen Farbklassen erlauben. Daraus folgt, dass das CFI-Problem auf ungeordneten Hyperwürfeln mit keinem der bisher bekannten CPT-Algorithmen lösbar ist. In Kapitel 8 gehen wir noch einen Schritt weiter, indem wir eine allgemeine Klasse von CPT-Algorithmen für das CFI-Problem definieren, welche auf der Idee von Dawar, Richerby und Rossman (DRR) aufbauen; dies trifft insbesondere auf alle bisher überhaupt bekannten solchen Algorithmen zu. Wir zeigen, dass das CFI-Problem über einer Graphklasse K nur dann von einem DRR- Algorithmus gelöst werden kann, wenn eine Familie von symmetrischen XOR-Schaltkreisen existiert, die die gleichen Symmetrien wie die Graphen in K aufweisen und einige weitere Einschränkungen erfüllen. In Kapitel 9 zeigen wir dann, dass solche Schaltkreisfamilien mit nur geringfügig stärkeren Einschränkungen nicht existieren können, wenn wir für K wieder die Klasse der n-dimensionalen Hyperwürfel wählen. Dieses Resultat beweist also fast, dass kein DRR-Algorithmus das CFI-Problem über ungeordneten Hyperwürfeln lösen kann. In Kapitel 10 betrachten wir schließlich einen völlig anderen Ansatz und beweisen folgende Aussage: Jedes Paar nicht-isomorpher Graphen, das in CPT unterscheidbar ist, ist auch in einer Variante des extended polynomial calculus unterscheidbar. Als Konsequenz lassen sich potentielle zukünftige untere Schranken für die Komplexität des Graphisomorphieproblems in diesem algebraischen Beweiskalkül auf CPT übertragen, was ebenfalls zur Trennung von CPT und P führen könnte.

One of the central open questions in finite model theory asks whether there exists a logic that captures polynomial time. This question is significant for several reasons, one of them being that a negative answer would separate P from NP, by Fagin’s theorem. Yuri Gurevich, who was the first to make this question precise, conjectured that no logic captures polynomial time. This motivates the research on lower bounds against symmetric computation models contained in PTIME. One of the few such formalisms that have not yet been separated from PTIME is the logic Choiceless Polynomial Time (CPT). Establishing strong lower bounds for CPT has been a challenging problem ever since its invention by Blass, Gurevich and Shelah in 1999. This thesis focuses exactly on this goal. Our approach is mainly based on the famous Cai-Fürer-Immerman (CFI) query, which can be seen as an instance of the graph isomorphism problem but also as a linear equation system over the field Z2. Variants of this problem have been used to separate fixed-point logic with counting and rank logic from PTIME. Results by Dawar, Richerby and Rossman, and subsequently by Pakusa, Schalthöfer and Selman show that the CFI-query is definable in CPT in the following cases: over linearly ordered base graphs, preordered base graphs with colour classes of logarithmic size, and unordered base graphs of linear degree. However, the general unordered case remains open. In Chapter 7, we show that there is a family of unordered base graphs (namely, hypercubes) of sublinear degree which does not admit CPT-definable preorders with logarithmic colour classes. Consequently, none of the currently known CPT-algorithms for the CFI-query can be used to solve the unordered case. In Chapter 8, we go a step further: We define a general class of choiceless algorithms for the CFI-query that are based on the Dawar-Richerby-Rossman (DRR) technique; this encompasses all the known algorithms mentioned above. Then we show that the CFI-query on a class K of base graphs is not definable by a DRR-algorithm unless there exists a family of polynomial-size symmetric Boolean XOR-circuits with the same symmetries as the graphs in K and certain restrictions on the connectivity between the gates. In Chapter 9, we also present an almost sufficient lower bound against these circuits: If the connectivity and symmetry restrictions are slightly strengthened, and K is the class of n-dimensional hypercubes, then the required circuit family indeed does not exist. It remains as a problem for future work to lift this non-existence result also to the less restricted circuits – this would show that no DRR-algorithm decides the CFI-query on unordered hypercubes. Finally, in Chapter 10, we propose a different approach towards CPT lower bounds: We show that if CPT can distinguish all pairs of non-isomorphic graphs in a family K, then this is also possible in a propositional proof system called the degree-3 extended polynomial calculus. Thus, potential future lower bounds for solving graph isomorphism in this proof system translate into CPT lower bounds and could also lead to a separation of CPT from PTIME.

OpenAccess:
PDF
(additional files)