50 Search Results for "Forster, Sebastian"

Document
DOI: 10.4230/LIPIcs.STACS.2026.38
Fully Dynamic Spectral Sparsification for Directed Hypergraphs

Authors: Sebastian Forster, Gramoz Goranci, and Ali Momeni

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
There has been a surge of interest in spectral hypergraph sparsification, a natural generalization of spectral sparsification for graphs. In this paper, we present a simple fully dynamic algorithm for maintaining spectral hypergraph sparsifiers of directed hypergraphs. Our algorithm achieves a near-optimal size of O(n² / ε ² log ⁷ m) and amortized update time of O(r² log ³ m), where n is the number of vertices, and m and r respectively upper bound the number of hyperedges and the rank of the hypergraph at any time. We also extend our approach to the parallel batch-dynamic setting, where a batch of any k hyperedge insertions or deletions can be processed with O(kr² log ³ m) amortized work and O(log ² m) depth. This constitutes the first spectral-based sparsification algorithm in this setting.
Cite as

Sebastian Forster, Gramoz Goranci, and Ali Momeni. Fully Dynamic Spectral Sparsification for Directed Hypergraphs. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 38:1-38:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.STACS.2026.38,
  author =	{Forster, Sebastian and Goranci, Gramoz and Momeni, Ali},
  title =	{{Fully Dynamic Spectral Sparsification for Directed Hypergraphs}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{38:1--38:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.38},
  URN =		{urn:nbn:de:0030-drops-255272},
  doi =		{10.4230/LIPIcs.STACS.2026.38},
  annote =	{Keywords: Spectral sparsification, Dynamic algorithms, (Directed) hypergraphs, Data structures}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.19
Clustering in Varying Metrics

Authors: Deeparnab Chakrabarty, Jonathan Conroy, and Ankita Sarkar

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
We introduce the aggregated clustering problem, where one is given T instances of a center-based clustering task over the same n points, but under different metrics. The goal is to open k centers to minimize an aggregate of the clustering costs - e.g., the average or maximum - where the cost is measured via k-center/median/means objectives. More generally, we minimize a norm Ψ over the T cost values. We show that for T ≥ 3, the problem is inapproximable to any finite factor in polynomial time. For T = 2, we give constant-factor approximations. We also show W[2]-hardness when parameterized by k, but obtain f(k,T)poly(n)-time 3-approximations when parameterized by both k and T. When the metrics have structure, we obtain efficient parameterized approximation schemes (EPAS). If all T metrics have bounded ε-scatter dimension, we achieve a (1+ε)-approximation in f(k,T,ε)poly(n) time. If the metrics are induced by edge weights on a common graph G of bounded treewidth tw, and Ψ is the sum function, we get an EPAS in f(T,ε,tw)poly(n,k) time. Conversely, unless (randomized) ETH is false, any finite factor approximation is impossible if parametrized by only T, even when the treewidth is tw = Ω(polylog n).
Cite as

Deeparnab Chakrabarty, Jonathan Conroy, and Ankita Sarkar. Clustering in Varying Metrics. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chakrabarty_et_al:LIPIcs.FSTTCS.2025.19,
  author =	{Chakrabarty, Deeparnab and Conroy, Jonathan and Sarkar, Ankita},
  title =	{{Clustering in Varying Metrics}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{19:1--19:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.19},
  URN =		{urn:nbn:de:0030-drops-251007},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.19},
  annote =	{Keywords: Clustering, approximation algorithms, LP rounding, parameterized and exact algorithms, dynamic programming, fixed parameter tractability, hardness of approximation}
}
Document
Invited Paper
DOI: 10.4230/OASIcs.RW.2024/2025.7
Modern Datalog: Concepts, Methods, Applications (Invited Paper)

Authors: Markus Krötzsch

Published in: OASIcs, Volume 138, Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025)

