39 Search Results for "Schweitzer, Pascal"

Document
Survey
DOI: 10.4230/TGDK.3.2.1
Resilience in Knowledge Graph Embeddings

Authors: Arnab Sharma, N'Dah Jean Kouagou, and Axel-Cyrille Ngonga Ngomo

Published in: TGDK, Volume 3, Issue 2 (2025). Transactions on Graph Data and Knowledge, Volume 3, Issue 2

Abstract
In recent years, knowledge graphs have gained interest and witnessed widespread applications in various domains, such as information retrieval, question-answering, recommendation systems, amongst others. Large-scale knowledge graphs to this end have demonstrated their utility in effectively representing structured knowledge. To further facilitate the application of machine learning techniques, knowledge graph embedding models have been developed. Such models can transform entities and relationships within knowledge graphs into vectors. However, these embedding models often face challenges related to noise, missing information, distribution shift, adversarial attacks, etc. This can lead to sub-optimal embeddings and incorrect inferences, thereby negatively impacting downstream applications. While the existing literature has focused so far on adversarial attacks on KGE models, the challenges related to the other critical aspects remain unexplored. In this paper, we, first of all, give a unified definition of resilience, encompassing several factors such as generalisation, in-distribution generalization, distribution adaption, and robustness. After formalizing these concepts for machine learning in general, we define them in the context of knowledge graphs. To find the gap in the existing works on resilience in the context of knowledge graphs, we perform a systematic survey, taking into account all these aspects mentioned previously. Our survey results show that most of the existing works focus on a specific aspect of resilience, namely robustness. After categorizing such works based on their respective aspects of resilience, we discuss the challenges and future research directions.
Cite as

Arnab Sharma, N'Dah Jean Kouagou, and Axel-Cyrille Ngonga Ngomo. Resilience in Knowledge Graph Embeddings. In Transactions on Graph Data and Knowledge (TGDK), Volume 3, Issue 2, pp. 1:1-1:38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{sharma_et_al:TGDK.3.2.1,
  author =	{Sharma, Arnab and Kouagou, N'Dah Jean and Ngomo, Axel-Cyrille Ngonga},
  title =	{{Resilience in Knowledge Graph Embeddings}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{1:1--1:38},
  ISSN =	{2942-7517},
  year =	{2025},
  volume =	{3},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.3.2.1},
  URN =		{urn:nbn:de:0030-drops-248117},
  doi =		{10.4230/TGDK.3.2.1},
  annote =	{Keywords: Knowledge graphs, Resilience, Robustness}
}
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
DOI: 10.4230/LIPIcs.MFCS.2025.88
Color Refinement for Relational Structures

Authors: Benjamin Scheidt and Nicole Schweikardt

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

Abstract
Color Refinement, also known as Naive Vertex Classification, is a classical method to distinguish graphs by iteratively computing a coloring of their vertices. While it is traditionally used as an imperfect way to test for isomorphism, the algorithm has permeated many other, seemingly unrelated, areas of computer science. The method is algorithmically simple, and it has a well-understood distinguishing power: it has been logically characterized by Immerman and Lander (1990) and Cai, Fürer, Immerman (1992), who showed that it distinguishes precisely those graphs that can be distinguished by a sentence of first-order logic with counting quantifiers and only two variables. A combinatorial characterization was given by Dvořák (2010), who showed that it distinguishes precisely those graphs that differ in the number of homomorphisms from some tree. In this paper, we introduce Relational Color Refinement (RCR, for short), a generalization of the Color Refinement method from graphs to arbitrary relational structures, whose distinguishing power admits the equivalent combinatorial and logical characterizations as Color Refinement has on graphs: we show that RCR distinguishes precisely those structures that differ in the number of homomorphisms from an acyclic connected relational structure. Further, we show that RCR distinguishes precisely those structures that are distinguished by a sentence of the guarded fragment of first-order logic with counting quantifiers. Additionally, we show that for every fixed finite relational signature, RCR can be implemented to run on structures of that signature in time O(N⋅log N), where N denotes the number of tuples present in the structure.
Cite as

