arXiv subjects

Moritz Lichter

Publications and source records attributed to Moritz Lichter.

14 recordsLinked to original sources

arXiv2026

Weisfeiler-Leman on graphs of small twin-width

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 number $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 purely combinatorial 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\'y, Guspiel, Hlinen\'y, Pokr\'yvka, and Sokolowski that stable graphs of twin-width 2 have bounded rank-width. This in particular implies that isomorphism of these graphs can be decided by a fixed dimension of the Weisfeiler-Leman algorithm.

math.CO↗

arXiv2024

Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism

We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Tor\'an and W\"orz (TOCL 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}$) and hence by a count-free variant of the $k$-dimensional Weisfeiler-Leman algorithm. 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^{\Omega(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 width versus tree-like size trade-off by Razborov (JACM 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 a modified variant of the compressed CFI graphs introduced by Grohe, Lichter, Neuen, and Schweitzer (FOCS 2023). Using a recent improved robust compressed CFI construction of Janett, Nordstr\"om, and Pang (unpublished manuscript), we obtain a similar bound for width $k$ (instead of the stronger but less common narrow width) and make the result more robust.

cs.LO↗

arXiv2024

Limitations of Affine Integer Relaxations for Solving Constraint Satisfaction Problems

We show that various recent algorithms for finite-domain constraint satisfaction problems (CSP), which are based on solving their affine integer relaxations, do not solve all tractable and not even all Maltsev CSPs. This rules them out as candidates for a universal polynomial-time CSP algorithm. The algorithms are $\mathbb{Z}$-affine $k$-consistency, BLP+AIP, BA$^{k}$, and CLAP. We thereby answer a question by Brakensiek, Guruswami, Wrochna, and \v{Z}ivn\'y whether BLP+AIP solves all tractable CSPs in the negative. We also refute a conjecture by Dalmau and Opr\v{s}al (LICS 2024) that every CSP is either solved by $\mathbb{Z}$-affine $k$-consistency or admits a Datalog reduction from 3-colorability. For the cohomological $k$-consistency algorithm, that is also based on affine relaxations, we show that it correctly solves our counterexample but fails on an NP-complete template.

cs.CC↗

arXiv2024

Computational complexity of the Weisfeiler-Leman dimension

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.

cs.CC↗

arXiv2023

Compressing CFI Graphs and Lower Bounds for the Weisfeiler-Leman Refinements

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\"urer'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(n^{k/2})$-lower bound for all $k$.

cs.DM↗

arXiv2023

Limitations of Game Comonads via Homomorphism Indistinguishability

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 \'O 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\'asz-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.

cs.LO↗

arXiv2023

The Iteration Number of the Weisfeiler-Leman Algorithm

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$ [Lichter et al., LICS 2019]. 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)}$ [Berkholz, Nordstr\"{o}m, LICS 2016]. 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 $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 $C_{k+1}$, as well as tradeoffs between variable number and quantifier rank.

cs.DS↗

arXiv2022

Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting

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 overcome this problem is witnessed symmetric choice. It allows for choices from definable orbits which are 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. This structure possibly has other automorphisms exploitable by the WSC-operator. For similar extensions of pure fixed-point logic (IFP) it is known that IFP+WSCI 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. We separate IFPC+WSC from IFPC+WSCI by showing that IFPC+WSC is not closed under FO-interpretations. 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.

cs.LO↗

arXiv2022

Choiceless Polynomial Time with Witnessed Symmetric Choice

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.

cs.LO↗

arXiv2021

Limitations of the Invertible-Map Equivalences

This note draws conclusions that arise by combining two recent papers, by Anuj Dawar, Erich Gr\"adel, 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\"urer-Immerman (CFI) structures. These $\equiv^\text{IM}_{k,Q}$-equivalences, for a 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 do not 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 earlier work, this second result separates rank logic from polynomial time. We unify the two approaches and prove that CFI-structures over the rings $\mathbb{Z}_{2^i}$ are indistinguishable with respect to $\equiv^\text{IM}_{k,\mathbb{P}}$, for the set $\mathbb{P}$ of all primes. This implies the following two results. 1. There is no fixed $k$ such that the invertible-map equivalence $\equiv^\text{IM}_{k,\mathbb{P}}$ coincides with isomorphism on all finite graphs. 2. No extension of fixed-point logic by linear-algebraic operators over fields can capture polynomial time.

cs.LO↗

arXiv2021

Separating Rank Logic from Polynomial Time

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.

cs.LO↗

arXiv2020

Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time

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.

cs.LO↗

arXiv2019

Walk refinement, walk logic, and the iteration number of the Weisfeiler-Leman algorithm

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.

cs.LO↗

arXiv2018

Constructive Analysis of S1S and Büchi Automata

We study S1S and Büchi automata in the constructive type theory of the Coq proof assistant. For UP semantics (ultimately periodic sequences), we verify Büchi's translation of formulas to automata and thereby establish decidability of S1S constructively. For AS semantics (all sequences), we verify Büchi's translation assuming that sequences over finite semigroups have Ramseyan factorisations (RF). Assuming RF, UP semantics and AS semantics agree. RF is a consequence of Ramsey's theorem and implies the infinite pigeonhole principle, which is known to be unprovable constructively. We show that each of the following properties holds for UP semantics but is equivalent to RF for AS semantics: excluded middle of formula satisfaction, excluded middle of automaton acceptance, and existence of complement automata.

cs.LO↗