Abstract
Pure Datalog is arguably the most fundamental rule language, elegant and simple, but also often too limited to be useful in practice. This has motivated the introduction of many new expressive features, ranging from datatypes and related functions, over aggregates and semi-ring generalisations, to existential quantifiers and complex terms. In spite of their variety, all these approaches remain true to the nature of Datalog as a direct, pattern-based way of computing on structured data. We therefore find that a modern notion of Datalog is emerging, distinctly different from other approaches of logic programming and with its own set of related methods and applications. In this course, we introduce Datalog and its most common extensions, and explain when and how these features can be used together (which is often, but not always, safe to do). We further look at modern Datalog systems and some of their primary use cases. Hands-on work with Datalog and its extensions is done with the free Datalog engine https://knowsys.github.io/nemo-doc/. The course is accessible to all audiences and does not assume specific prior knowledge.
Cite as

Markus Krötzsch. Modern Datalog: Concepts, Methods, Applications (Invited Paper). In Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025). Open Access Series in Informatics (OASIcs), Volume 138, pp. 7:1-7:41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{krotzsch:OASIcs.RW.2024/2025.7,
  author =	{Kr\"{o}tzsch, Markus},
  title =	{{Modern Datalog: Concepts, Methods, Applications}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{7:1--7:41},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-405-5},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{138},
  editor =	{Artale, Alessandro and Bienvenu, Meghyn and Garc{\'\i}a, Yazm{\'\i}n Ib\'{a}\~{n}ez and Murlak, Filip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.RW.2024/2025.7},
  URN =		{urn:nbn:de:0030-drops-250524},
  doi =		{10.4230/OASIcs.RW.2024/2025.7},
  annote =	{Keywords: Datalog, query language, knowlegde representation and reasoning, logic programming, Horn logic, SPARQL, datatypes and aggregation, lecture notes, tutorial}
}
Document
DOI: 10.4230/LIPIcs.GD.2025.16
Structural Parameterizations of k-Planarity

Authors: Tatsuya Gima, Yasuaki Kobayashi, and Yuto Okada

Published in: LIPIcs, Volume 357, 33rd International Symposium on Graph Drawing and Network Visualization (GD 2025)

Abstract
The concept of k-planarity is extensively studied in the context of Beyond Planarity. A graph is k-planar if it admits a drawing in the plane in which each edge is crossed at most k times. The local crossing number of a graph is the minimum integer k such that it is k-planar. The problem of determining whether an input graph is 1-planar is known to be NP-complete even for near-planar graphs [Cabello and Mohar, SIAM J. Comput. 2013], that is, the graphs obtained from planar graphs by adding a single edge. Moreover, the local crossing number is hard to approximate within a factor 2 - ε for any ε > 0 [Urschel and Wellens, IPL 2021]. To address this computational intractability, Bannister, Cabello, and Eppstein [JGAA 2018] investigated the parameterized complexity of the case of k = 1, particularly focusing on structural parameterizations on input graphs, such as treedepth, vertex cover number, and feedback edge number. In this paper, we extend their approach by considering the general case k ≥ 1 and give (tight) parameterized upper and lower bound results. In particular, we strengthen the aforementioned lower bound results to subclasses of constant-treewidth graphs: we show that testing 1-planarity is NP-complete even for near-planar graphs with feedback vertex set number at most 3 and pathwidth at most 4, and the local crossing number is hard to approximate within any constant factor for graphs with feedback vertex set number at most 2.
Cite as

Tatsuya Gima, Yasuaki Kobayashi, and Yuto Okada. Structural Parameterizations of k-Planarity. In 33rd International Symposium on Graph Drawing and Network Visualization (GD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 357, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gima_et_al:LIPIcs.GD.2025.16,
  author =	{Gima, Tatsuya and Kobayashi, Yasuaki and Okada, Yuto},
  title =	{{Structural Parameterizations of k-Planarity}},
  booktitle =	{33rd International Symposium on Graph Drawing and Network Visualization (GD 2025)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-403-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{357},
  editor =	{Dujmovi\'{c}, Vida and Montecchiani, Fabrizio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.GD.2025.16},
  URN =		{urn:nbn:de:0030-drops-250021},
  doi =		{10.4230/LIPIcs.GD.2025.16},
  annote =	{Keywords: 1-planar graphs, local crossing number, beyond planarity, parameterized complexity, kernelization}
}
Document
DOI: 10.4230/LIPIcs.GD.2025.17
Visualizing Treewidth

Authors: Alvin Chiu, Thomas Depian, David Eppstein, Michael T. Goodrich, and Martin Nöllenburg

Published in: LIPIcs, Volume 357, 33rd International Symposium on Graph Drawing and Network Visualization (GD 2025)

Abstract
A witness drawing of a graph is a visualization that clearly shows a given property of a graph. We study and implement various drawing paradigms for witness drawings to clearly show that graphs have bounded pathwidth or treewidth. Our approach draws the tree decomposition or path decomposition as a tree of bags, with induced subgraphs shown in each bag, and with "tracks" for each graph vertex connecting its copies in multiple bags. Within bags, we optimize the vertex layout to avoid crossings of edges and tracks. We implement a visualization prototype for crossing minimization using dynamic programming for graphs of small width and heuristic approaches for graphs of larger width. We introduce a taxonomy of drawing styles, which render the subgraph for each bag as an arc diagram with one or two pages or as a circular layout with straight-line edges, and we render tracks either with straight lines or with orbital-radial paths.
Cite as

Alvin Chiu, Thomas Depian, David Eppstein, Michael T. Goodrich, and Martin Nöllenburg. Visualizing Treewidth. In 33rd International Symposium on Graph Drawing and Network Visualization (GD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 357, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chiu_et_al:LIPIcs.GD.2025.17,
  author =	{Chiu, Alvin and Depian, Thomas and Eppstein, David and Goodrich, Michael T. and N\"{o}llenburg, Martin},
  title =	{{Visualizing Treewidth}},
  booktitle =	{33rd International Symposium on Graph Drawing and Network Visualization (GD 2025)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-403-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{357},
  editor =	{Dujmovi\'{c}, Vida and Montecchiani, Fabrizio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.GD.2025.17},
  URN =		{urn:nbn:de:0030-drops-250034},
  doi =		{10.4230/LIPIcs.GD.2025.17},
  annote =	{Keywords: Graph drawing, witness drawings, pathwidth, treewidth}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.26
Towards Constant Time Multi-Call Rumor Spreading on Small-Set Expanders

Authors: Emilio Cruciani, Sebastian Forster, and Tijn de Vos

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
We study a multi-call variant of the classic PUSH&PULL rumor spreading process where nodes can contact k of their neighbors instead of a single one during both PUSH and PULL operations. We show that rumor spreading can be made faster at the cost of an increased amount of communication between the nodes. As a motivating example, consider the process on a complete graph of n nodes: while the standard PUSH&PULL protocol takes Θ(log n) rounds, we prove that our k-PUSH&PULL variant completes in Θ(log_{k} n) rounds, with high probability. We generalize this result in an expansion-sensitive way, as has been done for the classic PUSH&PULL protocol for different notions of expansion, e.g., conductance and vertex expansion. We consider small-set vertex expanders, graphs in which every sufficiently small subset of nodes has a large neighborhood, ensuring strong local connectivity. In particular, when the expansion parameter satisfies ϕ > 1, these graphs have a diameter of o(log n), as opposed to other standard notions of expansion. Since the graph’s diameter is a lower bound on the number of rounds required for rumor spreading, this makes small-set expanders particularly well-suited for fast information dissemination. We prove that k-PUSH&PULL takes O(log_{ϕ} n ⋅ log_{k} n) rounds in these expanders, with high probability. We complement this with a simple lower bound of Ω(log_{ϕ} n+ log_{k} n) rounds.
Cite as

Emilio Cruciani, Sebastian Forster, and Tijn de Vos. Towards Constant Time Multi-Call Rumor Spreading on Small-Set Expanders. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 26:1-26:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cruciani_et_al:LIPIcs.DISC.2025.26,
  author =	{Cruciani, Emilio and Forster, Sebastian and de Vos, Tijn},
  title =	{{Towards Constant Time Multi-Call Rumor Spreading on Small-Set Expanders}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{26:1--26:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.26},
  URN =		{urn:nbn:de:0030-drops-248434},
  doi =		{10.4230/LIPIcs.DISC.2025.26},
  annote =	{Keywords: small set expansion, vertex expansion, rumor spreading, multi-call rumor spreading, push\&pull protocol}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.25
Model-Agnostic Approximation of Constrained Forest Problems

Authors: Corinna Coupette, Alipasha Montaseri, and Christoph Lenzen

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
Constrained Forest Problems (CFPs) as introduced by Goemans and Williamson in 1995 capture a wide range of network design problems with edge subsets as solutions, such as Minimum Spanning Tree, Steiner Forest, and Point-to-Point Connection. While individual CFPs have been studied extensively in individual computational models, a unified approach to solving general CFPs in multiple computational models has been lacking. Against this background, we present the shell-decomposition algorithm, a model-agnostic meta-algorithm that efficiently computes a (2+ε)-approximation to CFPs for a broad class of forest functions. The shell-decomposition algorithm isolates the problem-specific hardness of individual CFPs in a single computational subroutine, breaking the remainder of the computation into fundamental tasks that are studied extensively in a wide range of computational models. In contrast to prior work, our framework is compatible with the use of approximate distances. To demonstrate the power and flexibility of this result, we instantiate our algorithm for three fundamental, NP-hard CFPs (Steiner Forest, Point-to-Point Connection, and Facility Placement and Connection) in three different computational models (Congest, PRAM, and Multi-Pass Streaming). For constant ε, we obtain the following (2+ε)-approximations in the Congest model: [(1)] 1) For Steiner Forest specified via input components (SF-IC), where each node knows the identifier of one of k disjoint subsets of V (the input components), we achieve a deterministic (2+ε)-approximation in 𝒪̃(√n+D+k) rounds, where D is the hop diameter of the graph, significantly improving over the state of the art. 2) For Steiner Forest specified via symmetric connection requests (SF-SCR), where connection requests are issued to pairs of nodes u,v ∈ V, we leverage randomized equality testing to reduce the running time to 𝒪̃(√n+D), succeeding with high probability. 3) For Point-to-Point Connection, we provide a (2+ε)-approximation in 𝒪̃(√n+D) rounds. 4) For Facility Placement and Connection, a relative of non-metric Uncapacitated Facility Location, we obtain a (2+ε)-approximation in 𝒪̃(√n + D) rounds. We further show how to replace the √n+D term by the complexity of solving Partwise Aggregation, achieving (near-)universal optimality in any setting in which a solution to Partwise Aggregation in near-shortcut-quality time is known. Notably, all of our concrete results can be derived with relative ease once our model-agnostic meta-algorithm has been specified. This demonstrates the power of our modularization approach to algorithm design.
Cite as

Corinna Coupette, Alipasha Montaseri, and Christoph Lenzen. Model-Agnostic Approximation of Constrained Forest Problems. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 25:1-25:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{coupette_et_al:LIPIcs.DISC.2025.25,
  author =	{Coupette, Corinna and Montaseri, Alipasha and Lenzen, Christoph},
  title =	{{Model-Agnostic Approximation of Constrained Forest Problems}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{25:1--25:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.25},
  URN =		{urn:nbn:de:0030-drops-248420},
  doi =		{10.4230/LIPIcs.DISC.2025.25},
  annote =	{Keywords: Distributed Graph Algorithms, Model-Agnostic Algorithms, Steiner Forest}
}
Document
DOI: 10.4230/LIPIcs.ESA.2025.32
Linear-Time Multilevel Graph Partitioning via Edge Sparsification

Authors: Lars Gottesbüren, Nikolai Maas, Dominik Rosch, Peter Sanders, and Daniel Seemaier

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
The current landscape of balanced graph partitioning is divided into high-quality but expensive multilevel algorithms and cheaper approaches with linear running time, such as single-level algorithms and streaming algorithms. We demonstrate how to achieve the best of both worlds with a linear time multilevel algorithm. Multilevel algorithms construct a hierarchy of increasingly smaller graphs by repeatedly contracting clusters of nodes. Our approach preserves their distinct advantage, allowing refinement of the partition over multiple levels with increasing detail. At the same time, we use edge sparsification to guarantee geometric size reduction between the levels and thus linear running time. We provide a proof of the linear running time as well as additional insights into the behavior of multilevel algorithms, showing that graphs with low modularity are most likely to trigger worst-case running time. We evaluate multiple approaches for edge sparsification and integrate our algorithm into the state-of-the-art multilevel partitioner KaMinPar, maintaining its excellent parallel scalability. As demonstrated in detailed experiments, this results in a 1.49× average speedup (up to 4× for some instances) with only 1% loss in solution quality. Moreover, our algorithm clearly outperforms state-of-the-art single-level and streaming approaches.
Cite as

Lars Gottesbüren, Nikolai Maas, Dominik Rosch, Peter Sanders, and Daniel Seemaier. Linear-Time Multilevel Graph Partitioning via Edge Sparsification. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gottesburen_et_al:LIPIcs.ESA.2025.32,
  author =	{Gottesb\"{u}ren, Lars and Maas, Nikolai and Rosch, Dominik and Sanders, Peter and Seemaier, Daniel},
  title =	{{Linear-Time Multilevel Graph Partitioning via Edge Sparsification}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.32},
  URN =		{urn:nbn:de:0030-drops-245007},
  doi =		{10.4230/LIPIcs.ESA.2025.32},
  annote =	{Keywords: Graph Partitioning, Graph Algorithms, Linear Time Algorithms, Graph Sparsification}
}
Document
DOI: 10.4230/LIPIcs.ESA.2025.21
A Unified FPT Framework for Crossing Number Problems

Authors: Éric Colin de Verdière and Petr Hliněný

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
The basic (and traditional) crossing number problem is to determine the minimum number of crossings in a topological drawing of an input graph in the plane. We develop a unified framework that smoothly captures many generalized crossing number problems, and that yields fixed-parameter tractable (FPT) algorithms for them not only in the plane but also on surfaces. Our framework takes the following form. We fix a surface S, an integer r, and a map κ from the set of topological drawings of graphs in S to ℤ_+ ∪ {∞}, satisfying some natural monotonicity conditions, but essentially describing the allowed drawings and how we want to count the crossings in them. Then deciding whether an input graph G has an allowed drawing D on S with κ(D) ≤ r can be done in time quadratic in the size of G (and exponential in other parameters). More generally, we may take as input an edge-colored graph, and distinguish crossings by the colors of the involved edges; and we may allow to perform a bounded number of edge removals and vertex splits to G before drawing it. The proof is a reduction to the embeddability of a graph on a two-dimensional simplicial complex. This framework implies, in a unified way, quadratic FPT algorithms for many topological crossing number variants established in the graph drawing community. Some of these variants already had previously published FPT algorithms, mostly relying on Courcelle’s metatheorem, but for many of those, we obtain an algorithm with a better runtime. Moreover, our framework extends, at no cost, to these crossing number variants in any fixed surface.
Cite as

Éric Colin de Verdière and Petr Hliněný. A Unified FPT Framework for Crossing Number Problems. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{colindeverdiere_et_al:LIPIcs.ESA.2025.21,
  author =	{Colin de Verdi\`{e}re, \'{E}ric and Hlin\v{e}n\'{y}, Petr},
  title =	{{A Unified FPT Framework for Crossing Number Problems}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.21},
  URN =		{urn:nbn:de:0030-drops-244897},
  doi =		{10.4230/LIPIcs.ESA.2025.21},
  annote =	{Keywords: computational geometry, fixed-parameter tractability, graph drawing, graph embedding, crossing number, two-dimensional simplicial complex, surface}
}
Document
DOI: 10.4230/LIPIcs.ESA.2025.20
Beeping Deterministic CONGEST Algorithms in Graphs

Authors: Pawel Garncarek, Dariusz R. Kowalski, Shay Kutten, and Miguel A. Mosteiro

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
Beeping Network (BN) is a popular graph-based model of wireless computation, which applies the OR operation to one-bit messages sent simultaneously by neighbors. It admits fast (polylogarithmic in the number of nodes n) randomized solutions to many graph problems, but all known deterministic algorithms for non-trivial graph problems are at least polynomial in the maximum node degree Δ. We improve known results for deterministic algorithms by showing that this polynomial can be as low as Õ(Δ²). More precisely, we show how to simulate a single round of any CONGEST algorithm in any network in O(Δ² polylog n) beeping rounds, each accommodating at most one beep per node, even if the nodes intend to send different messages to different neighbors. This upper bound reduces polynomially the time for a deterministic simulation of CONGEST in a Beeping Network, comparing to the best known algorithms, and nearly matches the time obtained recently using randomization (up to a poly-logarithmic factor) as well as the lower bound. Specifically, any algorithm designed for the CONGEST networks can be run in BNs with O(Δ² polylog n) multiplicative overhead, e.g., we can now deterministically compute an MIS in any BN in O(Δ² polylog n) beeping rounds, improving the previous best Θ(Δ³)-round solution. For h-hop simulations, we prove a lower bound Ω(Δ^{h+1}), and we design a nearly matching algorithm that is able to "pipeline" the node-to-node information in a faster way than beeping layer-by-layer.
Cite as

Pawel Garncarek, Dariusz R. Kowalski, Shay Kutten, and Miguel A. Mosteiro. Beeping Deterministic CONGEST Algorithms in Graphs. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{garncarek_et_al:LIPIcs.ESA.2025.20,
  author =	{Garncarek, Pawel and Kowalski, Dariusz R. and Kutten, Shay and Mosteiro, Miguel A.},
  title =	{{Beeping Deterministic CONGEST Algorithms in Graphs}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{20:1--20:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.20},
  URN =		{urn:nbn:de:0030-drops-244880},
  doi =		{10.4230/LIPIcs.ESA.2025.20},
  annote =	{Keywords: Beeping Networks, CONGEST Networks, deterministic simulations, graph algorithms}
}
Document
DOI: 10.4230/LIPIcs.ESA.2025.113
Bootstrapping Dynamic APSP via Sparsification

Authors: Rasmus Kyng, Simon Meierhans, and Gernot Zöcklein

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
We give a simple algorithm for the dynamic approximate All-Pairs Shortest Paths (APSP) problem. Given a graph G = (V, E, l) with polynomially bounded edge lengths, our data structure processes |E| edge insertions and deletions in total time |E|^{1+o(1)} and provides query access to |E|^o(1)-approximate distances in time Õ(1) per query. We produce a data structure that mimics Thorup-Zwick distance oracles [Thorup and Zwick, 2005], but is dynamic and deterministic. Our algorithm selects a small number of pivot vertices. Then, for every other vertex, it reduces distance computation to maintaining distances to a small neighborhood around that vertex and to the nearest pivot. We maintain distances between pivots efficiently by representing them in a smaller graph and recursing. We maintain these smaller graphs by (a) reducing vertex count using the dynamic distance-preserving core graphs of Kyng-Meierhans-Probst Gutenberg [Kyng et al., 2024] in a black-box manner and (b) reducing edge-count using a dynamic spanner akin to Chen-Kyng-Liu-Meierhans-Probst Gutenberg [Chen et al., 2024]. Our dynamic spanner internally uses an APSP data structure. Choosing a large enough size reduction factor in the first step allows us to simultaneously bootstrap a spanner and a dynamic APSP data structure. Notably, our approach does not need expander graphs, an otherwise ubiquitous tool in derandomization.
Cite as

Rasmus Kyng, Simon Meierhans, and Gernot Zöcklein. Bootstrapping Dynamic APSP via Sparsification. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 113:1-113:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kyng_et_al:LIPIcs.ESA.2025.113,
  author =	{Kyng, Rasmus and Meierhans, Simon and Z\"{o}cklein, Gernot},
  title =	{{Bootstrapping Dynamic APSP via Sparsification}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{113:1--113:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.113},
  URN =		{urn:nbn:de:0030-drops-245826},
  doi =		{10.4230/LIPIcs.ESA.2025.113},
  annote =	{Keywords: Dynamic Graph Algorithms, Spanners, Vertex Sparsification, Bootstrapping}
}
Document
DOI: 10.4230/LIPIcs.ESA.2025.36
Efficient Contractions of Dynamic Graphs - With Applications

Authors: Monika Henzinger, Evangelos Kosinas, Robin Münk, and Harald Räcke

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
A non-trivial minimum cut (NMC) sparsifier is a multigraph Ĝ that preserves all non-trivial minimum cuts of a given undirected graph G. We introduce a flexible data structure for fully dynamic graphs that can efficiently provide an NMC sparsifier upon request at any point during the sequence of updates. We employ simple dynamic forest data structures to achieve a fast from-scratch construction of the sparsifier at query time. Based on the strength of the adversary and desired type of time bounds, the data structure comes with different guarantees. Specifically, let G be a fully dynamic simple graph with n vertices and minimum degree δ. Then our data structure supports an insertion/deletion of an edge to/from G in n^o(1) worst-case time. Furthermore, upon request, it can return w.h.p. an NMC sparsifier of G that has O(n/δ) vertices and O(n) edges, in Ô(n) time. The probabilistic guarantees hold against an adaptive adversary. Alternatively, the update and query times can be improved to Õ(1) and Õ(n) respectively, if amortized-time guarantees are sufficient, or if the adversary is oblivious. Throughout the paper, we use Õ to hide polylogarithmic factors and Ô to hide subpolynomial (i.e., n^o(1)) factors. We discuss two applications of our new data structure. First, it can be used to efficiently report a cactus representation of all minimum cuts of a fully dynamic simple graph. Building this cactus for the NMC sparsifier instead of the original graph allows for a construction time that is sublinear in the number of edges. Against an adaptive adversary, we can with high probability output the cactus representation in worst-case Ô(n) time. Second, our data structure allows us to efficiently compute the maximal k-edge-connected subgraphs of undirected simple graphs, by repeatedly applying a minimum cut algorithm on the NMC sparsifier. Specifically, we can compute with high probability the maximal k-edge-connected subgraphs of a simple graph with n vertices and m edges in Õ(m+n²/k) time. This improves the best known time bounds for k = Ω(n^{1/8}) and naturally extends to the case of fully dynamic graphs.
Cite as

Monika Henzinger, Evangelos Kosinas, Robin Münk, and Harald Räcke. Efficient Contractions of Dynamic Graphs - With Applications. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 36:1-36:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.ESA.2025.36,
  author =	{Henzinger, Monika and Kosinas, Evangelos and M\"{u}nk, Robin and R\"{a}cke, Harald},
  title =	{{Efficient Contractions of Dynamic Graphs - With Applications}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{36:1--36:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.36},
  URN =		{urn:nbn:de:0030-drops-245047},
  doi =		{10.4230/LIPIcs.ESA.2025.36},
  annote =	{Keywords: Graph Algorithms, Cut Sparsifiers, Dynamic Algorithms}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.4
A Formalization of Divided Powers in Lean

Authors: Antoine Chambert-Loir and María Inés de Frutos-Fernández

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Given an ideal I in a commutative ring A, a divided power structure on I is a collection of maps {γ_n : I → A}_{n ∈ ℕ}, subject to axioms that imply that it behaves like the family {x ↦ xⁿ/n!}_{n ∈ ℕ}, but which can be defined even when division by factorials is not possible in A. Divided power structures have important applications in diverse areas of mathematics, including algebraic topology, number theory and algebraic geometry. In this article we describe a formalization in Lean 4 of the basic theory of divided power structures, including divided power morphisms and sub-divided power ideals, and we provide several fundamental constructions, in particular quotients and sums. This constitutes the first formalization of this theory in any theorem prover. As a prerequisite of general interest, we expand the formalized theory of multivariate power series rings, endowing them with a topology and defining evaluation and substitution of power series.
Cite as

Antoine Chambert-Loir and María Inés de Frutos-Fernández. A Formalization of Divided Powers in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chambertloir_et_al:LIPIcs.ITP.2025.4,
  author =	{Chambert-Loir, Antoine and de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s},
  title =	{{A Formalization of Divided Powers in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{4:1--4:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.4},
  URN =		{urn:nbn:de:0030-drops-246038},
  doi =		{10.4230/LIPIcs.ITP.2025.4},
  annote =	{Keywords: Formal mathematics, algebraic number theory, commutative algebra, divided powers, Lean, Mathlib}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.36
Verifying Datalog Reasoning with Lean

Authors: Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Datalog is an essential logical rule language with many applications, and modern rule engines compute logical consequences for Datalog with high performance and scalability. While Datalog is rather simple and, in principle, explainable by design, such sophisticated implementations and optimizations are hard to verify. We therefore propose a certificate-based approach to validate results of Datalog reasoners in a formally verified checker for Datalog proofs. Using the proof assistant Lean, we implement such a checker and verify its correctness against direct formalizations of the Datalog semantics. We propose two JSON encodings for Datalog proofs: one using the widely supported Datalog proof trees, and one using directed acyclic graphs for succinctness. To evaluate the practical feasibility and performance of our approach, we validate proofs that we obtain by converting derivation traces of an existing Datalog reasoner into our tool-independent format.
Cite as

Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. Verifying Datalog Reasoning with Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tantow_et_al:LIPIcs.ITP.2025.36,
  author =	{Tantow, Johannes and Gerlach, Lukas and Mennicke, Stephan and Kr\"{o}tzsch, Markus},
  title =	{{Verifying Datalog Reasoning with Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{36:1--36:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.36},
  URN =		{urn:nbn:de:0030-drops-246342},
  doi =		{10.4230/LIPIcs.ITP.2025.36},
  annote =	{Keywords: Certifying Algorithms, Datalog, Formal Verification}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2025.37
LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper)

Authors: Eric Vin, Kyle A. Miller, and Daniel J. Fremont

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, making it straightforward to define properties involving numerical or other types. We prove that standard flavors of LTL can be embedded in our framework. The library also provides automation for reasoning about LeanLTL formulas in a way that facilitates using Lean’s existing tactics. Finally, we provide examples illustrating the utility of the library in reasoning about systems that come from applications.
Cite as

Eric Vin, Kyle A. Miller, and Daniel J. Fremont. LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 37:1-37:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vin_et_al:LIPIcs.ITP.2025.37,
  author =	{Vin, Eric and Miller, Kyle A. and Fremont, Daniel J.},
  title =	{{LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{37:1--37:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.37},
  URN =		{urn:nbn:de:0030-drops-246356},
  doi =		{10.4230/LIPIcs.ITP.2025.37},
  annote =	{Keywords: Linear Temporal Logic, Interactive Theorem Proving, Lean 4}
}
  • Refine by Type
  • 50 Document/PDF
  • 37 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 37 2025
  • 3 2024
  • 4 2023
  • 3 2022
  • Show More...

  • Refine by Author
  • 7 Forster, Sebastian
  • 5 Nazari, Yasamin
  • 4 Beohar, Harsh
  • 4 Goranci, Gramoz
  • 4 de Vos, Tijn
  • Show More...

  • Refine by Series/Journal
  • 46 LIPIcs
  • 3 OASIcs
  • 1 DagRep

  • Refine by Classification
  • 12 Theory of computation → Dynamic graph algorithms
  • 9 Theory of computation → Sparsification and spanners
  • 6 Theory of computation → Modal and temporal logics
  • 4 Theory of computation → Distributed algorithms
  • 3 Mathematics of computing → Graph algorithms
  • Show More...

  • Refine by Keyword
  • 3 Dynamic Algorithms
  • 3 Graph Algorithms
  • 3 Hopsets
  • 3 Shortest Paths
  • 3 modal logics
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact