15 Search Results for "Mal�k, Josef"

Document
DOI: 10.4230/LIPIcs.ITP.2023.19
MizAR 60 for Mizar 50

Authors: Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60% of the Mizar theorems in the hammer setting. We also automatically prove 75% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.
Cite as

Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban. MizAR 60 for Mizar 50. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jakubuv_et_al:LIPIcs.ITP.2023.19,
  author =	{Jakub\r{u}v, Jan and Chvalovsk\'{y}, Karel and Goertzel, Zarathustra and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Mirek and Piotrowski, Bartosz and Schulz, Stephan and Suda, Martin and Urban, Josef},
  title =	{{MizAR 60 for Mizar 50}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.19},
  URN =		{urn:nbn:de:0030-drops-183942},
  doi =		{10.4230/LIPIcs.ITP.2023.19},
  annote =	{Keywords: Mizar, ENIGMA, Automated Reasoning, Machine Learning}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.16
The Isabelle ENIGMA

Authors: Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, and Josef Urban

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of the ENIGMA guidance for the Isabelle problems, targeted versions of neural premise selection, and targeted strategies for E. The methods are trained in several iterations over hundreds of thousands untyped and typed first-order problems extracted from Isabelle. Our final best single-strategy ENIGMA and premise selection system improves the best previous version of E by 25.3% in 15 seconds, outperforming also all other previous ATP and SMT systems.
Cite as

Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, and Josef Urban. The Isabelle ENIGMA. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 16:1-16:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{goertzel_et_al:LIPIcs.ITP.2022.16,
  author =	{Goertzel, Zarathustra A. and Jakub\r{u}v, Jan and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Miroslav and Piepenbrock, Jelle and Urban, Josef},
  title =	{{The Isabelle ENIGMA}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{16:1--16:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.16},
  URN =		{urn:nbn:de:0030-drops-167253},
  doi =		{10.4230/LIPIcs.ITP.2022.16},
  annote =	{Keywords: E Prover, ENIGMA, Premise Selection, Isabelle/Sledgehammer}
}
Document
DOI: 10.4230/LIPIcs.ISAAC.2018.5
Colouring (P_r+P_s)-Free Graphs

Authors: Tereza Klimosová, Josef Malík, Tomás Masarík, Jana Novotná, Daniël Paulusma, and Veronika Slívová

Published in: LIPIcs, Volume 123, 29th International Symposium on Algorithms and Computation (ISAAC 2018)

Abstract
The k-Colouring problem is to decide if the vertices of a graph can be coloured with at most k colours for a fixed integer k such that no two adjacent vertices are coloured alike. If each vertex u must be assigned a colour from a prescribed list L(u) subseteq {1,...,k}, then we obtain the List k-Colouring problem. A graph G is H-free if G does not contain H as an induced subgraph. We continue an extensive study into the complexity of these two problems for H-free graphs. We prove that List 3-Colouring is polynomial-time solvable for (P_2+P_5)-free graphs and for (P_3+P_4)-free graphs. Combining our results with known results yields complete complexity classifications of 3-Colouring and List 3-Colouring on H-free graphs for all graphs H up to seven vertices. We also prove that 5-Colouring is NP-complete for (P_3+P_5)-free graphs.
Cite as

Tereza Klimosová, Josef Malík, Tomás Masarík, Jana Novotná, Daniël Paulusma, and Veronika Slívová. Colouring (P_r+P_s)-Free Graphs. In 29th International Symposium on Algorithms and Computation (ISAAC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 123, pp. 5:1-5:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{klimosova_et_al:LIPIcs.ISAAC.2018.5,
  author =	{Klimosov\'{a}, Tereza and Mal{\'\i}k, Josef and Masar{\'\i}k, Tom\'{a}s and Novotn\'{a}, Jana and Paulusma, Dani\"{e}l and Sl{\'\i}vov\'{a}, Veronika},
  title =	{{Colouring (P\underliner+P\underlines)-Free Graphs}},
  booktitle =	{29th International Symposium on Algorithms and Computation (ISAAC 2018)},
  pages =	{5:1--5:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-094-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{123},
  editor =	{Hsu, Wen-Lian and Lee, Der-Tsai and Liao, Chung-Shou},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2018.5},
  URN =		{urn:nbn:de:0030-drops-99533},
  doi =		{10.4230/LIPIcs.ISAAC.2018.5},
  annote =	{Keywords: vertex colouring, H-free graph, linear forest}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.4
Selecting a Leader in a Network of Finite State Machines

Authors: Yehuda Afek, Yuval Emek, and Noa Kolikant

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
This paper studies a variant of the leader election problem under the stone age model (Emek and Wattenhofer, PODC 2013) that considers a network of n randomized finite automata with very weak communication capabilities (a multi-frequency asynchronous generalization of the beeping model's communication scheme). Since solving the classic leader election problem is impossible even in more powerful models, we consider a relaxed variant, referred to as k-leader selection, in which a leader should be selected out of at most k initial candidates. Our main contribution is an algorithm that solves k-leader selection for bounded k in the aforementioned stone age model. On (general topology) graphs of diameter D, this algorithm runs in O~(D) time and succeeds with high probability. The assumption that k is bounded turns out to be unavoidable: we prove that if k = omega (1), then no algorithm in this model can solve k-leader selection with a (positive) constant probability.
Cite as

Yehuda Afek, Yuval Emek, and Noa Kolikant. Selecting a Leader in a Network of Finite State Machines. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{afek_et_al:LIPIcs.DISC.2018.4,
  author =	{Afek, Yehuda and Emek, Yuval and Kolikant, Noa},
  title =	{{Selecting a Leader in a Network of Finite State Machines}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{4:1--4:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.4},
  URN =		{urn:nbn:de:0030-drops-97933},
  doi =		{10.4230/LIPIcs.DISC.2018.4},
  annote =	{Keywords: stone age model, beeping communication scheme, leader election, k-leader selection, randomized finite state machines, asynchronous scheduler}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.9
Almost Global Problems in the LOCAL Model

Authors: Alkida Balliu, Sebastian Brandt, Dennis Olivetti, and Jukka Suomela

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
The landscape of the distributed time complexity is nowadays well-understood for subpolynomial complexities. When we look at deterministic algorithms in the LOCAL model and locally checkable problems (LCLs) in bounded-degree graphs, the following picture emerges: - There are lots of problems with time complexities Theta(log^* n) or Theta(log n). - It is not possible to have a problem with complexity between omega(log^* n) and o(log n). - In general graphs, we can construct LCL problems with infinitely many complexities between omega(log n) and n^{o(1)}. - In trees, problems with such complexities do not exist. However, the high end of the complexity spectrum was left open by prior work. In general graphs there are problems with complexities of the form Theta(n^alpha) for any rational 0 < alpha <=1/2, while for trees only complexities of the form Theta(n^{1/k}) are known. No LCL problem with complexity between omega(sqrt{n}) and o(n) is known, and neither are there results that would show that such problems do not exist. We show that: - In general graphs, we can construct LCL problems with infinitely many complexities between omega(sqrt{n}) and o(n). - In trees, problems with such complexities do not exist. Put otherwise, we show that any LCL with a complexity o(n) can be solved in time O(sqrt{n}) in trees, while the same is not true in general graphs.
Cite as

Alkida Balliu, Sebastian Brandt, Dennis Olivetti, and Jukka Suomela. Almost Global Problems in the LOCAL Model. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{balliu_et_al:LIPIcs.DISC.2018.9,
  author =	{Balliu, Alkida and Brandt, Sebastian and Olivetti, Dennis and Suomela, Jukka},
  title =	{{Almost Global Problems in the LOCAL Model}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{9:1--9:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.9},
  URN =		{urn:nbn:de:0030-drops-97982},
  doi =		{10.4230/LIPIcs.DISC.2018.9},
  annote =	{Keywords: Distributed complexity theory, locally checkable labellings, LOCAL model}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.15
Deterministic Blind Radio Networks

Authors: Artur Czumaj and Peter Davies

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
Ad-hoc radio networks and multiple access channels are classical and well-studied models of distributed systems, with a large body of literature on deterministic algorithms for fundamental communications primitives such as broadcasting and wake-up. However, almost all of these algorithms assume knowledge of the number of participating nodes and the range of possible IDs, and often make the further assumption that the latter is linear in the former. These are very strong assumptions for models which were designed to capture networks of weak devices organized in an ad-hoc manner. It was believed that without this knowledge, deterministic algorithms must necessarily be much less efficient. In this paper we address this fundamental question and show that this is not the case. We present deterministic algorithms for blind networks (in which nodes know only their own IDs), which match or nearly match the running times of the fastest algorithms which assume network knowledge (and even surpass the previous fastest algorithms which assume parameter knowledge but not small labels). Specifically, in multiple access channels with k participating nodes and IDs up to L, we give a wake-up algorithm requiring O((k log L log k)/(log log k)) time, improving dramatically over the O(L^3 log^3 L) time algorithm of De Marco et al. (2007), and a broadcasting algorithm requiring O(k log L log log k) time, improving over the O(L) time algorithm of Gasieniec et al. (2001) in most circumstances. Furthermore, we show how these same algorithms apply directly to multi-hop radio networks, achieving even larger running time improvements.
Cite as

Artur Czumaj and Peter Davies. Deterministic Blind Radio Networks. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czumaj_et_al:LIPIcs.DISC.2018.15,
  author =	{Czumaj, Artur and Davies, Peter},
  title =	{{Deterministic Blind Radio Networks}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.15},
  URN =		{urn:nbn:de:0030-drops-98047},
  doi =		{10.4230/LIPIcs.DISC.2018.15},
  annote =	{Keywords: Broadcasting, Deterministic Algorithms, Radio Networks}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.19
TuringMobile: A Turing Machine of Oblivious Mobile Robots with Limited Visibility and Its Applications

Authors: Giuseppe A. Di Luna, Paola Flocchini, Nicola Santoro, and Giovanni Viglietta

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
In this paper we investigate the computational power of a set of mobile robots with limited visibility. At each iteration, a robot takes a snapshot of its surroundings, uses the snapshot to compute a destination point, and it moves toward its destination. Each robot is punctiform and memoryless, it operates in R^m, it has a local reference system independent of the other robots' ones, and is activated asynchronously by an adversarial scheduler. Moreover, the robots are non-rigid, in that they may be stopped by the scheduler at each move before reaching their destination (but are guaranteed to travel at least a fixed unknown distance before being stopped). We show that despite these strong limitations, it is possible to arrange 3m+3k of these weak entities in R^m to simulate the behavior of a stronger robot that is rigid (i.e., it always reaches its destination) and is endowed with k registers of persistent memory, each of which can store a real number. We call this arrangement a TuringMobile. In its simplest form, a TuringMobile consisting of only three robots can travel in the plane and store and update a single real number. We also prove that this task is impossible with fewer than three robots. Among the applications of the TuringMobile, we focused on Near-Gathering (all robots have to gather in a small-enough disk) and Pattern Formation (of which Gathering is a special case) with limited visibility. Interestingly, our investigation implies that both problems are solvable in Euclidean spaces of any dimension, even if the visibility graph of the robots is initially disconnected, provided that a small amount of these robots are arranged to form a TuringMobile. In the special case of the plane, a basic TuringMobile of only three robots is sufficient.
Cite as

Giuseppe A. Di Luna, Paola Flocchini, Nicola Santoro, and Giovanni Viglietta. TuringMobile: A Turing Machine of Oblivious Mobile Robots with Limited Visibility and Its Applications. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{diluna_et_al:LIPIcs.DISC.2018.19,
  author =	{Di Luna, Giuseppe A. and Flocchini, Paola and Santoro, Nicola and Viglietta, Giovanni},
  title =	{{TuringMobile: A Turing Machine of Oblivious Mobile Robots with Limited Visibility and Its Applications}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.19},
  URN =		{urn:nbn:de:0030-drops-98086},
  doi =		{10.4230/LIPIcs.DISC.2018.19},
  annote =	{Keywords: Mobile Robots, Turing Machine, Real RAM}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.20
Beeping a Deterministic Time-Optimal Leader Election

Authors: Fabien Dufoulon, Janna Burman, and Joffroy Beauquier

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
The beeping model is an extremely restrictive broadcast communication model that relies only on carrier sensing. In this model, we solve the leader election problem with an asymptotically optimal round complexity of O(D + log n), for a network of unknown size n and unknown diameter D (but with unique identifiers). Contrary to the best previously known algorithms in the same setting, the proposed one is deterministic. The techniques we introduce give a new insight as to how local constraints on the exchangeable messages can result in efficient algorithms, when dealing with the beeping model. Using this deterministic leader election algorithm, we obtain a randomized leader election algorithm for anonymous networks with an asymptotically optimal round complexity of O(D + log n) w.h.p. In previous works this complexity was obtained in expectation only. Moreover, using deterministic leader election, we obtain efficient algorithms for symmetry-breaking and communication procedures: O(log n) time MIS and 5-coloring for tree networks (which is time-optimal), as well as k-source multi-broadcast for general graphs in O(min(k,log n) * D + k log{(n M)/k}) rounds (for messages in {1,..., M}). This latter result improves on previous solutions when the number of sources k is sublogarithmic (k = o(log n)).
Cite as

Fabien Dufoulon, Janna Burman, and Joffroy Beauquier. Beeping a Deterministic Time-Optimal Leader Election. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{dufoulon_et_al:LIPIcs.DISC.2018.20,
  author =	{Dufoulon, Fabien and Burman, Janna and Beauquier, Joffroy},
  title =	{{Beeping a Deterministic Time-Optimal Leader Election}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{20:1--20:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.20},
  URN =		{urn:nbn:de:0030-drops-98090},
  doi =		{10.4230/LIPIcs.DISC.2018.20},
  annote =	{Keywords: distributed algorithms, leader election, beeping model, time complexity, deterministic algorithms, wireless networks}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.29
Derandomizing Distributed Algorithms with Small Messages: Spanners and Dominating Set

Authors: Mohsen Ghaffari and Fabian Kuhn

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
This paper presents improved deterministic distributed algorithms, with O(log n)-bit messages, for some basic graph problems. The common ingredient in our results is a deterministic distributed algorithm for computing a certain hitting set, which can replace the random part of a number of standard randomized distributed algorithms. This deterministic hitting set algorithm itself is derived using a simple method of conditional expectations. As one main end-result of this derandomized hitting set, we get a deterministic distributed algorithm with round complexity 2^O(sqrt{log n * log log n}) for computing a (2k-1)-spanner of size O~(n^{1+1/k}). This improves considerably on a recent algorithm of Grossman and Parter [DISC'17] which needs O(n^{1/2-1/k} * 2^k) rounds. We also get a 2^O(sqrt{log n * log log n})-round deterministic distributed algorithm for computing an O(log^2 n)-approximation of minimum dominating set; all prior algorithms for this problem were either randomized or required large messages.
Cite as

Mohsen Ghaffari and Fabian Kuhn. Derandomizing Distributed Algorithms with Small Messages: Spanners and Dominating Set. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ghaffari_et_al:LIPIcs.DISC.2018.29,
  author =	{Ghaffari, Mohsen and Kuhn, Fabian},
  title =	{{Derandomizing Distributed Algorithms with Small Messages: Spanners and Dominating Set}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{29:1--29:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.29},
  URN =		{urn:nbn:de:0030-drops-98181},
  doi =		{10.4230/LIPIcs.DISC.2018.29},
  annote =	{Keywords: Distributed Algorithms, Derandomization, Spanners, Dominating Set}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.35
Adapting Local Sequential Algorithms to the Distributed Setting

Authors: Ken-ichi Kawarabayashi and Gregory Schwartzman

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
It is a well known fact that sequential algorithms which exhibit a strong "local" nature can be adapted to the distributed setting given a legal graph coloring. The running time of the distributed algorithm will then be at least the number of colors. Surprisingly, this well known idea was never formally stated as a unified framework. In this paper we aim to define a robust family of local sequential algorithms which can be easily adapted to the distributed setting. We then develop new tools to further enhance these algorithms, achieving state of the art results for fundamental problems. We define a simple class of greedy-like algorithms which we call orderless-local algorithms. We show that given a legal c-coloring of the graph, every algorithm in this family can be converted into a distributed algorithm running in O(c) communication rounds in the CONGEST model. We show that this family is indeed robust as both the method of conditional expectations and the unconstrained submodular maximization algorithm of Buchbinder et al. [Niv Buchbinder et al., 2015] can be expressed as orderless-local algorithms for local utility functions - Utility functions which have a strong local nature to them. We use the above algorithms as a base for new distributed approximation algorithms for the weighted variants of some fundamental problems: Max k-Cut, Max-DiCut, Max 2-SAT and correlation clustering. We develop algorithms which have the same approximation guarantees as their sequential counterparts, up to a constant additive epsilon factor, while achieving an O(log^* n) running time for deterministic algorithms and O(epsilon^{-1}) running time for randomized ones. This improves exponentially upon the currently best known algorithms.
Cite as

Ken-ichi Kawarabayashi and Gregory Schwartzman. Adapting Local Sequential Algorithms to the Distributed Setting. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kawarabayashi_et_al:LIPIcs.DISC.2018.35,
  author =	{Kawarabayashi, Ken-ichi and Schwartzman, Gregory},
  title =	{{Adapting Local Sequential Algorithms to the Distributed Setting}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{35:1--35:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.35},
  URN =		{urn:nbn:de:0030-drops-98245},
  doi =		{10.4230/LIPIcs.DISC.2018.35},
  annote =	{Keywords: Distributed, Approximation Algorithms, Derandomization, Max-Cut}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.40
Congested Clique Algorithms for Graph Spanners

Authors: Merav Parter and Eylon Yogev

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
Graph spanners are sparse subgraphs that faithfully preserve the distances in the original graph up to small stretch. Spanner have been studied extensively as they have a wide range of applications ranging from distance oracles, labeling schemes and routing to solving linear systems and spectral sparsification. A k-spanner maintains pairwise distances up to multiplicative factor of k. It is a folklore that for every n-vertex graph G, one can construct a (2k-1) spanner with O(n^{1+1/k}) edges. In a distributed setting, such spanners can be constructed in the standard CONGEST model using O(k^2) rounds, when randomization is allowed. In this work, we consider spanner constructions in the congested clique model, and show: - a randomized construction of a (2k-1)-spanner with O~(n^{1+1/k}) edges in O(log k) rounds. The previous best algorithm runs in O(k) rounds; - a deterministic construction of a (2k-1)-spanner with O~(n^{1+1/k}) edges in O(log k +(log log n)^3) rounds. The previous best algorithm runs in O(k log n) rounds. This improvement is achieved by a new derandomization theorem for hitting sets which might be of independent interest; - a deterministic construction of a O(k)-spanner with O(k * n^{1+1/k}) edges in O(log k) rounds.
Cite as

Merav Parter and Eylon Yogev. Congested Clique Algorithms for Graph Spanners. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{parter_et_al:LIPIcs.DISC.2018.40,
  author =	{Parter, Merav and Yogev, Eylon},
  title =	{{Congested Clique Algorithms for Graph Spanners}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{40:1--40:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.40},
  URN =		{urn:nbn:de:0030-drops-98298},
  doi =		{10.4230/LIPIcs.DISC.2018.40},
  annote =	{Keywords: Distributed Graph Algorithms, Spanner, Congested Clique}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.41
Lattice Agreement in Message Passing Systems

Authors: Xiong Zheng, Changyong Hu, and Vijay K. Garg

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
This paper studies the lattice agreement problem and the generalized lattice agreement problem in distributed message passing systems. In the lattice agreement problem, given input values from a lattice, processes have to non-trivially decide output values that lie on a chain. We consider the lattice agreement problem in both synchronous and asynchronous systems. For synchronous lattice agreement, we present two algorithms which run in log(f) and min{O(log^2 h(L)), O(log^2 f)} rounds, respectively, where h(L) denotes the height of the input sublattice L, f < n is the number of crash failures the system can tolerate, and n is the number of processes in the system. These algorithms have significant better round complexity than previously known algorithms. The algorithm by Attiya et al. [Attiya et al. DISC, 1995] takes log(n) synchronous rounds, and the algorithm by Mavronicolasa [Mavronicolasa, 2018] takes min{O(h(L)), O(sqrt(f))} rounds. For asynchronous lattice agreement, we propose an algorithm which has time complexity of 2*min{h(L), f + 1} message delays which improves on the previously known time complexity of O(n) message delays. The generalized lattice agreement problem defined by Faleiro et al in [Faleiro et al. PODC, 2012] is a generalization of the lattice agreement problem where it is applied for the replicated state machine. We propose an algorithm which guarantees liveness when a majority of the processes are correct in asynchronous systems. Our algorithm requires min{O(h(L)), O(f)} units of time in the worst case which is better than O(n) units of time required by the algorithm in [Faleiro et al. PODC, 2012].
Cite as

Xiong Zheng, Changyong Hu, and Vijay K. Garg. Lattice Agreement in Message Passing Systems. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 41:1-41:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{zheng_et_al:LIPIcs.DISC.2018.41,
  author =	{Zheng, Xiong and Hu, Changyong and Garg, Vijay K.},
  title =	{{Lattice Agreement in Message Passing Systems}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{41:1--41:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.41},
  URN =		{urn:nbn:de:0030-drops-98301},
  doi =		{10.4230/LIPIcs.DISC.2018.41},
  annote =	{Keywords: Lattice Agreement, Replicated State Machine, Consensus}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2018.47
Brief Announcement: A Tight Lower Bound for Clock Synchronization in Odd-Ary M-Toroids

Authors: Reginald Frank and Jennifer L. Welch

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
In this paper we show a tight closed-form expression for the optimal clock synchronization in k-ary m-cubes with wraparound, where k is odd. This is done by proving a lower bound of 1/4um (k-1/k), where k is the (odd) number of processes in each of the m dimensions, and u is the uncertainty in delay on every link. Our lower bound matches the previously known upper bound.
Cite as

Reginald Frank and Jennifer L. Welch. Brief Announcement: A Tight Lower Bound for Clock Synchronization in Odd-Ary M-Toroids. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 47:1-47:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{frank_et_al:LIPIcs.DISC.2018.47,
  author =	{Frank, Reginald and Welch, Jennifer L.},
  title =	{{Brief Announcement: A Tight Lower Bound for Clock Synchronization in Odd-Ary M-Toroids}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{47:1--47:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.47},
  URN =		{urn:nbn:de:0030-drops-98360},
  doi =		{10.4230/LIPIcs.DISC.2018.47},
  annote =	{Keywords: Clock synchronization, Lower bound, k-ary m-toroid}
}
Document
DOI: 10.4230/LIPIcs.SWAT.2018.9
Tree Containment With Soft Polytomies

Authors: Matthias Bentert, Josef Malík, and Mathias Weller

Published in: LIPIcs, Volume 101, 16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018)

Abstract
The Tree Containment problem has many important applications in the study of evolutionary history. Given a phylogenetic network N and a phylogenetic tree T whose leaves are labeled by a set of taxa, it asks if N and T are consistent. While the case of binary N and T has received considerable attention, the more practically relevant variant dealing with biological uncertainty has not. Such uncertainty manifests itself as high-degree vertices ("polytomies") that are "jokers" in the sense that they are compatible with any binary resolution of their children. Contrasting the binary case, we show that this problem, called Soft Tree Containment, is NP-hard, even if N is a binary, multi-labeled tree in which each taxon occurs at most thrice. On the other hand, we reduce the case that each label occurs at most twice to solving a 2-SAT instance of size O(|T|^3). This implies NP-hardness and polynomial-time solvability on reticulation-visible networks in which the maximum in-degree is bounded by three and two, respectively.
Cite as

Matthias Bentert, Josef Malík, and Mathias Weller. Tree Containment With Soft Polytomies. In 16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 101, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bentert_et_al:LIPIcs.SWAT.2018.9,
  author =	{Bentert, Matthias and Mal{\'\i}k, Josef and Weller, Mathias},
  title =	{{Tree Containment With Soft Polytomies}},
  booktitle =	{16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018)},
  pages =	{9:1--9:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-068-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{101},
  editor =	{Eppstein, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SWAT.2018.9},
  URN =		{urn:nbn:de:0030-drops-88353},
  doi =		{10.4230/LIPIcs.SWAT.2018.9},
  annote =	{Keywords: Phylogenetics, Reticulation-Visible Networks, Multifurcating Trees}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2017.12
Covering Lattice Points by Subspaces and Counting Point-Hyperplane Incidences

Authors: Martin Balko, Josef Cibulka, and Pavel Valtr

Published in: LIPIcs, Volume 77, 33rd International Symposium on Computational Geometry (SoCG 2017)

Abstract
Let d and k be integers with 1 <= k <= d-1. Let Lambda be a d-dimensional lattice and let K be a d-dimensional compact convex body symmetric about the origin. We provide estimates for the minimum number of k-dimensional linear subspaces needed to cover all points in the intersection of Lambda with K. In particular, our results imply that the minimum number of k-dimensional linear subspaces needed to cover the d-dimensional n * ... * n grid is at least Omega(n^(d(d-k)/(d-1)-epsilon)) and at most O(n^(d(d-k)/(d-1))), where epsilon > 0 is an arbitrarily small constant. This nearly settles a problem mentioned in the book of Brass, Moser, and Pach. We also find tight bounds for the minimum number of k-dimensional affine subspaces needed to cover the intersection of Lambda with K. We use these new results to improve the best known lower bound for the maximum number of point-hyperplane incidences by Brass and Knauer. For d > =3 and epsilon in (0,1), we show that there is an integer r=r(d,epsilon) such that for all positive integers n, m the following statement is true. There is a set of n points in R^d and an arrangement of m hyperplanes in R^d with no K_(r,r) in their incidence graph and with at least Omega((mn)^(1-(2d+3)/((d+2)(d+3)) - epsilon)) incidences if d is odd and Omega((mn)^(1-(2d^2+d-2)/((d+2)(d^2+2d-2)) - epsilon)) incidences if d is even.
Cite as

Martin Balko, Josef Cibulka, and Pavel Valtr. Covering Lattice Points by Subspaces and Counting Point-Hyperplane Incidences. In 33rd International Symposium on Computational Geometry (SoCG 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 77, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{balko_et_al:LIPIcs.SoCG.2017.12,
  author =	{Balko, Martin and Cibulka, Josef and Valtr, Pavel},
  title =	{{Covering Lattice Points by Subspaces and Counting Point-Hyperplane Incidences}},
  booktitle =	{33rd International Symposium on Computational Geometry (SoCG 2017)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-038-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{77},
  editor =	{Aronov, Boris and Katz, Matthew J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2017.12},
  URN =		{urn:nbn:de:0030-drops-71955},
  doi =		{10.4230/LIPIcs.SoCG.2017.12},
  annote =	{Keywords: lattice point, covering, linear subspace, point-hyperplane incidence}
}
  • Refine by Author
  • 2 Jakubův, Jan
  • 2 Kaliszyk, Cezary
  • 2 Malík, Josef
  • 2 Urban, Josef
  • 1 Afek, Yehuda
  • Show More...

  • Refine by Classification
  • 7 Theory of computation → Distributed algorithms
  • 3 Theory of computation → Distributed computing models
  • 2 Theory of computation → Automated reasoning
  • 1 Applied computing → Biological networks
  • 1 Computing methodologies → Multi-agent planning
  • Show More...

  • Refine by Keyword
  • 2 Derandomization
  • 2 ENIGMA
  • 2 leader election
  • 1 Approximation Algorithms
  • 1 Automated Reasoning
  • Show More...

  • Refine by Type
  • 15 document

  • Refine by Publication Year
  • 12 2018
  • 1 2017
  • 1 2022
  • 1 2023

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