84 Search Results for "Müller, Peter"


Volume

LIPIcs, Volume 74

31st European Conference on Object-Oriented Programming (ECOOP 2017)

ECOOP 2017, June 19-23, 2017, Barcelona, Spain

Editors: Peter Müller

Document
Connected Partitions via Connected Dominating Sets

Authors: Aikaterini Niklanovits, Kirill Simonov, Shaily Verma, and Ziena Zeif

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


Abstract
The classical theorem due to Győri and Lovász states that any k-connected graph G admits a partition into k connected subgraphs, where each subgraph has a prescribed size and contains a prescribed vertex, as long as the total size of target subgraphs is equal to the size of G. However, this result is notoriously evasive in terms of efficient constructions, and it is still unknown whether such a partition can be computed in polynomial time, even for k = 5. We make progress towards an efficient constructive version of the Győri-Lovász theorem by considering a natural strengthening of the k-connectivity requirement. Specifically, we show that the desired connected partition can be found in polynomial time, if G contains k disjoint connected dominating sets. As a consequence of this result, we give several efficient approximate and exact constructive versions of the original Győri-Lovász theorem: - On general graphs, a Győri-Lovász partition with k parts can be computed in polynomial time when the input graph has connectivity Ω(k ⋅ log² n); - On convex bipartite graphs, connectivity of 4k is sufficient; - On biconvex graphs and interval graphs, connectivity of k is sufficient, meaning that our algorithm gives a "true" constructive version of the theorem on these graph classes.

Cite as

