Twin-width is a graph parameter introduced in the context of first-order model checking, and has since become a central parameter in algorithmic graph theory. While many algorithmic problems become easier on arbitrary classes of bounded twin-width, graph isomorphism on graphs of twin-width 4 and above is as hard as the general isomorphism problem. For each positive integer k, the k-dimensional Weisfeiler-Leman algorithm is an iterative color refinement algorithm that encodes structural similarities and serves as a fundamental tool for distinguishing non-isomorphic graphs. We show that the graph isomorphism problem for graphs of twin-width 1 can be solved by the 3-dimensional Weisfeiler-Leman algorithm, while there is no fixed k such that the k-dimensional Weisfeiler-Leman algorithm solves the graph isomorphism problem for graphs of twin-width 4. Moreover, we prove the conjecture of Bergougnoux, Gajarský, Guspiel, Hlinený, Pokrývka, and Sokolowski (ISAAC 2023) that stable graphs of twin-width 2 have bounded rank-width. This implies that isomorphism of these graphs is solved by a fixed dimension of the Weisfeiler-Leman algorithm.

The Weisfeiler-Leman dimension of a graph \( G \) is the least number \( k \) such that the \( k \) -dimensional Weisfeiler-Leman algorithm distinguishes \( G \) from every other non-isomorphic graph, or equivalently, the least \( k \) such that \( G \) is definable in \((k+1)\) -variable logic with counting. The dimension is a standard measure of the descriptive or structural complexity of a graph and recently finds various applications in particular in the context of machine learning. This article studies the complexity of computing the Weisfeiler-Leman dimension. We observe that deciding whether the Weisfeiler-Leman dimension of \( G \) is at most \( k \) is NP -hard, even if \( G \) is restricted to have 4-bounded color classes. Therefore, we study parameterized versions of the problem. For each fixed \(k\geq 2\) , we give a polynomial-time algorithm that decides whether the Weisfeiler-Leman dimension of a given graph with 5-bounded color classes is at most \( k \) . Moreover, we show that for these bounds on the color classes, this is optimal because the problem is P -hard under logspace-uniform AC 0 -reductions. Furthermore, for each larger bound \( c \) on the color classes and each fixed \(k\geq 2\) , we provide a polynomial-time decision algorithm for the abelian case, that is, for structures of which each color class has an abelian automorphism group. While the graph classes we consider may seem quite restrictive, graphs with 4-bounded abelian colors include CFI-graphs and multipedes, which form the basis of almost all known hard instances and lower bounds related to the Weisfeiler-Leman algorithm.

The Weisfeiler-Leman dimension of a graph $G$ is the least number $k$ such that the $k$-dimensional Weisfeiler-Leman algorithm distinguishes $G$ from every other non-isomorphic graph. The dimension is a standard measure of the descriptive complexity of a graph and recently finds various applications in particular in the context of machine learning. In this paper, we study the computational complexity of computing the Weisfeiler-Leman dimension. We observe that in general the problem of deciding whether the Weisfeiler-Leman dimension of $G$ is at most $k$ is NP-hard. This is also true for the more restricted problem with graphs of color multiplicity at most 4. Therefore, we study parameterized versions of the problem. We give, for each fixed $k\geq 2$, a polynomial-time algorithm that decides whether the Weisfeiler-Leman dimension of a given graph of color multiplicity at most $5$ is at most $k$. Moreover, we show that for these color multiplicities this is optimal in the sense that this problem is P-hard under logspace-uniform $\text{AC}_0$-reductions. Furthermore, for each larger bound $c$ on the color classes and each fixed $k\geq 2$, we provide a polynomial-time decision algorithm for the abelian case, that is, for structures of which each color class has an abelian automorphism group. While the graph classes we consider may seem quite restrictive, graphs with $4$-bounded abelian colors include CFI-graphs and multipedes, which form the basis of almost all known hard instances and lower bounds related to the Weisfeiler-Leman algorithm.

We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Torán and Wörz [Jacobo Torán and Florian Wörz, 2023] showed that there is a resolution refutation of narrow width k for two graphs if and only if they can be distinguished in (k+1)-variable first-order logic (FO^{k+1}). While DAG-like narrow width k resolution refutations have size at most n^k, tree-like refutations may be much larger. We show that there are graphs of order n, whose isomorphism can be refuted in narrow width k but only in tree-like size 2^{Ω(n^{k/2})}. This is a supercritical trade-off where bounding one parameter (the narrow width) causes the other parameter (the size) to grow above its worst case. The size lower bound is super-exponential in the formula size and improves a related supercritical trade-off by Razborov [Alexander A. Razborov, 2016]. To prove our result, we develop a new variant of the k-pebble EF-game for FO^k to reason about tree-like refutation size in a similar way as the Prover-Delayer games in proof complexity. We analyze this game on the compressed CFI graphs introduced by Grohe, Lichter, Neuen, and Schweitzer [Martin Grohe et al., 2023]. Using a recent improved robust compressed CFI construction of de Rezende, Fleming, Janett, Nordström, and Pang [Susanna F. de Rezende et al., 2024], we obtain a similar bound for width k (instead of the stronger but less common narrow width) and make the result more robust.