Benjamin Scheidt and Nicole Schweikardt. Color Refinement for Relational Structures. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 88:1-88:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{scheidt_et_al:LIPIcs.MFCS.2025.88,
  author =	{Scheidt, Benjamin and Schweikardt, Nicole},
  title =	{{Color Refinement for Relational Structures}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{88:1--88:19},
  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.88},
  URN =		{urn:nbn:de:0030-drops-241958},
  doi =		{10.4230/LIPIcs.MFCS.2025.88},
  annote =	{Keywords: color refinement, counting logics, homomorphism counts, homomorphism indistinguishability, guarded logics, pebble games, relational structures, alpha-acyclicity, join-trees}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.89
Homomorphism Indistinguishability and Game Comonads for Restricted Conjunction and Requantification

Authors: Georg Schindling

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

Abstract
The notion of homomorphism indistinguishability offers a combinatorial framework for characterizing equivalence relations of graphs, in particular equivalences in counting logics within finite model theory. That is, for certain graph classes, two structures agree on all homomorphism counts from the class if and only if they satisfy the same sentences in a corresponding logic. This perspective often reveals connections between the combinatorial properties of graph classes and the syntactic structure of logical fragments. In this work, we extend this perspective to logics with restricted requantification, refining the stratification of logical resources in finite-variable counting logics. Specifically, we generalize Lovász-type theorems for these logics with either restricted conjunction or bounded quantifier-rank and present new combinatorial proofs of existing results. To this end, we introduce novel path and tree decompositions that incorporate the concept of reusability and develop characterizations based on pursuit-evasion games. Leveraging this framework, we establish that classes of bounded pathwidth and treewidth with reusability constraints are homomorphism distinguishing closed. Finally, we develop a comonadic perspective on requantification by constructing new comonads that encapsulate restricted-reusability pebble games. We show a tight correspondence between their coalgebras and path/tree decompositions, yielding categorical characterizations of reusability in graph decompositions. This unifies logical, combinatorial, and categorical perspectives on the notion of reusability.
Cite as

Georg Schindling. Homomorphism Indistinguishability and Game Comonads for Restricted Conjunction and Requantification. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 89:1-89:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schindling:LIPIcs.MFCS.2025.89,
  author =	{Schindling, Georg},
  title =	{{Homomorphism Indistinguishability and Game Comonads for Restricted Conjunction and Requantification}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{89:1--89:19},
  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.89},
  URN =		{urn:nbn:de:0030-drops-241962},
  doi =		{10.4230/LIPIcs.MFCS.2025.89},
  annote =	{Keywords: homomorphism indistinguishability, game comonads, finite variable counting logic, restricted conjunction, restricted requantification, tree decomposition, path decomposition}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.18
Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism

Authors: Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth

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

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

Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth. Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.MFCS.2025.18,
  author =	{Berkholz, Christoph and Lichter, Moritz and Vinall-Smeeth, Harry},
  title =	{{Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{18:1--18:19},
  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.18},
  URN =		{urn:nbn:de:0030-drops-241253},
  doi =		{10.4230/LIPIcs.MFCS.2025.18},
  annote =	{Keywords: Proof complexity, Resolution, Width, Tree-like size, Supercritical trade-off, Lower bound, Finite model theory, CFI graphs}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.7
Temporal Explorability Games

Authors: Pete Austin, Sougata Bose, Nicolas Mazzocchi, and Patrick Totzke

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Temporal graphs extend ordinary graphs with discrete time that affects the availability of edges. We consider solving games played on temporal graphs where one player aims to explore the graph, i.e., visit all vertices. The complexity depends majorly on two factors: the presence of an adversary and how edge availability is specified. We demonstrate that on static graphs, where edges are always available, solving explorability games is just as hard as solving reachability games. In contrast, on temporal graphs, the complexity of explorability coincides with generalized reachability (NP-complete for one-player and PSPACE-complete for two player games). We show that if temporal graphs are given symbolically, even one-player reachability (and thus explorability and generalized reachability) games are PSPACE-hard. For one player, all these are also solvable in PSPACE and for two players, they are in PSPACE, EXP and EXP, respectively.
Cite as

Pete Austin, Sougata Bose, Nicolas Mazzocchi, and Patrick Totzke. Temporal Explorability Games. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{austin_et_al:LIPIcs.CONCUR.2025.7,
  author =	{Austin, Pete and Bose, Sougata and Mazzocchi, Nicolas and Totzke, Patrick},
  title =	{{Temporal Explorability Games}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{7:1--7:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.7},
  URN =		{urn:nbn:de:0030-drops-239575},
  doi =		{10.4230/LIPIcs.CONCUR.2025.7},
  annote =	{Keywords: Temporal Graphs, Explorability, Reachability, Games}
}
Document
DOI: 10.4230/LIPIcs.WABI.2025.12
Extension of Partial Atom-To-Atom Maps: Uniqueness and Algorithms

Authors: Marcos E. González Laffitte, Tieu-Long Phan, and Peter F. Stadler

Published in: LIPIcs, Volume 344, 25th International Conference on Algorithms for Bioinformatics (WABI 2025)

Abstract
Chemical reaction databases typically report the molecular structures of reactant and product compounds, as well as their stoichiometry, but lack information, in particular, on the correspondence of reactant and product atoms. These atom-to-atom maps (AAM), however, are crucial for applications including chemical synthesis planning in organic chemistry and the analysis of isotope labeling experiments in modern metabolomics. AAMs therefore need to be reconstructed computationally. This situation is aggravated, furthermore, by the fact that chemically correct AAMs are, fundamentally, determined by quantum-mechanical phenomena and thus cannot be reliably computed by solving graph-theoretical optimization problems defined by the reactant and product structures. A viable solution for this problem is to shift the focus into first identifying a partial AAM containing the reaction center, i.e., covering the atoms incident with all bonds that change during a reaction. This then leads to the problem of extending the partial map to the full reaction. The AAM of a reaction is faithfully represented by the Imaginary Transition State (ITS) graph, providing a convenient graph-theoretic framework to address the questions of when and how a partial AAM can be extended. We show that an unique extension exists whenever, and only if, these partial AAMs cover the reaction center. In this case their extension can be computed by solving a constrained graph-isomorphism search between specific subgraphs of ITS graphs. We close by benchmarking different tools for this task.
Cite as

Marcos E. González Laffitte, Tieu-Long Phan, and Peter F. Stadler. Extension of Partial Atom-To-Atom Maps: Uniqueness and Algorithms. In 25th International Conference on Algorithms for Bioinformatics (WABI 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 344, pp. 12:1-12:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gonzalezlaffitte_et_al:LIPIcs.WABI.2025.12,
  author =	{Gonz\'{a}lez Laffitte, Marcos E. and Phan, Tieu-Long and Stadler, Peter F.},
  title =	{{Extension of Partial Atom-To-Atom Maps: Uniqueness and Algorithms}},
  booktitle =	{25th International Conference on Algorithms for Bioinformatics (WABI 2025)},
  pages =	{12:1--12:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-386-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{344},
  editor =	{Brejov\'{a}, Bro\v{n}a and Patro, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2025.12},
  URN =		{urn:nbn:de:0030-drops-239410},
  doi =		{10.4230/LIPIcs.WABI.2025.12},
  annote =	{Keywords: atom-to-atom maps, imaginary transition state (ITS) graphs, condensed graph of the reaction (CGR), chemical reaction mechanisms, molecular graphs, metabolic networks, chemical synthesis planning, constrained graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.15
Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets

Authors: Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
We propose symmetric core learning (SCL) as a novel approach to making the implicit hitting set approach (IHS) to constraint optimization more symmetry-aware. SCL has the potential of significantly reducing the number of iterations and, in particular, the number of calls to an NP decision solver for extracting individual unsatisfiable cores. As the technique is focused on generating symmetric cores to the hitting set component of IHS, SCL is generally applicable in IHS-style search for essentially any constraint optimization paradigm. In this work, we focus in particular on integrating SCL to IHS for pseudo-Boolean optimization (PBO), as earlier proposed static symmetry breaking through lex-leader constraints generated before search turns out to often degrade the performance of the IHS approach to PBO. In contrast, we show that SCL can improve the runtime performance of a state-of-the-art IHS approach to PBO and generally does not impose significant overhead in terms of runtime performance.
Cite as

Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts. Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 15:1-15:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ihalainen_et_al:LIPIcs.CP.2025.15,
  author =	{Ihalainen, Hannes and Berg, Jeremias and J\"{a}rvisalo, Matti and Bogaerts, Bart},
  title =	{{Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{15:1--15:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.15},
  URN =		{urn:nbn:de:0030-drops-238767},
  doi =		{10.4230/LIPIcs.CP.2025.15},
  annote =	{Keywords: Implicit hitting sets, symmetries, unsatisfiable cores, pseudo-Boolean optimization}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.32
Efficient Certified Reasoning for Binarized Neural Networks

Authors: Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Neural networks have emerged as essential components in safety-critical applications - these use cases demand complex, yet trustworthy computations. Binarized Neural Networks (BNNs) are a type of neural network where each neuron is constrained to a Boolean value; they are particularly well-suited for safety-critical tasks because they retain much of the computational capacities of full-scale (floating-point or quantized) deep neural networks, but remain compatible with satisfiability solvers for qualitative verification and with model counters for quantitative reasoning. However, existing methods for BNN analysis suffer from either limited scalability or susceptibility to soundness errors, which hinders their applicability in real-world scenarios. In this work, we present a scalable and trustworthy approach for both qualitative and quantitative verification of BNNs. Our approach introduces a native representation of BNN constraints in a custom-designed solver for qualitative reasoning, and in an approximate model counter for quantitative reasoning. We further develop specialized proof generation and checking pipelines with native support for BNN constraint reasoning, ensuring trustworthiness for all of our verification results. Empirical evaluations on a BNN robustness verification benchmark suite demonstrate that our certified solving approach achieves a 9× speedup over prior certified CNF and PB-based approaches, and our certified counting approach achieves a 218× speedup over the existing CNF-based baseline. In terms of coverage, our pipeline produces fully certified results for 99% and 86% of the qualitative and quantitative reasoning queries on BNNs, respectively. This is in sharp contrast to the best existing baselines which can fully certify only 62% and 4% of the queries, respectively.
Cite as

Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel. Efficient Certified Reasoning for Binarized Neural Networks. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.SAT.2025.32,
  author =	{Yang, Jiong and Tan, Yong Kiam and Soos, Mate and Myreen, Magnus O. and Meel, Kuldeep S.},
  title =	{{Efficient Certified Reasoning for Binarized Neural Networks}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.32},
  URN =		{urn:nbn:de:0030-drops-237665},
  doi =		{10.4230/LIPIcs.SAT.2025.32},
  annote =	{Keywords: Neural network verification, proof certification, SAT solving, approximate model counting}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.129
An Upper Bound on the Weisfeiler-Leman Dimension

Authors: Thomas Schneider and Pascal Schweitzer

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
The Weisfeiler-Leman (WL) algorithms form a family of incomplete approaches to the graph isomorphism problem. They recently found various applications in algorithmic group theory and machine learning. In fact, the algorithms form a parameterized family: for each k ∈ ℕ there is a corresponding k-dimensional algorithm WLk. The algorithms become increasingly powerful with increasing dimension, but at the same time the running time increases. The WL-dimension of a graph G is the smallest k ∈ ℕ for which WLk correctly decides isomorphism between G and every other graph. In some sense, the WL-dimension measures how difficult it is to test isomorphism of one graph to others using a fairly general class of combinatorial algorithms. Nowadays, it is a standard measure in descriptive complexity theory for the structural complexity of a graph. We prove that the WL-dimension of a graph on n vertices is at most 3/20 ⋅ n + o(n) = 0.15 ⋅ n + o(n). Reducing the question to coherent configurations, the proof develops various techniques to analyze their structure. This includes sufficient conditions under which a fiber can be restored uniquely up to isomorphism if it is removed, a recursive proof exploiting a degree reduction and treewidth bounds, as well as an exhaustive analysis of interspaces involving small fibers. As a base case, we also analyze the dimension of coherent configurations with small fiber size and thereby graphs with small color class size.
Cite as

Thomas Schneider and Pascal Schweitzer. An Upper Bound on the Weisfeiler-Leman Dimension. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 129:1-129:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schneider_et_al:LIPIcs.ICALP.2025.129,
  author =	{Schneider, Thomas and Schweitzer, Pascal},
  title =	{{An Upper Bound on the Weisfeiler-Leman Dimension}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{129:1--129:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.129},
  URN =		{urn:nbn:de:0030-drops-235065},
  doi =		{10.4230/LIPIcs.ICALP.2025.129},
  annote =	{Keywords: Weisfeiler-Leman dimension, descriptive complexity, coherent configurations}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.123
New and Improved Bounds for Markov Paging

Authors: Chirag Pabbaraju and Ali Vakilian

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
In the Markov paging model, one assumes that page requests are drawn from a Markov chain over the pages in memory, and the goal is to maintain a fast cache that suffers few page faults in expectation. While computing the optimal online algorithm (OPT) for this problem naively takes time exponential in the size of the cache, the best-known polynomial-time approximation algorithm is the dominating distribution algorithm due to Lund, Phillips and Reingold (FOCS 1994), who showed that the algorithm is 4-competitive against OPT. We substantially improve their analysis and show that the dominating distribution algorithm is in fact 2-competitive against OPT. We also show a lower bound of 1.5907-competitiveness for this algorithm - to the best of our knowledge, no such lower bound was previously known.
Cite as

Chirag Pabbaraju and Ali Vakilian. New and Improved Bounds for Markov Paging. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 123:1-123:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{pabbaraju_et_al:LIPIcs.ICALP.2025.123,
  author =	{Pabbaraju, Chirag and Vakilian, Ali},
  title =	{{New and Improved Bounds for Markov Paging}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{123:1--123:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.123},
  URN =		{urn:nbn:de:0030-drops-235005},
  doi =		{10.4230/LIPIcs.ICALP.2025.123},
  annote =	{Keywords: Beyond Worst-case Analyis, Online Paging, Markov Paging}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2025.65
Recognizing 2-Layer and Outer k-Planar Graphs

Authors: Yasuaki Kobayashi, Yuto Okada, and Alexander Wolff

Published in: LIPIcs, Volume 332, 41st International Symposium on Computational Geometry (SoCG 2025)

Abstract
The crossing number of a graph is the least number of crossings over all drawings of the graph in the plane. Computing the crossing number of a given graph is NP-hard, but fixed-parameter tractable (FPT) with respect to the natural parameter. Two well-known variants of the problem are 2-layer crossing minimization and circular crossing minimization, where every vertex must lie on one of two layers, namely two parallel lines, or a circle, respectively. In both cases, edges are drawn as straight-line segments. Both variants are NP-hard, but admit FPT-algorithms with respect to the natural parameter. In recent years, in the context of beyond-planar graphs, a local version of the crossing number has also received considerable attention. A graph is k-planar if it admits a drawing with at most k crossings per edge. In contrast to the crossing number, recognizing k-planar graphs is NP-hard even if k = 1 and hence not likely to be FPT with respect to the natural parameter k. In this paper, we consider the two above variants in the local setting. The k-planar graphs that admit a straight-line drawing with vertices on two layers or on a circle are called 2-layer k-planar and outer k-planar graphs, respectively. We study the parameterized complexity of the two recognition problems with respect to the natural parameter k. For k = 0, the two classes of graphs are exactly the caterpillars and outerplanar graphs, respectively, which can be recognized in linear time. Two groups of researchers independently showed that outer 1-planar graphs can also be recognized in linear time [Hong et al., Algorithmica 2015; Auer et al., Algorithmica 2016]. One group asked explicitly whether outer 2-planar graphs can be recognized in polynomial time. Our main contribution consists of XP-algorithms for recognizing 2-layer k-planar graphs and outer k-planar graphs, which implies that both recognition problems can be solved in polynomial time for every fixed k. We complement these results by showing that recognizing 2-layer k-planar graphs is XNLP-complete and that recognizing outer k-planar graphs is XNLP-hard. This implies that both problems are W[t]-hard for every t and that it is unlikely that they admit FPT-algorithms. On the other hand, we present an FPT-algorithm for recognizing 2-layer k-planar graphs where the order of the vertices on one layer is specified.
Cite as

Yasuaki Kobayashi, Yuto Okada, and Alexander Wolff. Recognizing 2-Layer and Outer k-Planar Graphs. In 41st International Symposium on Computational Geometry (SoCG 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 332, pp. 65:1-65:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kobayashi_et_al:LIPIcs.SoCG.2025.65,
  author =	{Kobayashi, Yasuaki and Okada, Yuto and Wolff, Alexander},
  title =	{{Recognizing 2-Layer and Outer k-Planar Graphs}},
  booktitle =	{41st International Symposium on Computational Geometry (SoCG 2025)},
  pages =	{65:1--65:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-370-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{332},
  editor =	{Aichholzer, Oswin and Wang, Haitao},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2025.65},
  URN =		{urn:nbn:de:0030-drops-232170},
  doi =		{10.4230/LIPIcs.SoCG.2025.65},
  annote =	{Keywords: 2-layer k-planar graphs, outer k-planar graphs, recognition algorithms, local crossing number, bandwidth, FPT, XNLP, XP, W\lbrackt\rbrack}
}
Document
DOI: 10.4230/LIPIcs.CPM.2025.5
Covers in Optimal Space

Authors: Itai Boneh and Shay Golan

Published in: LIPIcs, Volume 331, 36th Annual Symposium on Combinatorial Pattern Matching (CPM 2025)

Abstract
A cover of a string S is a string C such that every index of S is contained in some occurrence of C. First introduced by Apostolico and Ehrenfeucht [TCS'93] over 30 years ago, covers have since received significant attention in the string algorithms community. In this work, we present a space-efficient algorithm for computing a compact representation of all covers of a given string. Our algorithm requires only O(log n) additional memory while accessing the input string of length n in a read-only manner. Moreover, it runs in O(n) time, matching the best-known time complexity for this problem while achieving an exponential improvement in space usage.
Cite as

Itai Boneh and Shay Golan. Covers in Optimal Space. In 36th Annual Symposium on Combinatorial Pattern Matching (CPM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 331, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{boneh_et_al:LIPIcs.CPM.2025.5,
  author =	{Boneh, Itai and Golan, Shay},
  title =	{{Covers in Optimal Space}},
  booktitle =	{36th Annual Symposium on Combinatorial Pattern Matching (CPM 2025)},
  pages =	{5:1--5:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-369-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{331},
  editor =	{Bonizzoni, Paola and M\"{a}kinen, Veli},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CPM.2025.5},
  URN =		{urn:nbn:de:0030-drops-230993},
  doi =		{10.4230/LIPIcs.CPM.2025.5},
  annote =	{Keywords: Cover, Read-only random access, small space}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.75
Canonical Labeling of Sparse Random Graphs

Authors: Oleg Verbitsky and Maksim Zhukovskii

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
We show that if p = O(1/n), then the Erdős-Rényi random graph G(n,p) with high probability admits a canonical labeling computable in time O(nlog n). Combined with the previous results on the canonization of random graphs, this implies that G(n,p) with high probability admits a polynomial-time canonical labeling whatever the edge probability function p. Our algorithm combines the standard color refinement routine with simple post-processing based on the classical linear-time tree canonization. Noteworthy, our analysis of how well color refinement performs in this setting allows us to complete the description of the automorphism group of the 2-core of G(n,p).
Cite as

Oleg Verbitsky and Maksim Zhukovskii. Canonical Labeling of Sparse Random Graphs. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 75:1-75:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{verbitsky_et_al:LIPIcs.STACS.2025.75,
  author =	{Verbitsky, Oleg and Zhukovskii, Maksim},
  title =	{{Canonical Labeling of Sparse Random Graphs}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{75:1--75:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine 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.2025.75},
  URN =		{urn:nbn:de:0030-drops-229003},
  doi =		{10.4230/LIPIcs.STACS.2025.75},
  annote =	{Keywords: Graph isomorphism, random graphs, canonical labeling, color refinement}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.13
Computational Complexity of the Weisfeiler-Leman Dimension

Authors: Moritz Lichter, Simon Raßmann, and Pascal Schweitzer

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
The Weisfeiler-Leman dimension of a graph G is the least number k such that the k-dimensional Weisfeiler-Leman algorithm distinguishes G from every other non-isomorphic graph, or equivalently, the least k such that G is definable in (k+1)-variable first-order logic with counting. The dimension is a standard measure of the descriptive or structural complexity of a graph and recently finds various applications in particular in the context of machine learning. This paper studies the complexity of computing the Weisfeiler-Leman dimension. We observe that deciding whether the Weisfeiler-Leman dimension of G is at most k is NP-hard, even if G is restricted to have 4-bounded color classes. For each fixed k ≥ 2, we give a polynomial-time algorithm that decides whether the Weisfeiler-Leman dimension of a given graph with 5-bounded color classes is at most k. Moreover, we show that for these bounds on the color classes, this is optimal because the problem is PTIME-hard under logspace-uniform AC_0-reductions. Furthermore, for each larger bound c on the color classes and each fixed k ≥ 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.
Cite as

Moritz Lichter, Simon Raßmann, and Pascal Schweitzer. Computational Complexity of the Weisfeiler-Leman Dimension. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lichter_et_al:LIPIcs.CSL.2025.13,
  author =	{Lichter, Moritz and Ra{\ss}mann, Simon and Schweitzer, Pascal},
  title =	{{Computational Complexity of the Weisfeiler-Leman Dimension}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{13:1--13:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.13},
  URN =		{urn:nbn:de:0030-drops-227707},
  doi =		{10.4230/LIPIcs.CSL.2025.13},
  annote =	{Keywords: Weisfeiler-Leman algorithm, dimension, complexity, coherent configurations}
}
  • Refine by Type
  • 39 Document/PDF
  • 16 Document/HTML

  • Refine by Publication Year
  • 17 2025
  • 3 2023
  • 3 2022
  • 6 2021
  • 2 2020
  • Show More...

  • Refine by Author
  • 20 Schweitzer, Pascal
  • 7 Anders, Markus
  • 3 Lichter, Moritz
  • 2 Brachter, Jendrik
  • 2 Neuen, Daniel
  • Show More...

  • Refine by Series/Journal
  • 37 LIPIcs
  • 1 TGDK
  • 1 DagRep

  • Refine by Classification
  • 8 Mathematics of computing → Graph algorithms
  • 7 Theory of computation → Complexity theory and logic
  • 5 Mathematics of computing → Graph theory
  • 5 Theory of computation → Design and analysis of algorithms
  • 5 Theory of computation → Graph algorithms analysis
  • Show More...

  • Refine by Keyword
  • 10 graph isomorphism
  • 3 Graph isomorphism
  • 2 Graph Isomorphism
  • 2 Lower bounds
  • 2 Online algorithms
  • 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