108 Search Results for "Szeider, Stefan"

Volume

LIPIcs, Volume 241

47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

MFCS 2022, August 22-26, 2022, Vienna, Austria

Editors: Stefan Szeider, Robert Ganian, and Alexandra Silva

Document
DOI: 10.4230/LIPIcs.CP.2023.39
Searching for Smallest Universal Graphs and Tournaments with SAT

Authors: Tianwei Zhang and Stefan Szeider

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract
A graph is induced k-universal if it contains all graphs of order k as an induced subgraph. For over half a century, the question of determining smallest k-universal graphs has been studied. A related question asks for a smallest k-universal tournament containing all tournaments of order k. This paper proposes and compares SAT-based methods for answering these questions exactly for small values of k. Our methods scale to values for which a generate-and-test approach isn't feasible; for instance, we show that an induced 7-universal graph has more than 16 vertices, whereas the number of all connected graphs on 16 vertices, modulo isomorphism, is a number with 23 decimal digits Our methods include static and dynamic symmetry breaking and lazy encodings, employing external subgraph isomorphism testing.
Cite as

Tianwei Zhang and Stefan Szeider. Searching for Smallest Universal Graphs and Tournaments with SAT. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 39:1-39:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.CP.2023.39,
  author =	{Zhang, Tianwei and Szeider, Stefan},
  title =	{{Searching for Smallest Universal Graphs and Tournaments with SAT}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{39:1--39:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.39},
  URN =		{urn:nbn:de:0030-drops-190760},
  doi =		{10.4230/LIPIcs.CP.2023.39},
  annote =	{Keywords: Constrained-based combinatorics, synthesis problems, symmetry breaking, SAT solving, subgraph isomorphism, tournament, directed graphs}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2023.48
Proven Optimally-Balanced Latin Rectangles with SAT (Short Paper)

Authors: Vaidyanathan Peruvemba Ramaswamy and Stefan Szeider

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract
Motivated by applications from agronomic field experiments, Díaz, Le Bras, and Gomes [CPAIOR 2015] introduced Partially Balanced Latin Rectangles as a generalization of Spatially Balanced Latin Squares. They observed that the generation of Latin rectangles that are optimally balanced is a highly challenging computational problem. They computed, utilizing CSP and MIP encodings, Latin rectangles up to 12 × 12, some optimally balanced, some suboptimally balanced. In this paper, we develop a SAT encoding for generating balanced Latin rectangles. We compare experimentally encoding variants. Our results indicate that SAT encodings perform competitively with the MIP encoding, in some cases better. In some cases we could find Latin rectangles that are more balanced than previously known ones. This finding is significant, as there are many arithmetic constraints involved. The SAT approach offers the advantage that we can certify that Latin rectangles are optimally balanced through DRAT proofs that can be verified independently.
Cite as

Vaidyanathan Peruvemba Ramaswamy and Stefan Szeider. Proven Optimally-Balanced Latin Rectangles with SAT (Short Paper). In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 48:1-48:10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{peruvembaramaswamy_et_al:LIPIcs.CP.2023.48,
  author =	{Peruvemba Ramaswamy, Vaidyanathan and Szeider, Stefan},
  title =	{{Proven Optimally-Balanced Latin Rectangles with SAT}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{48:1--48:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.48},
  URN =		{urn:nbn:de:0030-drops-190855},
  doi =		{10.4230/LIPIcs.CP.2023.48},
  annote =	{Keywords: combinatorial design, SAT encodings, certified optimality, arithmetic constraints, spatially balanced Latin rectangles}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.8
IPASIR-UP: User Propagators for CDCL

Authors: Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
Modern SAT solvers are frequently embedded as sub-reasoning engines into more complex tools for addressing problems beyond the Boolean satisfiability problem. Examples include solvers for Satisfiability Modulo Theories (SMT), combinatorial optimization, model enumeration and counting. In such use cases, the SAT solver is often able to provide relevant information beyond the satisfiability answer. Further, domain knowledge of the embedding system (e.g., symmetry properties or theory axioms) can be beneficial for the CDCL search, but cannot be efficiently represented in clausal form. In this paper, we propose a general interface to inspect and influence the internal behaviour of CDCL SAT solvers. Our goal is to capture the most essential functionalities that are sufficient to simplify and improve use cases that require a more fine-grained interaction with the SAT solver than provided via the standard IPASIR interface. For our experiments, we extend CaDiCaL with our interface and evaluate it on two representative use cases: enumerating graphs within the SAT modulo Symmetries framework (SMS), and as the main CDCL(T) SAT engine of the SMT solver cvc5.
Cite as

Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: User Propagators for CDCL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 8:1-8:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{fazekas_et_al:LIPIcs.SAT.2023.8,
  author =	{Fazekas, Katalin and Niemetz, Aina and Preiner, Mathias and Kirchweger, Markus and Szeider, Stefan and Biere, Armin},
  title =	{{IPASIR-UP: User Propagators for CDCL}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{8:1--8:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.8},
  URN =		{urn:nbn:de:0030-drops-184709},
  doi =		{10.4230/LIPIcs.SAT.2023.8},
  annote =	{Keywords: SAT, CDCL, Satisfiability Modulo Theories, Satisfiability Modulo Symmetries}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.13
A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture

Authors: Markus Kirchweger, Tomáš Peitl, and Stefan Szeider

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
In 1972, Paul Erdős, Vance Faber, and Lászlo Lovász asked whether every linear hypergraph with n vertices can be edge-colored with n colors, a statement that has come to be known as the EFL conjecture. Erdős himself considered the conjecture as one of his three favorite open problems, and offered increasing money prizes for its solution on several occasions. A proof of the conjecture was recently announced, for all but a finite number of hypergraphs. In this paper we look at some of the cases not covered by this proof. We use SAT solvers, and in particular the SAT Modulo Symmetries (SMS) framework, to generate non-colorable linear hypergraphs with a fixed number of vertices and hyperedges modulo isomorphisms. Since hypergraph colorability is NP-hard, we cannot directly express in a propositional formula that we want only non-colorable hypergraphs. Instead, we use one SAT (SMS) solver to generate candidate hypergraphs modulo isomorphisms, and another to reject them by finding a coloring. Each successive candidate is required to defeat all previous colorings, whereby we avoid having to generate and test all linear hypergraphs. Computational methods have previously been used to verify the EFL conjecture for small hypergraphs. We verify and extend these results to larger values and discuss challenges and directions. Ours is the first computational approach to the EFL conjecture that allows producing independently verifiable, DRAT proofs.
Cite as

Markus Kirchweger, Tomáš Peitl, and Stefan Szeider. A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 13:1-13:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kirchweger_et_al:LIPIcs.SAT.2023.13,
  author =	{Kirchweger, Markus and Peitl, Tom\'{a}\v{s} and Szeider, Stefan},
  title =	{{A SAT Solver’s Opinion on the Erd\H{o}s-Faber-Lov\'{a}sz Conjecture}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.13},
  URN =		{urn:nbn:de:0030-drops-184752},
  doi =		{10.4230/LIPIcs.SAT.2023.13},
  annote =	{Keywords: hypergraphs, graph coloring, SAT modulo symmetries}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.14
SAT-Based Generation of Planar Graphs

Authors: Markus Kirchweger, Manfred Scheucher, and Stefan Szeider

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
To test a graph’s planarity in SAT-based graph generation we develop SAT encodings with dynamic symmetry breaking as facilitated in the SAT modulo Symmetry (SMS) framework. We implement and compare encodings based on three planarity criteria. In particular, we consider two eager encodings utilizing order-based and universal-set-based planarity criteria, and a lazy encoding based on Kuratowski’s theorem. The performance and scalability of these encodings are compared on two prominent problems from combinatorics: the computation of planar Turán numbers and the Earth-Moon problem. We further showcase the power of SMS equipped with a planarity encoding by verifying and extending several integer sequences from the Online Encyclopedia of Integer Sequences (OEIS) related to planar graph enumeration. Furthermore, we extend the SMS framework to directed graphs which might be of independent interest.
Cite as

Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. SAT-Based Generation of Planar Graphs. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 14:1-14:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kirchweger_et_al:LIPIcs.SAT.2023.14,
  author =	{Kirchweger, Markus and Scheucher, Manfred and Szeider, Stefan},
  title =	{{SAT-Based Generation of Planar Graphs}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.14},
  URN =		{urn:nbn:de:0030-drops-184767},
  doi =		{10.4230/LIPIcs.SAT.2023.14},
  annote =	{Keywords: SAT modulo Symmetry (SMS), dynamic symmetry breaking, planarity test, universal point set, order dimension, Schnyder’s theorem, Kuratowski’s theorem, Tur\'{a}n’s theorem, Earth-Moon problem}
}
Document
DOI: 10.4230/LIPIcs.SEA.2023.1
Engineering a Preprocessor for Symmetry Detection

Authors: Markus Anders, Pascal Schweitzer, and Julian Stieß

Published in: LIPIcs, Volume 265, 21st International Symposium on Experimental Algorithms (SEA 2023)

Abstract
State-of-the-art solvers for symmetry detection in combinatorial objects are becoming increasingly sophisticated software libraries. Most of the solvers were initially designed with inputs from combinatorics in mind (nauty, bliss, Traces, dejavu). They excel at dealing with a complicated core of the input. Others focus on practical instances that exhibit sparsity. They excel at dealing with comparatively easy but extremely large substructures of the input (saucy). In practice, these differences manifest in significantly diverging performances on different types of graph classes. We engineer a preprocessor for symmetry detection. The result is a tool designed to shrink sparse, large substructures of the input graph. On most of the practical instances, the preprocessor improves the overall running time significantly for many of the state-of-the-art solvers. At the same time, our benchmarks show that the additional overhead is negligible. Overall we obtain single algorithms with competitive performance across all benchmark graphs. As such, the preprocessor bridges the disparity between solvers that focus on combinatorial graphs and large practical graphs. In fact, on most of the practical instances the combined setup significantly outperforms previous state-of-the-art.
Cite as

Markus Anders, Pascal Schweitzer, and Julian Stieß. Engineering a Preprocessor for Symmetry Detection. In 21st International Symposium on Experimental Algorithms (SEA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 265, pp. 1:1-1:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.SEA.2023.1,
  author =	{Anders, Markus and Schweitzer, Pascal and Stie{\ss}, Julian},
  title =	{{Engineering a Preprocessor for Symmetry Detection}},
  booktitle =	{21st International Symposium on Experimental Algorithms (SEA 2023)},
  pages =	{1:1--1:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-279-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{265},
  editor =	{Georgiadis, Loukas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2023.1},
  URN =		{urn:nbn:de:0030-drops-183511},
  doi =		{10.4230/LIPIcs.SEA.2023.1},
  annote =	{Keywords: graph isomorphism, automorphism groups, symmetry detection, preprocessors}
}
Document
DOI: 10.4230/LIPIcs.ESA.2022.46
SAT Backdoors: Depth Beats Size

Authors: Jan Dreier, Sebastian Ordyniak, and Stefan Szeider

Published in: LIPIcs, Volume 244, 30th Annual European Symposium on Algorithms (ESA 2022)

Abstract
For several decades, much effort has been put into identifying classes of CNF formulas whose satisfiability can be decided in polynomial time. Classic results are the linear-time tractability of Horn formulas (Aspvall, Plass, and Tarjan, 1979) and Krom (i.e., 2CNF) formulas (Dowling and Gallier, 1984). Backdoors, introduced by Williams, Gomes and Selman (2003), gradually extend such a tractable class to all formulas of bounded distance to the class. Backdoor size provides a natural but rather crude distance measure between a formula and a tractable class. Backdoor depth, introduced by Mählmann, Siebertz, and Vigny (2021), is a more refined distance measure, which admits the utilization of different backdoor variables in parallel. Bounded backdoor size implies bounded backdoor depth, but there are formulas of constant backdoor depth and arbitrarily large backdoor size. We propose FPT approximation algorithms to compute backdoor depth into the classes Horn and Krom. This leads to a linear-time algorithm for deciding the satisfiability of formulas of bounded backdoor depth into these classes. We base our FPT approximation algorithm on a sophisticated notion of obstructions, extending Mählmann et al.’s obstruction trees in various ways, including the addition of separator obstructions. We develop the algorithm through a new game-theoretic framework that simplifies the reasoning about backdoors. Finally, we show that bounded backdoor depth captures tractable classes of CNF formulas not captured by any known method.
Cite as

Jan Dreier, Sebastian Ordyniak, and Stefan Szeider. SAT Backdoors: Depth Beats Size. In 30th Annual European Symposium on Algorithms (ESA 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 244, pp. 46:1-46:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dreier_et_al:LIPIcs.ESA.2022.46,
  author =	{Dreier, Jan and Ordyniak, Sebastian and Szeider, Stefan},
  title =	{{SAT Backdoors: Depth Beats Size}},
  booktitle =	{30th Annual European Symposium on Algorithms (ESA 2022)},
  pages =	{46:1--46:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-247-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{244},
  editor =	{Chechik, Shiri and Navarro, Gonzalo and Rotenberg, Eva 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.2022.46},
  URN =		{urn:nbn:de:0030-drops-169840},
  doi =		{10.4230/LIPIcs.ESA.2022.46},
  annote =	{Keywords: satisfiability, backdoor (depth)}
}
Document
DOI: 10.4230/LIPIcs.ESA.2022.47
Finding a Cluster in Incomplete Data

Authors: Eduard Eiben, Robert Ganian, Iyad Kanj, Sebastian Ordyniak, and Stefan Szeider

Published in: LIPIcs, Volume 244, 30th Annual European Symposium on Algorithms (ESA 2022)

Abstract
We study two variants of the fundamental problem of finding a cluster in incomplete data. In the problems under consideration, we are given a multiset of incomplete d-dimensional vectors over the binary domain and integers k and r, and the goal is to complete the missing vector entries so that the multiset of complete vectors either contains (i) a cluster of k vectors of radius at most r, or (ii) a cluster of k vectors of diameter at most r. We give tight characterizations of the parameterized complexity of the problems under consideration with respect to the parameters k, r, and a third parameter that captures the missing vector entries.
Cite as

Eduard Eiben, Robert Ganian, Iyad Kanj, Sebastian Ordyniak, and Stefan Szeider. Finding a Cluster in Incomplete Data. In 30th Annual European Symposium on Algorithms (ESA 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 244, pp. 47:1-47:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{eiben_et_al:LIPIcs.ESA.2022.47,
  author =	{Eiben, Eduard and Ganian, Robert and Kanj, Iyad and Ordyniak, Sebastian and Szeider, Stefan},
  title =	{{Finding a Cluster in Incomplete Data}},
  booktitle =	{30th Annual European Symposium on Algorithms (ESA 2022)},
  pages =	{47:1--47:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-247-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{244},
  editor =	{Chechik, Shiri and Navarro, Gonzalo and Rotenberg, Eva 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.2022.47},
  URN =		{urn:nbn:de:0030-drops-169858},
  doi =		{10.4230/LIPIcs.ESA.2022.47},
  annote =	{Keywords: Parameterized complexity, incomplete data, clustering}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.MFCS.2022
LIPIcs, Volume 241, MFCS 2022, Complete Volume

Authors: Stefan Szeider, Robert Ganian, and Alexandra Silva

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
LIPIcs, Volume 241, MFCS 2022, Complete Volume
Cite as

Stefan Szeider, Robert Ganian, and Alexandra Silva. LIPIcs, Volume 241, MFCS 2022, Complete Volume. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 1-1236, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Proceedings{szeider_et_al:LIPIcs.MFCS.2022,
  title =	{{LIPIcs, Volume 241, MFCS 2022, Complete Volume}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{1--1236},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022},
  URN =		{urn:nbn:de:0030-drops-167975},
  doi =		{10.4230/LIPIcs.MFCS.2022},
  annote =	{Keywords: LIPIcs, Volume 241, MFCS 2022, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.MFCS.2022.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Stefan Szeider, Robert Ganian, and Alexandra Silva

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

Stefan Szeider, Robert Ganian, and Alexandra Silva. Front Matter, Table of Contents, Preface, Conference Organization. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 0:i-0:xviii, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{szeider_et_al:LIPIcs.MFCS.2022.0,
  author =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{0:i--0:xviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.0},
  URN =		{urn:nbn:de:0030-drops-167981},
  doi =		{10.4230/LIPIcs.MFCS.2022.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2022.1
Long Cycles in Graphs: Extremal Combinatorics Meets Parameterized Algorithms (Invited Talk)

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

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We discuss recent algorithmic extensions of two classic results of extremal combinatorics about long paths in graphs. First, the theorem of Dirac from 1952 asserts that a 2-connected graph G with the minimum vertex degree d > 1, is either Hamiltonian or contains a cycle of length at least 2d. Second, the theorem of Erdős-Gallai from 1959, states that a graph G with the average vertex degree D > 1, contains a cycle of length at least D. The proofs of these theorems are constructive, they provide polynomial-time algorithms constructing cycles of lengths 2d and D. We extend these algorithmic results by showing that each of the problems, to decide whether a 2-connected graph contains a cycle of length at least 2d+k or of a cycle of length at least D+k, is fixed-parameter tractable parameterized by k.
Cite as

Fedor V. Fomin, Petr A. Golovach, Danil Sagunov, and Kirill Simonov. Long Cycles in Graphs: Extremal Combinatorics Meets Parameterized Algorithms (Invited Talk). In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 1:1-1:4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fomin_et_al:LIPIcs.MFCS.2022.1,
  author =	{Fomin, Fedor V. and Golovach, Petr A. and Sagunov, Danil and Simonov, Kirill},
  title =	{{Long Cycles in Graphs: Extremal Combinatorics Meets Parameterized Algorithms}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{1:1--1:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.1},
  URN =		{urn:nbn:de:0030-drops-167999},
  doi =		{10.4230/LIPIcs.MFCS.2022.1},
  annote =	{Keywords: Longest path, longest cycle, fixed-parameter tractability, above guarantee parameterization, average degree, dense graph, Dirac theorem, Erd\H{o}s-Gallai theorem}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2022.2
Modern Dynamic Data Structures (Invited Talk)

Authors: Monika Henzinger

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We give an overview of differentially private dynamic data structure, aka differentially private algorithms under continual release.
Cite as

Monika Henzinger. Modern Dynamic Data Structures (Invited Talk). In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 2:1-2:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{henzinger:LIPIcs.MFCS.2022.2,
  author =	{Henzinger, Monika},
  title =	{{Modern Dynamic Data Structures}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.2},
  URN =		{urn:nbn:de:0030-drops-168009},
  doi =		{10.4230/LIPIcs.MFCS.2022.2},
  annote =	{Keywords: Differential privacy, data structures}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2022.3
An Updated Survey of Bidding Games on Graphs (Invited Talk)

Authors: Guy Avni and Thomas A. Henzinger

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an "auction" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We summarize how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.
Cite as

Guy Avni and Thomas A. Henzinger. An Updated Survey of Bidding Games on Graphs (Invited Talk). In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 3:1-3:6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.MFCS.2022.3,
  author =	{Avni, Guy and Henzinger, Thomas A.},
  title =	{{An Updated Survey of Bidding Games on Graphs}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{3:1--3:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.3},
  URN =		{urn:nbn:de:0030-drops-168017},
  doi =		{10.4230/LIPIcs.MFCS.2022.3},
  annote =	{Keywords: Bidding games, Richman bidding, poorman bidding, mean-payoff, parity}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2022.4
Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk)

Authors: Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos, and Rui Yan

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
Game-theoretic concepts have been extensively studied in economics to provide insight into competitive behaviour and strategic decision making. As computing systems increasingly involve concurrently acting autonomous agents, game-theoretic approaches are becoming widespread in computer science as a faithful modelling abstraction. These techniques can be used to reason about the competitive or collaborative behaviour of multiple rational agents with distinct goals or objectives. This paper provides an overview of recent advances in developing a modelling, verification and strategy synthesis framework for concurrent stochastic games implemented in the probabilistic model checker PRISM-games. This is based on a temporal logic that supports finite- and infinite-horizon temporal properties in both a zero-sum and nonzero-sum setting, the latter using Nash and correlated equilibria with respect to two optimality criteria, social welfare and social fairness. We summarise the key concepts, logics and algorithms and the currently available tool support. Future challenges and recent progress in adapting the framework and algorithmic solutions to continuous environments and neural networks are also outlined.
Cite as

Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos, and Rui Yan. Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk). In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 4:1-4:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kwiatkowska_et_al:LIPIcs.MFCS.2022.4,
  author =	{Kwiatkowska, Marta and Norman, Gethin and Parker, David and Santos, Gabriel and Yan, Rui},
  title =	{{Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{4:1--4:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.4},
  URN =		{urn:nbn:de:0030-drops-168026},
  doi =		{10.4230/LIPIcs.MFCS.2022.4},
  annote =	{Keywords: Probabilistic model checking, stochastic games, equilibria}
}
  • Refine by Author
  • 21 Szeider, Stefan
  • 7 Ganian, Robert
  • 6 Ordyniak, Sebastian
  • 5 Kirchweger, Markus
  • 4 Ouaknine, Joël
  • Show More...

  • Refine by Classification
  • 9 Theory of computation → Graph algorithms analysis
  • 8 Mathematics of computing → Graph algorithms
  • 8 Theory of computation → Design and analysis of algorithms
  • 8 Theory of computation → Parameterized complexity and exact algorithms
  • 7 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 5 Parameterized complexity
  • 4 parameterized complexity
  • 3 NP-hardness
  • 3 Parameterized Complexity
  • 3 SAT
  • Show More...

  • Refine by Type
  • 107 document
  • 1 volume

  • Refine by Publication Year
  • 91 2022
  • 6 2023
  • 2 2013
  • 2 2017
  • 2 2021
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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