The k -dimensional Weisfeiler-Leman ( k -WL) algorithm is a simple combinatorial algorithm that was originally designed as a graph isomorphism heuristic. It naturally finds applications in Babai’s quasipolynomial-time isomorphism algorithm, practical isomorphism solvers, and algebraic graph theory. However, it also has surprising connections to other areas such as logic, proof complexity, combinatorial optimization, and machine learning. The algorithm iteratively computes a coloring of the k -tuples of vertices of a graph. Since Fürer’s linear lower bound [ICALP 2001], it has been an open question whether there is a super-linear lower bound for the iteration number for k -WL on graphs. We answer this question affirmatively, establishing an Ω ( n k /2 )-lower bound for all k .

We prove new upper and lower bounds on the number of iterations the \(k\) -dimensional Weisfeiler-Leman algorithm ( \(k\) -WL) requires until stabilization. For \(k\geq 3\) , we show that \(k\) -WL stabilizes after at most \(O(kn^{k-1}\log n)\) iterations (where \(n\) denotes the number of vertices of the input structures), obtaining the first improvement over the trivial upper bound of \(n^{k}-1\) and extending a previous upper bound of \(O(n\log n)\) for \(k=2\) . We complement our upper bounds by constructing \(k\) -ary relational structures on which \(k\) -WL requires at least \(n^{\Omega(k)}\) iterations to stabilize. This improves over a previous lower bound of \(n^{\Omega(k/\log k)}\) . We also investigate tradeoffs between the dimension and the iteration number of WL, and show that \(d\) -WL, where \(d=\lceil\frac{3(k + 1)}{2}\rceil\) , can simulate the \(k\) -WL algorithm using only \(O(k^{2}\cdot n^{\lfloor k/2\rfloor+1}\log n)\) many iterations, but still requires at least \(n^{\Omega(k)}\) iterations for any \(d\) (that is sufficiently smaller than \(n\) ). The number of iterations required by \(k\) -WL to distinguish two structures corresponds to the quantifier rank of a sentence distinguishing them in the \((k + 1)\) -variable fragment \(\mathsf{C}_{k + 1}\) of first-order logic with counting quantifiers. Hence, our results also imply new upper and lower bounds on the quantifier rank required in the logic \(\mathsf{C}_{k + 1}\) , as well as tradeoffs between variable number and quantifier rank.

Abramsky, Dawar, and Wang (2017) introduced the pebbling comonad for k-variable counting logic and thereby initiated a line of work that imports category theoretic machinery to finite model theory. Such game comonads have been developed for various logics, yielding characterisations of logical equivalences in terms of isomorphisms in the associated co-Kleisli category. We show a first limitation of this approach by studying linear-algebraic logic, which is strictly more expressive than first-order counting logic and whose k-variable logical equivalence relations are known as invertible-map equivalences (IM). We show that there exists no finite-rank comonad on the category of graphs whose co-Kleisli isomorphisms characterise IM-equivalence, answering a question of Ó Conghaile and Dawar (CSL 2021). We obtain this result by ruling out a characterisation of IM-equivalence in terms of homomorphism indistinguishability and employing the Lovász-type theorems for game comonads established by Dawar, Jakl, and Reggio (2021). Two graphs are homomorphism indistinguishable over a graph class if they admit the same number of homomorphisms from every graph in the class. The IM-equivalences cannot be characterised in this way, neither when counting homomorphisms in the natural numbers, nor in any finite prime field.

We extend Choiceless Polynomial Time (CPT), the currently only remaining promising candidate in the quest for a logic capturing Ptime , so that this extended logic has the following property: for every class of structures for which isomorphism is definable, the logic automatically captures Ptime . For the construction of this logic, we extend CPT by a witnessed symmetric choice operator. This operator allows for choices from definable orbits. But, to ensure polynomial-time evaluation, automorphisms have to be provided to certify that the choice set is indeed an orbit. We argue that, in this logic, definable isomorphism implies definable canonization. Thereby, our construction removes the non-trivial step of extending isomorphism definability results to canonization. This step was a part of proofs that show that CPT or other logics capture Ptime on a particular class of structures. The step typically required substantial extra effort.

