444 Search Results for "R�ckert, Markus"

Document
Extended Abstract
DOI: 10.4230/LIPIcs.ITCS.2024.57
Communicating with Anecdotes (Extended Abstract)

Authors: Nika Haghtalab, Nicole Immorlica, Brendan Lucier, Markus Mobius, and Divyarthi Mohan

Published in: LIPIcs, Volume 287, 15th Innovations in Theoretical Computer Science Conference (ITCS 2024)

Abstract
We study a communication game between a sender and receiver. The sender chooses one of her signals about the state of the world (i.e., an anecdote) and communicates it to the receiver who takes an action affecting both players. The sender and receiver both care about the state of the world but are also influenced by personal preferences, so their ideal actions can differ. We characterize perfect Bayesian equilibria. The sender faces a temptation to persuade: she wants to select a biased anecdote to influence the receiver’s action. Anecdotes are still informative to the receiver (who will debias at equilibrium) but the attempt to persuade comes at the cost of precision. This gives rise to informational homophily where the receiver prefers to listen to like-minded senders because they provide higher-precision signals. Communication becomes polarized when the sender is an expert with access to many signals, with the sender choosing extreme outlier anecdotes at equilibrium (unless preferences are perfectly aligned). This polarization dissipates all the gains from communication with an increasingly well-informed sender when the anecdote distribution is heavy-tailed. Experts therefore face a curse of informedness: receivers will prefer to listen to less-informed senders who cannot pick biased signals as easily.
Cite as