Aikaterini Niklanovits, Kirill Simonov, Shaily Verma, and Ziena Zeif. Connected Partitions via Connected Dominating Sets. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{niklanovits_et_al:LIPIcs.ESA.2025.10,
  author =	{Niklanovits, Aikaterini and Simonov, Kirill and Verma, Shaily and Zeif, Ziena},
  title =	{{Connected Partitions via Connected Dominating Sets}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{10:1--10: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.10},
  URN =		{urn:nbn:de:0030-drops-244785},
  doi =		{10.4230/LIPIcs.ESA.2025.10},
  annote =	{Keywords: Gy\H{o}ri-Lov\'{a}sz theorem, connected dominating sets, graph classes}
}
Document
Fine-Grained Classification of Detecting Dominating Patterns

Authors: Jonathan Dransfeld, Marvin Künnemann, and Mirza Redzic

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


Abstract
We consider the following generalization of dominating sets: Let G be a host graph and P be a pattern graph P. A dominating P-pattern in G is a subset S of vertices in G that (1) forms a dominating set in G and (2) induces a subgraph isomorphic to P. The graph theory literature studies the properties of dominating P-patterns for various patterns P, including cliques, matchings, independent sets, cycles and paths. Previous work (Kunnemann, Redzic 2024) obtains algorithms and conditional lower bounds for detecting dominating P-patterns particularly for P being a k-clique, a k-independent set and a k-matching. Their results give conditionally tight lower bounds if k is sufficiently large (where the bound depends the matrix multiplication exponent ω). We ask: Can we obtain a classification of the fine-grained complexity for all patterns P? Indeed, we define a graph parameter ρ(P) such that if ω = 2, then (n^ρ(P) m^{(|V(P)|-ρ(P))/2})^{1±o(1)} is the optimal running time assuming the Orthogonal Vectors Hypothesis, for all patterns P except the triangle K₃. Here, the host graph G has n vertices and m = Θ(n^α) edges, where 1 ≤ α ≤ 2. The parameter ρ(P) is closely related (but sometimes different) to a parameter δ(P) = max_{S ⊆ V(P)} |S|-|N(S)| studied in (Alon 1981) to tightly quantify the maximum number of occurrences of induced subgraphs isomorphic to P. Our results stand in contrast to the lack of a full fine-grained classification of detecting an arbitrary (not necessarily dominating) induced P-pattern.

Cite as

Jonathan Dransfeld, Marvin Künnemann, and Mirza Redzic. Fine-Grained Classification of Detecting Dominating Patterns. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 98:1-98:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{dransfeld_et_al:LIPIcs.ESA.2025.98,
  author =	{Dransfeld, Jonathan and K\"{u}nnemann, Marvin and Redzic, Mirza},
  title =	{{Fine-Grained Classification of Detecting Dominating Patterns}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{98:1--98: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.98},
  URN =		{urn:nbn:de:0030-drops-245679},
  doi =		{10.4230/LIPIcs.ESA.2025.98},
  annote =	{Keywords: fine-grained complexity theory, domination in graphs, subgraph isomorphism, classification theorem, parameterized algorithms}
}
Document
Reconstructing Random Graphs from Distance Queries

Authors: Michael Krivelevich and Maksim Zhukovskii

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


Abstract
We estimate the minimum number of distance queries that is sufficient to reconstruct the binomial random graph G(n,p) with constant diameter with high probability. We get a tight (up to a constant factor) answer for all p > n^{-1+o(1)} outside "threshold windows" around n^{-k/(k+1)+o(1)}, k ∈ ℤ_{> 0}: with high probability the query complexity equals Θ(n^{4-d}p^{2-d}), where d is the diameter of the random graph. This demonstrates the following non-monotone behaviour: the query complexity jumps down at moments when the diameter gets larger; yet, between these moments the query complexity grows. We also show that there exists a non-adaptive algorithm that reconstructs the random graph with O(n^{4-d}p^{2-d}ln n) distance queries with high probability, and this is best possible.

Cite as

Michael Krivelevich and Maksim Zhukovskii. Reconstructing Random Graphs from Distance Queries. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{krivelevich_et_al:LIPIcs.ESA.2025.30,
  author =	{Krivelevich, Michael and Zhukovskii, Maksim},
  title =	{{Reconstructing Random Graphs from Distance Queries}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{30:1--30: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.30},
  URN =		{urn:nbn:de:0030-drops-244982},
  doi =		{10.4230/LIPIcs.ESA.2025.30},
  annote =	{Keywords: random graphs, graph reconstruction, distance queries, query complexity}
}
Document
Linear Layouts Revisited: Stacks, Queues, and Exact Algorithms

Authors: Thomas Depian, Simon D. Fink, Robert Ganian, and Vaishali Surianarayanan

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


Abstract
In spite of the extensive study of stack and queue layouts, many fundamental questions remain open concerning the complexity-theoretic frontiers for computing stack and queue layouts. A stack (resp. queue) layout places vertices along a line and assigns edges to pages so that no two edges on the same page are crossing (resp. nested). We provide three new algorithms which together substantially expand our understanding of these problems: 1) A fixed-parameter algorithm for computing minimum-page stack and queue layouts w.r.t. the vertex integrity of an n-vertex graph G. This result is motivated by an open question in the literature and generalizes the previous algorithms parameterizing by the vertex cover number of G. The proof relies on a newly developed Ramsey pruning technique. Vertex integrity intuitively measures the vertex deletion distance to a subgraph with only small connected components. 2) An n^𝒪(q 𝓁) algorithm for computing 𝓁-page stack and queue layouts of page width at most q. This is the first algorithm avoiding a double-exponential dependency on the parameters. The page width of a layout measures the maximum number of edges one needs to cross on any page to reach the outer face. 3) A 2^𝒪(n) algorithm for computing 1-page queue layouts. This improves upon the previously fastest n^𝒪(n) algorithm and can be seen as a counterpart to the recent subexponential algorithm for computing 2-page stack layouts [ICALP'24], but relies on an entirely different technique.

Cite as

Thomas Depian, Simon D. Fink, Robert Ganian, and Vaishali Surianarayanan. Linear Layouts Revisited: Stacks, Queues, and Exact Algorithms. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{depian_et_al:LIPIcs.ESA.2025.15,
  author =	{Depian, Thomas and Fink, Simon D. and Ganian, Robert and Surianarayanan, Vaishali},
  title =	{{Linear Layouts Revisited: Stacks, Queues, and Exact Algorithms}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{15:1--15: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.15},
  URN =		{urn:nbn:de:0030-drops-244835},
  doi =		{10.4230/LIPIcs.ESA.2025.15},
  annote =	{Keywords: stack layouts, queue layouts, parameterized algorithms, vertex integrity, Ramsey theory}
}
Document
Parameterized Algorithms for Computing Pareto Sets

Authors: Joshua Marc Könen, Heiko Röglin, and Tarek Stuck

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


Abstract
The problem of computing the set of Pareto-optimal solutions has been studied for a variety of multiobjective optimization problems. For many such problems, algorithms are known that compute the Pareto set in (weak) output-polynomial time. These algorithms are often based on dynamic programming and by weak output-polynomial time, we mean that the running time depends polynomially on the size of the Pareto set but also on the sizes of the Pareto sets of the subproblems that occur in the dynamic program. For some problems, like the multiobjective minimum spanning tree problem, such algorithms are not known to exist and for other problems, like multiobjective versions of many NP-hard problems, such algorithms cannot exist, unless 𝒫 = 𝒩𝒫. Dynamic programming over tree decompositions is a common technique in parameterized algorithms. In this paper, we study whether this technique can also be applied to compute Pareto sets of multiobjective optimization problems. We first derive an algorithm to compute the Pareto set for the multicriteria s-t cut problem and show how this result can be applied to a polygon aggregation problem arising in cartography that has recently been introduced by Rottmann et al. (GIScience 2021). We also show how to apply these techniques to also compute the Pareto set of the multiobjective minimum spanning tree problem and for the multiobjective TSP. The running time of our algorithms is O(f(w)⋅poly(n,p_{max})), where f is some function in the treewidth w, n is the input size, and p_{max} is an upper bound on the size of the Pareto sets of the subproblems that occur in the dynamic program. Finally, we present an experimental evaluation of computing Pareto sets on real-world instances of polygon aggregation problems. For this matter we devised a task-specific data structure that allows for efficient storage and modification of large sets of Pareto-optimal solutions. Throughout the implementation process, we incorporated several improved strategies and heuristics that significantly reduced both runtime and memory usage, enabling us to solve instances with treewidth of up to 22 within reasonable amount of time. Moreover, we conducted a preprocessing study to compare different tree decompositions in terms of their estimated overall runtime.

Cite as

Joshua Marc Könen, Heiko Röglin, and Tarek Stuck. Parameterized Algorithms for Computing Pareto Sets. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 105:1-105:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{konen_et_al:LIPIcs.ESA.2025.105,
  author =	{K\"{o}nen, Joshua Marc and R\"{o}glin, Heiko and Stuck, Tarek},
  title =	{{Parameterized Algorithms for Computing Pareto Sets}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{105:1--105: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.105},
  URN =		{urn:nbn:de:0030-drops-245749},
  doi =		{10.4230/LIPIcs.ESA.2025.105},
  annote =	{Keywords: parameterized algorithms, treewidth, multicriteria optimization problems, multicriteria MST, multicriteria TSP, polygon aggregation}
}
Document
Edge Clique Partition and Cover Beyond Independence

Authors: Fedor V. Fomin, Petr A. Golovach, Danil Sagunov, and Kirill Simonov

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


Abstract
Covering and partitioning the edges of a graph into cliques are classical problems at the intersection of combinatorial optimization and graph theory, having been studied through a range of algorithmic and complexity-theoretic lenses. Despite the well-known fixed-parameter tractability of these problems when parameterized by the total number of cliques, such a parameterization often fails to be meaningful for sparse graphs. In many real-world instances, on the other hand, the minimum number of cliques in an edge cover or partition can be very close to the size of a maximum independent set α(G). Motivated by this observation, we investigate above-α parameterizations of the edge clique cover and partition problems. Concretely, we introduce and study Edge Clique Cover Above Independent Set (ECC/α) and Edge Clique Partition Above Independent Set (ECP/α), where the goal is to cover or partition all edges of a graph using at most α(G) + k cliques, and k is the parameter. Our main results reveal a distinct complexity landscape for the two variants. We show that ECP/α is fixed-parameter tractable, whereas ECC/α is NP-complete for all k ≥ 2, yet can be solved in polynomial time for k ∈ {0,1}. These findings highlight intriguing differences between the two problems when viewed through the lens of parameterization above a natural lower bound. Finally, we demonstrate that ECC/α becomes fixed-parameter tractable when parameterized by k + ω(G), where ω(G) is the size of a maximum clique of the graph G. This result is particularly relevant for sparse graphs, in which ω is typically small. For H-minor free graphs, we design a subexponential algorithm of running time f(H)^√k ⋅ n^𝒪(1).

Cite as

Fedor V. Fomin, Petr A. Golovach, Danil Sagunov, and Kirill Simonov. Edge Clique Partition and Cover Beyond Independence. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 43:1-43:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{fomin_et_al:LIPIcs.ESA.2025.43,
  author =	{Fomin, Fedor V. and Golovach, Petr A. and Sagunov, Danil and Simonov, Kirill},
  title =	{{Edge Clique Partition and Cover Beyond Independence}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{43:1--43:16},
  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.43},
  URN =		{urn:nbn:de:0030-drops-245113},
  doi =		{10.4230/LIPIcs.ESA.2025.43},
  annote =	{Keywords: edge clique partition, edge clique cover, independence number, parameterized complexity, above guarantee}
}
Document
Engineering Minimal k-Perfect Hash Functions

Authors: Stefan Hermann, Sebastian Kirmayer, Hans-Peter Lehmann, Peter Sanders, and Stefan Walzer

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


Abstract
Given a set S of n keys, a k-perfect hash function (kPHF) is a data structure that maps the keys to the first m integers, where each output integer can be hit by at most k input keys. When m = ⌈n/k⌉, the resulting function is called a minimal k-perfect hash function (MkPHF). Applications of kPHFs can be found in external memory data structures or to create efficient 1-perfect hash functions, which in turn have a wide range of applications from databases to bioinformatics. Several papers from the 1980s look at external memory data structures with small internal memory indexes. However, actual k-perfect hash functions are surprisingly rare, and the area has not seen a lot of research recently. At the same time, recent research in 1-perfect hashing shows that there is a lack of efficient kPHFs. In this paper, we revive the area of k-perfect hashing, presenting four new constructions. Our implementations simultaneously dominate older approaches in space consumption, construction time, and query time. We see this paper as a possible starting point of an active line of research, similar to the area of 1-perfect hashing.

Cite as

Stefan Hermann, Sebastian Kirmayer, Hans-Peter Lehmann, Peter Sanders, and Stefan Walzer. Engineering Minimal k-Perfect Hash Functions. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 99:1-99:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{hermann_et_al:LIPIcs.ESA.2025.99,
  author =	{Hermann, Stefan and Kirmayer, Sebastian and Lehmann, Hans-Peter and Sanders, Peter and Walzer, Stefan},
  title =	{{Engineering Minimal k-Perfect Hash Functions}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{99:1--99: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.99},
  URN =		{urn:nbn:de:0030-drops-245685},
  doi =		{10.4230/LIPIcs.ESA.2025.99},
  annote =	{Keywords: Compressed Data Structures, Perfect Hashing}
}
Document
A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching

Authors: Joshua M. Cohen

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


Abstract
Algebraic data types (ADTs) and pattern matching are widely used to write elegant functional programs and to specify program behavior. These constructs are critical to most general-purpose interactive theorem provers (e.g. Lean, Rocq/Coq), first-order SMT-based deductive verifiers (e.g. Dafny, VeriFast), and intermediate verification languages (e.g. Why3). Such features require layers of compilation - in Rocq, pattern matches are compiled to remove nesting, while SMT-based tools further axiomatize ADTs with a first-order specification. However, these critical steps have been omitted from prior formalizations of such toolchains (e.g. MetaRocq). We give the first proved-sound sophisticated pattern matching compiler (based on Maranget’s compilation to decision trees) and first-order axiomatization of ADTs, both based on Why3 implementations. We prove the soundness of exhaustiveness checking, extending pen-and-paper proofs from the literature, and formulate a robustness property with which we find an exhaustiveness-related bug in Why3. We show that many of our proofs could be useful for reasoning about any first-order program verifier supporting ADTs.

Cite as

Joshua M. Cohen. A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{cohen:LIPIcs.ITP.2025.5,
  author =	{Cohen, Joshua M.},
  title =	{{A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{5:1--5:20},
  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.5},
  URN =		{urn:nbn:de:0030-drops-246046},
  doi =		{10.4230/LIPIcs.ITP.2025.5},
  annote =	{Keywords: Pattern Matching Compilation, Algebraic Data Types, First-Order Logic}
}
Document
Navigating Exoplanetary Systems in Augmented Reality: Preliminary Insights on ExoAR

Authors: Bryson Lawton, Frank Maurer, and Daniel Zielasko

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)


Abstract
With thousands of exoplanets now confirmed by space missions such as NASA’s Kepler and TESS, scientific interest and public curiosity about these distant worlds continue to grow. However, current visualization tools for exploring exoplanetary systems often lack sufficient scientific accuracy or interactive features, limiting their educational effectiveness and analytical utility. To help address this gap, we developed ExoAR, an augmented reality tool designed to offer immersive, scientifically sound visualizations of all known exoplanetary systems using data directly sourced from NASA’s Exoplanet Archive. By leveraging augmented reality’s strengths, ExoAR enables users to immerse themselves in interactive, dynamic 3D models of these planetary systems with data-driven representations of planets and their host stars. The application also allows users to adjust various visualization scales independently, a capability designed to aid comprehension of comparative astronomical properties such as orbital mechanics, planetary sizes, and stellar classifications. To begin assessing ExoAR’s potential as an educational and analytical tool and inform future iterations, a pilot user study was conducted. Its findings indicate that participants found ExoAR improved user engagement and spatial understanding compared to NASA’s Eyes on Exoplanets application, a non-immersive exoplanetary system visualization tool. This work-in-progress paper presents these early insights, acknowledges current system limitations, and outlines future directions for more rigorously evaluating and further improving ExoAR’s capabilities for both educational and scientific communities.

Cite as

Bryson Lawton, Frank Maurer, and Daniel Zielasko. Navigating Exoplanetary Systems in Augmented Reality: Preliminary Insights on ExoAR. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 20:1-20:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{lawton_et_al:OASIcs.SpaceCHI.2025.20,
  author =	{Lawton, Bryson and Maurer, Frank and Zielasko, Daniel},
  title =	{{Navigating Exoplanetary Systems in Augmented Reality: Preliminary Insights on ExoAR}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{20:1--20:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.20},
  URN =		{urn:nbn:de:0030-drops-240106},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.20},
  annote =	{Keywords: Immersive Analytics, Data Visualization, Astronomy, Astrophysics, Exoplanet, Augmented Reality, AR}
}
Document
Movement in Low Gravity (MoLo) – LUNA: Biomechanical Modelling to Mitigate Lunar Surface Operation Risks

Authors: David Andrew Green

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)


Abstract
The Artemis programme seeks to develop and test concepts, hardware and approaches to support long term habitation of the Lunar surface, and future missions to Mars. In preparation for the Artemis missions determination of tasks to be performed, the functional requirements of such tasks and as mission duration extends whether physiological deconditioning becomes functionally significant, compromising the crew member’s ability to perform critical tasks on the surface, and/or upon return to earth [MoLo-LUNA – leveraging the Molo programme (and several other activities) - could become a key supporting activity for LUNA incl. validation of the Puppeteer offloading system itself via creation of a complementary MoLo-LUNA-LAB. Furthermore, the MoLo-LUNA programme could become a key facilitator of simulator suit instrumentation/definition, broader astronaut training activities and mission architecture development – including Artemis mission simulations. By employing a Puppeteer system external to the LUNA chamber hall it will optimise utilisation and cost-effectiveness of LUNA, and as such represents a critical service to future LUNA stakeholders. Furthermore, MoLo-LUNA would generate a unique data set that can be leveraged to predict de-conditioning on the Lunar surface - and thereby optimise functionality, and minimise mission risk – including informing the need for, and prescription of exercise countermeasures on the Lunar Surface and in transit. Thus, MoLo-LUNA offers a unique opportunity to place LUNA, and ESA as a key ongoing provider of evidence to define, optimise and support crew Artemis surface missions.

Cite as

David Andrew Green. Movement in Low Gravity (MoLo) – LUNA: Biomechanical Modelling to Mitigate Lunar Surface Operation Risks. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 26:1-26:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{green:OASIcs.SpaceCHI.2025.26,
  author =	{Green, David Andrew},
  title =	{{Movement in Low Gravity (MoLo) – LUNA: Biomechanical Modelling to Mitigate Lunar Surface Operation Risks}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{26:1--26:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.26},
  URN =		{urn:nbn:de:0030-drops-240166},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.26},
  annote =	{Keywords: Locomotion, hypogravity, modelling, Lunar}
}
Document
RANDOM
Density Frankl–Rödl on the Sphere

Authors: Venkatesan Guruswami and Shilun Li

Published in: LIPIcs, Volume 353, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)


Abstract
We establish a density variant of the Frankl–Rödl theorem on the sphere 𝕊^{n-1}, which concerns avoiding pairs of vectors with a specific distance, or equivalently, a prescribed inner product. In particular, we establish lower bounds on the probability that a randomly chosen pair of such vectors lies entirely within a measurable subset A ⊆ 𝕊^{n-1} of sufficiently large measure. Additionally, we prove a density version of spherical avoidance problems, which generalize from pairwise avoidance to broader configurations with prescribed pairwise inner products. Our framework encompasses a class of configurations we call inductive configurations, which include simplices with any prescribed inner product -1 < r < 1. As a consequence of our density statement, we show that all inductive configurations are sphere Ramsey.

Cite as

Venkatesan Guruswami and Shilun Li. Density Frankl–Rödl on the Sphere. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 353, pp. 44:1-44:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{guruswami_et_al:LIPIcs.APPROX/RANDOM.2025.44,
  author =	{Guruswami, Venkatesan and Li, Shilun},
  title =	{{Density Frankl–R\"{o}dl on the Sphere}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)},
  pages =	{44:1--44:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-397-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{353},
  editor =	{Ene, Alina and Chattopadhyay, Eshan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2025.44},
  URN =		{urn:nbn:de:0030-drops-244108},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2025.44},
  annote =	{Keywords: Frankl–R\"{o}dl, Sphere Ramsey, Sphere Avoidance, Reverse Hypercontractivity, Forbidden Angles}
}
Document
On the Enumeration of Signatures of XOR-CNF’s

Authors: Nadia Creignou, Oscar Defrain, Frédéric Olive, and Simon Vilmin

Published in: LIPIcs, Volume 349, 19th International Symposium on Algorithms and Data Structures (WADS 2025)


Abstract
Given a CNF formula φ with clauses C_1, … , C_m over a set of variables V, a truth assignment 𝐚: V → {0, 1} generates a binary sequence σ_φ(𝐚) = (C_1(𝐚), …, C_m(𝐚)), called a signature of φ, where C_i(𝐚) = 1 if clause C_i evaluates to 1 under assignment 𝐚, and C_i(𝐚) = 0 otherwise. Signatures and their associated generation problems have given rise to new yet promising research questions in algorithmic enumeration. In a recent paper, Bérczi et al. interestingly proved that generating signatures of a CNF is tractable despite the fact that verifying a solution is hard. They also showed the hardness of finding maximal signatures of an arbitrary CNF due to the intractability of satisfiability in general. Their contribution leaves open the problem of efficiently generating maximal signatures for tractable classes of CNFs, i.e., those for which satisfiability can be solved in polynomial time. Stepping into that direction, we completely characterize the complexity of generating all, minimal, and maximal signatures for XOR-CNF’s.

Cite as

Nadia Creignou, Oscar Defrain, Frédéric Olive, and Simon Vilmin. On the Enumeration of Signatures of XOR-CNF’s. In 19th International Symposium on Algorithms and Data Structures (WADS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 349, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{creignou_et_al:LIPIcs.WADS.2025.19,
  author =	{Creignou, Nadia and Defrain, Oscar and Olive, Fr\'{e}d\'{e}ric and Vilmin, Simon},
  title =	{{On the Enumeration of Signatures of XOR-CNF’s}},
  booktitle =	{19th International Symposium on Algorithms and Data Structures (WADS 2025)},
  pages =	{19:1--19:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-398-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{349},
  editor =	{Morin, Pat and Oh, Eunjin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WADS.2025.19},
  URN =		{urn:nbn:de:0030-drops-242508},
  doi =		{10.4230/LIPIcs.WADS.2025.19},
  annote =	{Keywords: Algorithmic enumeration, XOR-CNF, signatures, maximal bipartite subgraphs enumeration, extension, proximity search}
}
Document
Broadcasting Under Structural Restrictions

Authors: Yudai Egami, Tatsuya Gima, Tesshu Hanaka, Yasuaki Kobayashi, Michael Lampis, Valia Mitsou, Edouard Nemery, Yota Otachi, Manolis Vasilakis, and Daniel Vaz

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)


Abstract
In the Telephone Broadcast problem we are given a graph G = (V,E) with a designated source vertex s ∈ V. Our goal is to transmit a message, which is initially known only to s, to all vertices of the graph by using a process where in each round an informed vertex may transmit the message to one of its uninformed neighbors. The optimization objective is to minimize the number of rounds. Following up on several recent works, we investigate the structurally parameterized complexity of Telephone Broadcast. In particular, we first strengthen existing NP-hardness results by showing that the problem remains NP-complete on graphs of bounded tree-depth and also on cactus graphs which are one vertex deletion away from being path forests. Motivated by this (severe) hardness, we study several other parameterizations of the problem and obtain FPT algorithms parameterized by vertex integrity (generalizing a recent FPT algorithm parameterized by vertex cover by Fomin, Fraigniaud, and Golovach [TCS 2024]) and by distance to clique, as well as FPT approximation algorithms parameterized by clique-cover and cluster vertex deletion. Furthermore, we obtain structural results that relate the length of the optimal broadcast protocol of a graph G with its pathwidth and tree-depth. By presenting a substantial improvement over the best previously known bound for pathwidth (Aminian, Kamali, Seyed-Javadi, and Sumedha [ICALP 2025]) we exponentially improve the approximation ratio achievable in polynomial time on graphs of bounded pathwidth from 𝒪(4^pw) to 𝒪(pw).

Cite as

Yudai Egami, Tatsuya Gima, Tesshu Hanaka, Yasuaki Kobayashi, Michael Lampis, Valia Mitsou, Edouard Nemery, Yota Otachi, Manolis Vasilakis, and Daniel Vaz. Broadcasting Under Structural Restrictions. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 42:1-42:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{egami_et_al:LIPIcs.MFCS.2025.42,
  author =	{Egami, Yudai and Gima, Tatsuya and Hanaka, Tesshu and Kobayashi, Yasuaki and Lampis, Michael and Mitsou, Valia and Nemery, Edouard and Otachi, Yota and Vasilakis, Manolis and Vaz, Daniel},
  title =	{{Broadcasting Under Structural Restrictions}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{42:1--42:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.42},
  URN =		{urn:nbn:de:0030-drops-241492},
  doi =		{10.4230/LIPIcs.MFCS.2025.42},
  annote =	{Keywords: Parameterized Complexity, Structural Graph Parameters, Telephone Broadcast}
}
Document
Cops and Robbers for Graphs on Surfaces with Crossings

Authors: Prosenjit Bose, Pat Morin, and Karthik Murali

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)


Abstract
Cops and Robbers is a game played on a graph where a set of cops attempt to capture a single robber. The game proceeds in rounds, where each round first consists of the cops' turn, followed by the robber’s turn. In the first round, the cops place themselves on a subset of vertices, after which the robber chooses a vertex to place himself. From the next round onwards, in the cops' turn, every cop can choose to either stay on the same vertex or move to an adjacent vertex, and likewise the robber in his turn. The robber is considered to be captured if, at any point in time, there is some cop on the same vertex as the robber. The cops win if they can capture the robber within a finite number of rounds; else the robber wins. A natural question in this game concerns the cop-number of a graph - the minimum number of cops needed to capture a robber. It has long been known that graphs embeddable (without crossings) on surfaces of bounded genus have bounded cop-number. In contrast, it was shown recently that the class of 1-planar graphs - graphs that can be drawn on the plane with at most one crossing per edge - does not have bounded cop-number. This paper initiates an investigation into how the distance between crossing pairs of edges influences a graph’s cop number. In particular, we look at Distance d Cops and Robbers, a variant of the classical game, where the robber is considered to be captured if there is a cop within distance d of the robber. Let c_d(G) denote the minimum number of cops required in the graph G to capture a robber within distance d. We look at various classes of graphs, such as 1-plane graphs, k-plane graphs (graphs where each edge is crossed at most k times), and even general graph drawings, and show that if every crossing pair of edges can be connected by a path of small length, then c_d(G) is bounded, for small values of d. For example, we show that if a graph G admits a drawing in which every pair of crossing edges is contained in a path of length at most 3, then c₄(G) ≤ 21. And if the drawing permits a stronger assumption that the endpoints of every crossing induce the complete graph K₄, then c₃(G) ≤ 9. The tools and techniques that we develop in this paper are sufficiently general, enabling us to examine graphs drawn not only on the sphere but also on orientable and non-orientable surfaces.

Cite as

Prosenjit Bose, Pat Morin, and Karthik Murali. Cops and Robbers for Graphs on Surfaces with Crossings. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{bose_et_al:LIPIcs.MFCS.2025.27,
  author =	{Bose, Prosenjit and Morin, Pat and Murali, Karthik},
  title =	{{Cops and Robbers for Graphs on Surfaces with Crossings}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{27:1--27:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.27},
  URN =		{urn:nbn:de:0030-drops-241349},
  doi =		{10.4230/LIPIcs.MFCS.2025.27},
  annote =	{Keywords: Cops and Robbers, Crossings, 1-Planar, Surfaces}
}
  • Refine by Type
  • 83 Document/PDF
  • 51 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 48 2025
  • 3 2024
  • 3 2023
  • 1 2022
  • 1 2020
  • Show More...

  • Refine by Author
  • 8 Müller, Peter
  • 5 Müller, Heinrich
  • 5 Seidel, Hans-Peter
  • 4 Gross, Markus
  • 4 Müller, Rudolf
  • Show More...

  • Refine by Series/Journal
  • 48 LIPIcs
  • 9 OASIcs
  • 4 LITES
  • 3 TGDK
  • 2 DagRep
  • Show More...

  • Refine by Classification
  • 6 Theory of computation → Graph algorithms analysis
  • 6 Theory of computation → Logic and verification
  • 4 Theory of computation → Parameterized complexity and exact algorithms
  • 2 Computer systems organization → Real-time systems
  • 2 Computing methodologies → Artificial intelligence
  • Show More...

  • Refine by Keyword
  • 3 Mechanism Design
  • 3 parameterized algorithms
  • 2 3D acquisition and display
  • 2 3D reconstruction
  • 2 Behavioral Economics
  • 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