The k-dimensional Weisfeiler-Leman (k-WL) algorithm is a simple combinatorial algorithm that was originally designed as a graph isomorphism heuristic. It naturally finds applications in Babai’s quasipolynomial-time isomorphism algorithm, practical isomorphism solvers, and algebraic graph theory. However, it also has surprising connections to other areas such as logic, proof complexity, combinatorial optimization, and machine learning. The algorithm iteratively computes a coloring of the k-tuples of vertices of a graph. Since Fürer’s linear lower bound [ICALP 2001], it has been an open question whether there is a super-linear lower bound for the iteration number for k-WL on graphs. We answer this question affirmatively, establishing an $\Omega\left(n^{k / 2}\right)$-lower bound for all k.

At the core of the quest for a logic for Ptime is a mismatch between algorithms making arbitrary choices and isomorphism-invariant logics. One approach to tackle this problem is witnessed symmetric choice. It allows for choices from definable orbits certified by definable witnessing automorphisms. We consider the extension of fixed-point logic with counting (IFPC) with witnessed symmetric choice (IFPC+WSC) and a further extension with an interpretation operator (IFPC+WSC+I). The latter operator evaluates a subformula in the structure defined by an interpretation. When similarly extending pure fixed-point logic (IFP), IFP+WSC+I simulates counting which IFP+WSC fails to do. For IFPC+WSC, it is unknown whether the interpretation operator increases expressiveness and thus allows studying the relation between WSC and interpretations beyond counting. In this paper, we separate IFPC+WSC from IFPC+WSC+I by showing that IFPC+WSC is not closed under FO-interpretations. By the same argument, we answer an open question of Dawar and Richerby regarding non-witnessed symmetric choice in IFP. Additionally, we prove that nesting WSC-operators increases the expressiveness using the so-called CFI graphs. We show that if IFPC+WSC+I canonizes a particular class of base graphs, then it also canonizes the corresponding CFI graphs. This differs from various other logics, where CFI graphs provide difficult instances.

We prove new upper and lower bounds on the number of iterations the k-dimensional Weisfeiler-Leman algorithm (k-WL) requires until stabilization. For k ≥ 3, we show that k-WL stabilizes after at most O(knk−1log n) iterations (where n denotes the number of vertices of the input structures), obtaining the first improvement over the trivial upper bound of nk− 1 and extending a previous upper bound of O(n log n) for k = 2 [Lichter et al., LICS 2019].We complement our upper bounds by constructing k-ary relational structures on which k-WL requires at least nΩ(k)iterations to stabilize. This improves over a previous lower bound of nΩ(k/logk)[Berkholz, Nordström, LICS 2016].We also investigate tradeoffs between the dimension and the iteration number of WL, and show that d-WL, where $d = \left\lceil {\frac{{3(k + 1)}}{2}} \right\rceil $, can simulate the k-WL algorithm using only O(k2• n⌊k/2⌋+1log n) many iterations, but still requires at least nΩ(k)iterations for any d (that is sufficiently smaller than n).The number of iterations required by k-WL to distinguish two structures corresponds to the quantifier rank of a sentence distinguishing them in the (k + 1)-variable fragment ${{\mathcal{C}}_k}_{ + 1}$ of first-order logic with counting quantifiers. Hence, our results also imply new upper and lower bounds on the quantifier rank required in the logic ${{\mathcal{C}}_k}_{ + 1}$, as well as tradeoffs between variable number and quantifier rank.

In the search for a logic capturing polynomial time the most promising candidates are Choiceless Polynomial Time (CPT) and rank logic. Rank logic extends fixed-point logic with counting by a rank operator over prime fields. We show that the isomorphism problem for CFI graphs over ℤ 2 i cannot be defined in rank logic, even if the base graph is totally ordered. However, CPT can define this isomorphism problem. We thereby separate rank logic from CPT and in particular from polynomial time.

Abstract This note draws conclusions that arise by combining two recent papers, by Anuj Dawar, Erich Grädel and Wied Pakusa, published at ICALP 2019, and by Moritz Lichter, published at LICS 2021. In both papers, the main technical results rely on the combinatorial and algebraic analysis of the invertible-map equivalences ${\equiv ^{\text {IM}}_{k, Q}}$ on certain variants of Cai–Fürer–Immerman structures (CFI-structures for short). These ${\equiv ^{\text {IM}}_{k, Q}}$-equivalences, for a natural number $k$ and a set of primes $Q$, refine the well-known Weisfeiler–Leman equivalences used in algorithms for graph isomorphism. The intuition is that two graphs $G{\equiv ^{\text {IM}}_{k, Q}}H$ cannot be distinguished by iterative refinements of equivalences on $k$-tuples defined via linear operators on vector spaces over fields of characteristic $p \in Q$. In the first paper it has been shown, using considerable algebraic machinery, that for a prime $q \notin Q$, the ${\equiv ^{\text {IM}}_{k, Q}}$ equivalences are not strong enough to distinguish between non-isomorphic CFI-structures over the field $\mathbb {F}_q$. In the second paper, a similar but not identical construction for CFI-structures over the rings $\mathbb {Z}_{2^i}$ has, again by rather involved combinatorial and algebraic arguments, been shown to be indistinguishable with respect to ${\equiv ^{\text {IM}}_{k, \{2\}}}$. Together with an earlier work on rank logic, this second result suffices to separate rank logic from polynomial time. We show here that the two approaches can be unified to prove that CFI-structures over the rings $\mathbb {Z}_{2^i}$ are in fact indistinguishable with respect to ${\equiv ^{\text {IM}}_{k, {\mathbb {P}}}}$, for the set ${\mathbb {P}}$ of all primes. In particular, this implies the following two results. First, there is no fixed $k$ such that the invertible-map equivalence ${\equiv ^{\text {IM}}_{k, {\mathbb {P}}}}$ coincides with isomorphism on all finite graphs. Second, no extension of fixed-point logic by linear-algebraic operators over fields can capture polynomial time.

We extend Choiceless Polynomial Time (CPT), the currently only remaining promising candidate in the quest for a logic capturing Ptime, so that this extended logic has the following property: for every class of structures for which isomorphism is definable, the logic automatically captures Ptime.

In the quest for a logic capturing PTime the next natural classes of structures to consider are those with bounded color class size. We present a canonization procedure for graphs with dihedral color classes of bounded size in the logic of Choiceless Polynomial Time (CPT), which then captures PTime on this class of structures. This is the first result of this form for non-abelian color classes. The first step proposes a normal form which comprises a "rigid assemblage". This roughly means that the local automorphism groups form 2-injective 3-factor subdirect products. Structures with color classes of bounded size can be reduced canonization preservingly to normal form in CPT. In the second step, we show that for graphs in normal form with dihedral color classes of bounded size, the canonization problem can be solved in CPT. We also show the same statement for general ternary structures in normal form if the dihedral groups are defined over odd domains.

In the search for a logic capturing polynomial time the most promising candidates are Choiceless Polynomial Time (CPT) and rank logic. Rank logic extends fixed-point logic with counting by a rank operator over prime fields. We show that the isomorphism problem for CFI graphs over ${{\mathbb{Z}}_{{2^i}}}$ cannot be defined in rank logic, even if the base graph is totally ordered. However, CPT can define this isomorphism problem. We thereby separate rank logic from CPT and in particular from polynomial time.

We show that the 2-dimensional Weisfeiler-Leman algorithm stabilizes n-vertex graphs after at most O(n log n) iterations. This implies that if such graphs are distinguishable in 3-variable first order logic with counting, then they can also be distinguished in this logic by a formula of quantifier depth at most O(n log n). For this we exploit a new refinement based on counting walks and argue that its iteration number differs from the classic Weisfeiler-Leman refinement by at most a logarithmic factor. We then prove matching linear upper and lower bounds on the number of iterations of the walk refinement. This is achieved with an algebraic approach by exploiting properties of semisimple matrix algebras. We also define a walk logic and a bijective walk pebble game that precisely correspond to the new walk refinement.

Build systems are used in all but the smallest software projects to invoke the right build tools on the right files in the right order. A build system must be sound (after a build, generated files consistently reflect the latest source files) and efficient (recheck and rebuild as few build units as possible). Contemporary build systems provide limited efficiency because they lack support for expressing fine-grained file dependencies. We present a build system called pluto that supports the definition of reusable, parameterized, interconnected builders. When run, a builder notifies the build system about dynamically required and produced files as well as about other builders whose results are needed. To support fine-grained file dependencies, we generalize the traditional notion of time stamps to allow builders to declare their actual requirements on a file's content. pluto collects the requirements and products of a builder with their stamps in a build summary. This enables pluto to provides provably sound and optimal incremental rebuilding. To support dynamic dependencies, our rebuild algorithm interleaves dependency analysis and builder execution and enforces invariants on the dependency graph through a dynamic analysis. We have developed pluto as a Java API and used it to implement more than 25 builders. We describe our experience with migrating a larger Ant build script to pluto and compare the respective build times.