Nika Haghtalab, Nicole Immorlica, Brendan Lucier, Markus Mobius, and Divyarthi Mohan. Communicating with Anecdotes (Extended Abstract). In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 57:1-57:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{haghtalab_et_al:LIPIcs.ITCS.2024.57,
  author =	{Haghtalab, Nika and Immorlica, Nicole and Lucier, Brendan and Mobius, Markus and Mohan, Divyarthi},
  title =	{{Communicating with Anecdotes}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{57:1--57:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.57},
  URN =		{urn:nbn:de:0030-drops-195852},
  doi =		{10.4230/LIPIcs.ITCS.2024.57},
  annote =	{Keywords: Communication game, Equilibrium, Polarization, Signalling}
}
Document
DOI: 10.4230/DagRep.13.1.184
Quality of Sustainable Experience (QoSE) (Dagstuhl Seminar 23042)

Authors: Katrien De Moor, Markus Fiedler, Ashok Jhunjhunwala, and Alexander Raake

Published in: Dagstuhl Reports, Volume 13, Issue 1 (2023)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23042 "Quality of Sustainable Experience (QoSE)". The seminar aimed to bring together people from different fields, perspectives and backgrounds. The participants discussed how experiences - as the main selling point of products and services – in various ICT-related domains can be made more sustainable, how they can contribute to relevant sustainable development goals, and how the quality and degree of sustainability of such experiences may be evaluated and be better understood. The main objectives of the seminar were to foster new alliances, to inspire, to trigger scientific renewal, as well as to identify future opportunities and research challenges through a hands-on approach.
Cite as

Katrien De Moor, Markus Fiedler, Ashok Jhunjhunwala, and Alexander Raake. Quality of Sustainable Experience (QoSE) (Dagstuhl Seminar 23042). In Dagstuhl Reports, Volume 13, Issue 1, pp. 184-215, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{demoor_et_al:DagRep.13.1.184,
  author =	{De Moor, Katrien and Fiedler, Markus and Jhunjhunwala, Ashok and Raake, Alexander},
  title =	{{Quality of Sustainable Experience (QoSE) (Dagstuhl Seminar 23042)}},
  pages =	{184--215},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{13},
  number =	{1},
  editor =	{De Moor, Katrien and Fiedler, Markus and Jhunjhunwala, Ashok and Raake, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.13.1.184},
  URN =		{urn:nbn:de:0030-drops-191212},
  doi =		{10.4230/DagRep.13.1.184},
  annote =	{Keywords: Design for Sustainability, Digitalisation, Human-Computer Interaction, Information and Communication Technology, Wellbeing}
}
Document
DOI: 10.4230/LIPIcs.GIScience.2023.1
Do You Need Instructions Again? Predicting Wayfinding Instruction Demand

Authors: Negar Alinaghi, Tiffany C. K. Kwok, Peter Kiefer, and Ioannis Giannopoulos

Published in: LIPIcs, Volume 277, 12th International Conference on Geographic Information Science (GIScience 2023)

Abstract
The demand for instructions during wayfinding, defined as the frequency of requesting instructions for each decision point, can be considered as an important indicator of the internal cognitive processes during wayfinding. This demand can be a consequence of the mental state of feeling lost, being uncertain, mind wandering, having difficulty following the route, etc. Therefore, it can be of great importance for theoretical cognitive studies on human perception of the environment. From an application perspective, this demand can be used as a measure of the effectiveness of the navigation assistance system. It is therefore worthwhile to be able to predict this demand and also to know what factors trigger it. This paper takes a step in this direction by reporting a successful prediction of instruction demand (accuracy of 78.4%) in a real-world wayfinding experiment with 45 participants, and interpreting the environmental, user, instructional, and gaze-related features that caused it.
Cite as

Negar Alinaghi, Tiffany C. K. Kwok, Peter Kiefer, and Ioannis Giannopoulos. Do You Need Instructions Again? Predicting Wayfinding Instruction Demand. In 12th International Conference on Geographic Information Science (GIScience 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 277, pp. 1:1-1:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{alinaghi_et_al:LIPIcs.GIScience.2023.1,
  author =	{Alinaghi, Negar and Kwok, Tiffany C. K. and Kiefer, Peter and Giannopoulos, Ioannis},
  title =	{{Do You Need Instructions Again? Predicting Wayfinding Instruction Demand}},
  booktitle =	{12th International Conference on Geographic Information Science (GIScience 2023)},
  pages =	{1:1--1:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-288-4},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{277},
  editor =	{Beecham, Roger and Long, Jed A. and Smith, Dianna and Zhao, Qunshan and Wise, Sarah},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.GIScience.2023.1},
  URN =		{urn:nbn:de:0030-drops-188963},
  doi =		{10.4230/LIPIcs.GIScience.2023.1},
  annote =	{Keywords: Wayfinding, Navigation Instructions, Urban Computing, Gaze Analysis}
}
Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2023.56
Robustness for Space-Bounded Statistical Zero Knowledge

Authors: Eric Allender, Jacob Gray, Saachi Mutreja, Harsha Tirumala, and Pengxiang Wang

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

Abstract
We show that the space-bounded Statistical Zero Knowledge classes SZK_L and NISZK_L are surprisingly robust, in that the power of the verifier and simulator can be strengthened or weakened without affecting the resulting class. Coupled with other recent characterizations of these classes [Eric Allender et al., 2023], this can be viewed as lending support to the conjecture that these classes may coincide with the non-space-bounded classes SZK and NISZK, respectively.
Cite as

Eric Allender, Jacob Gray, Saachi Mutreja, Harsha Tirumala, and Pengxiang Wang. Robustness for Space-Bounded Statistical Zero Knowledge. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 275, pp. 56:1-56:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{allender_et_al:LIPIcs.APPROX/RANDOM.2023.56,
  author =	{Allender, Eric and Gray, Jacob and Mutreja, Saachi and Tirumala, Harsha and Wang, Pengxiang},
  title =	{{Robustness for Space-Bounded Statistical Zero Knowledge}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)},
  pages =	{56:1--56:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-296-9},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{275},
  editor =	{Megow, Nicole and Smith, Adam},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2023.56},
  URN =		{urn:nbn:de:0030-drops-188815},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2023.56},
  annote =	{Keywords: Interactive Proofs}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2023.1
Optimal Bicycle Routes with Few Signal Stops

Authors: Ekkehard Köhler, Markus Rogge, Robert Scheffler, and Martin Strehler

Published in: OASIcs, Volume 115, 23rd Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2023)

Abstract
With the increasing popularity of cycling as a mode of transportation, there is a growing need for efficient routing algorithms that consider the specific requirements of cyclists. This paper studies the optimization of bicycle routes while minimizing the number of stops at traffic signals. In particular, we consider three different types of stopping strategies and three types of routes, namely paths, trails, and walks. We present hardness results as well as a pseudo-polynomial algorithm for the problem of computing an optimal route with respect to a pre-defined stop bound.
Cite as

Ekkehard Köhler, Markus Rogge, Robert Scheffler, and Martin Strehler. Optimal Bicycle Routes with Few Signal Stops. In 23rd Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2023). Open Access Series in Informatics (OASIcs), Volume 115, pp. 1:1-1:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kohler_et_al:OASIcs.ATMOS.2023.1,
  author =	{K\"{o}hler, Ekkehard and Rogge, Markus and Scheffler, Robert and Strehler, Martin},
  title =	{{Optimal Bicycle Routes with Few Signal Stops}},
  booktitle =	{23rd Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2023)},
  pages =	{1:1--1:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-302-7},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{115},
  editor =	{Frigioni, Daniele and Schiewe, Philine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2023.1},
  URN =		{urn:nbn:de:0030-drops-187628},
  doi =		{10.4230/OASIcs.ATMOS.2023.1},
  annote =	{Keywords: Constrained shortest path, traffic signals, bicycle routes}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2023.4
Algebraic Reasoning for (Un)Solvable Loops (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Loop invariants describe valid program properties that hold before and after every loop iteration. As such, loop invariants are the workhorses in formalizing loop semantics and automating the formal analysis and verification of programs with loops. While automatically synthesizing loop invariants is, in general, an uncomputable problem, when considering only single-path loops with linear updates (linear loops), the strongest polynomial invariant is in fact computable [Michael Karr, 1976; Markus Müller-Olm and Helmut Seidl, 2004; Laura Kovács, 2008; Ehud Hrushovski et al., 2018]. Yet, already for loops with "only" polynomial updates, computing the strongest invariant has been an open challenge since 2004 [Markus Müller-Olm and Helmut Seidl, 2004]. In this invited talk, we first present computability results on polynomial invariant synthesis for restricted polynomial loops, called solvable loops [Rodríguez-Carbonell and Kapur, 2004]. Key to solvable loops is that one can automatically compute invariants from closed-form solutions of algebraic recurrence equations that model the loop behaviour [Laura Kovács, 2008; Andreas Humenberger et al., 2017]. We also establish a technique for invariant synthesis for classes of loops that are not solvable, termed unsolvable loops [Daneshvar Amrollahi et al., 2022]. We next study the limits of computability in deriving the (strongest) polynomial invariants for arbitrary polynomial loops. We prove that computing the strongest polynomial invariant of arbitrary, single-path polynomial loops is very hard [Julian Müllner, 2023] - namely, it is at least as hard as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008], a prominent algebraic problem in the theory of linear recurrences. Going beyond single-path loops, we show that the strongest polynomial invariant is uncomputable already for multi-path polynomial loops with arbitrary quadratic polynomial updates [Laura Kovács and Anton Varonka, 2023].
Cite as

Laura Kovács. Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.MFCS.2023.4,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Algebraic Reasoning for (Un)Solvable Loops}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.4},
  URN =		{urn:nbn:de:0030-drops-185385},
  doi =		{10.4230/LIPIcs.MFCS.2023.4},
  annote =	{Keywords: Symbolic Computation, Formal Methods, Loop Analysis, Polynomial Invariants}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.1
Algorithms Transcending the SAT-Symmetry Interface

Authors: Markus Anders, Pascal Schweitzer, and Mate Soos

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

Abstract
Dedicated treatment of symmetries in satisfiability problems (SAT) is indispensable for solving various classes of instances arising in practice. However, the exploitation of symmetries usually takes a black box approach. Typically, off-the-shelf external, general-purpose symmetry detection tools are invoked to compute symmetry groups of a formula. The groups thus generated are a set of permutations passed to a separate tool to perform further analyzes to understand the structure of the groups. The result of this second computation is in turn used for tasks such as static symmetry breaking or dynamic pruning of the search space. Within this pipeline of tools, the detection and analysis of symmetries typically incurs the majority of the time overhead for symmetry exploitation. In this paper we advocate for a more holistic view of what we call the SAT-symmetry interface. We formulate a computational setting, centered around a new concept of joint graph/group pairs, to analyze and improve the detection and analysis of symmetries. Using our methods, no information is lost performing computational tasks lying on the SAT-symmetry interface. Having access to the entire input allows for simpler, yet efficient algorithms. Specifically, we devise algorithms and heuristics for computing finest direct disjoint decompositions, finding equivalent orbits, and finding natural symmetric group actions. Our algorithms run in what we call instance-quasi-linear time, i.e., almost linear time in terms of the input size of the original formula and the description length of the symmetry group returned by symmetry detection tools. Our algorithms improve over both heuristics used in state-of-the-art symmetry exploitation tools, as well as theoretical general-purpose algorithms.
Cite as

Markus Anders, Pascal Schweitzer, and Mate Soos. Algorithms Transcending the SAT-Symmetry Interface. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.SAT.2023.1,
  author =	{Anders, Markus and Schweitzer, Pascal and Soos, Mate},
  title =	{{Algorithms Transcending the SAT-Symmetry Interface}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{1:1--1:21},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.1},
  URN =		{urn:nbn:de:0030-drops-184635},
  doi =		{10.4230/LIPIcs.SAT.2023.1},
  annote =	{Keywords: boolean satisfiability, symmetry exploitation, computational group theory}
}
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-dev.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-dev.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.CCC.2023.2
Border Complexity of Symbolic Determinant Under Rank One Restriction

Authors: Abhranil Chatterjee, Sumanta Ghosh, Rohit Gurjar, and Roshan Raj

Published in: LIPIcs, Volume 264, 38th Computational Complexity Conference (CCC 2023)

Abstract
VBP is the class of polynomial families that can be computed by the determinant of a symbolic matrix of the form A_0 + ∑_{i=1}^n A_i x_i where the size of each A_i is polynomial in the number of variables (equivalently, computable by polynomial-sized algebraic branching programs (ABP)). A major open problem in geometric complexity theory (GCT) is to determine whether VBP is closed under approximation i.e. whether VBP = VBP^ ̅. The power of approximation is well understood for some restricted models of computation, e.g. the class of depth-two circuits, read-once oblivious ABPs (ROABP), monotone ABPs, depth-three circuits of bounded top fan-in, and width-two ABPs. The former three classes are known to be closed under approximation [Markus Bläser et al., 2020], whereas the approximative closure of the last one captures the entire class of polynomial families computable by polynomial-sized formulas [Bringmann et al., 2017]. In this work, we consider the subclass of VBP computed by the determinant of a symbolic matrix of the form A_0 + ∑_{i=1}^n A_i x_i where for each 1 ≤ i ≤ n, A_i is of rank one. This class has been studied extensively [Edmonds, 1968; Jack Edmonds, 1979; Murota, 1993] and efficient identity testing algorithms are known for it [Lovász, 1989; Rohit Gurjar and Thomas Thierauf, 2020]. We show that this class is closed under approximation. In the language of algebraic geometry, we show that the set obtained by taking coordinatewise products of pairs of points from (the Plücker embedding of) a Grassmannian variety is closed.
Cite as

Abhranil Chatterjee, Sumanta Ghosh, Rohit Gurjar, and Roshan Raj. Border Complexity of Symbolic Determinant Under Rank One Restriction. In 38th Computational Complexity Conference (CCC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 264, pp. 2:1-2:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CCC.2023.2,
  author =	{Chatterjee, Abhranil and Ghosh, Sumanta and Gurjar, Rohit and Raj, Roshan},
  title =	{{Border Complexity of Symbolic Determinant Under Rank One Restriction}},
  booktitle =	{38th Computational Complexity Conference (CCC 2023)},
  pages =	{2:1--2:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-282-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{264},
  editor =	{Ta-Shma, Amnon},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2023.2},
  URN =		{urn:nbn:de:0030-drops-182721},
  doi =		{10.4230/LIPIcs.CCC.2023.2},
  annote =	{Keywords: Border Complexity, Symbolic Determinant, Valuated Matroid}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.124
The Identity Problem in ℤ ≀ ℤ Is Decidable

Authors: Ruiwen Dong

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We consider semigroup algorithmic problems in the wreath product ℤ ≀ ℤ. Our paper focuses on two decision problems introduced by Choffrut and Karhumäki (2005): the Identity Problem (does a semigroup contain the neutral element?) and the Group Problem (is a semigroup a group?) for finitely generated sub-semigroups of ℤ ≀ ℤ. We show that both problems are decidable. Our result complements the undecidability of the Semigroup Membership Problem (does a semigroup contain a given element?) in ℤ ≀ ℤ shown by Lohrey, Steinberg and Zetzsche (ICALP 2013), and contributes an important step towards solving semigroup algorithmic problems in general metabelian groups.
Cite as

Ruiwen Dong. The Identity Problem in ℤ ≀ ℤ Is Decidable. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 124:1-124:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dong:LIPIcs.ICALP.2023.124,
  author =	{Dong, Ruiwen},
  title =	{{The Identity Problem in \mathbb{Z} ≀ \mathbb{Z} Is Decidable}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{124:1--124:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.124},
  URN =		{urn:nbn:de:0030-drops-181768},
  doi =		{10.4230/LIPIcs.ICALP.2023.124},
  annote =	{Keywords: wreath product, algorithmic group theory, identity problem, polynomial semiring, positive coefficients}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.134
On the Complexity of Diameter and Related Problems in Permutation Groups

Authors: Markus Lohrey and Andreas Rosowski

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We prove that it is Π₂^𝖯-complete to verify whether the diameter of a given permutation group G = ⟨A⟩ is bounded by a unary encoded number k. This solves an open problem from a paper of Even and Goldreich, where the problem was shown to be NP-hard. Verifying whether the diameter is exactly k is complete for the class consisting of all intersections of a Π₂^𝖯-language and a Σ₂^𝖯-language. A similar result is shown for the length of a given permutation π, which is the minimal k such that π can be written as a product of at most k generators from A. Even and Goldreich proved that it is NP-complete to verify, whether the length of a given π is at most k (with k given in unary encoding). We show that it is DP-complete to verify whether the length is exactly k. Finally, we deduce from our result on the diameter that it is Π₂^𝖯-complete to check whether a given finite automaton with transitions labelled by permutations from S_n produces all permutations from S_n.
Cite as

Markus Lohrey and Andreas Rosowski. On the Complexity of Diameter and Related Problems in Permutation Groups. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 134:1-134:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{lohrey_et_al:LIPIcs.ICALP.2023.134,
  author =	{Lohrey, Markus and Rosowski, Andreas},
  title =	{{On the Complexity of Diameter and Related Problems in Permutation Groups}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{134:1--134:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.134},
  URN =		{urn:nbn:de:0030-drops-181864},
  doi =		{10.4230/LIPIcs.ICALP.2023.134},
  annote =	{Keywords: algorithms for finite groups, diameter of permutation groups, rational subsets in groups}
}
Document
DOI: 10.4230/LIPIcs.SAND.2023.14
Multistage Shortest Path: Instances and Practical Evaluation

Authors: Markus Chimani and Niklas Troost

Published in: LIPIcs, Volume 257, 2nd Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2023)

Abstract
A multistage graph problem is a generalization of a traditional graph problem where, instead of a single input graph, we consider a sequence of graphs. We ask for a sequence of solutions, one for each input graph, such that consecutive solutions are as similar as possible. There are several theoretical results on different multistage problems and their complexities, as well as FPT and approximation algorithms. However, there is a severe lack of experimental validation and resulting feedback. Not only are there no algorithmic experiments in literature, we do not even know of any strong set of multistage benchmark instances. In this paper we want to improve on this situation. We consider the natural problem of multistage shortest path (MSP). First, we propose a rich benchmark set, ranging from synthetic to real-world data, and discuss relevant aspects to ensure non-trivial instances, which is a surprisingly delicate task. Secondly, we present an explorative study on heuristic, approximate, and exact algorithms for the MSP problem from a practical point of view. Our practical findings also inform theoretical research in arguing sensible further directions. For example, based on our study we propose to focus on algorithms for multistage instances that do not rely on 2-stage oracles.
Cite as

Markus Chimani and Niklas Troost. Multistage Shortest Path: Instances and Practical Evaluation. In 2nd Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 257, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chimani_et_al:LIPIcs.SAND.2023.14,
  author =	{Chimani, Markus and Troost, Niklas},
  title =	{{Multistage Shortest Path: Instances and Practical Evaluation}},
  booktitle =	{2nd Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2023)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-275-4},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{257},
  editor =	{Doty, David and Spirakis, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAND.2023.14},
  URN =		{urn:nbn:de:0030-drops-179507},
  doi =		{10.4230/LIPIcs.SAND.2023.14},
  annote =	{Keywords: Multistage Graphs, Shortest Paths, Experiments}
}
  • Refine by Author
  • 39 Lohrey, Markus
  • 16 Bläser, Markus
  • 11 Ganardi, Moses
  • 11 Schmid, Markus L.
  • 9 Chimani, Markus
  • Show More...

  • Refine by Classification
  • 29 Theory of computation → Problems, reductions and completeness
  • 27 Theory of computation → Design and analysis of algorithms
  • 24 Mathematics of computing → Graph algorithms
  • 14 Theory of computation → Formal languages and automata theory
  • 14 Theory of computation → Models of computation
  • Show More...

  • Refine by Keyword
  • 6 Wayfinding
  • 6 complexity
  • 5 Preface
  • 5 Table of Contents
  • 5 algorithm engineering
  • Show More...

  • Refine by Type
  • 444 document

  • Refine by Publication Year
  • 83 2021
  • 73 2020
  • 72 2019
  • 41 2008
  • 23 2022
  • 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact