5 Search Results for "Piperno, Adolfo"

Document
DOI: 10.4230/LIPIcs.ITP.2024.16
A Formal Proof of R(4,5)=25

Authors: Thibault Gauthier and Chad E. Brown

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The authors have performed the computational parts of the proof with different implementations in order to reduce the possibility of an error in their programs. In this work, we prove this theorem in the interactive theorem prover HOL4 limiting the uncertainty to the small HOL4 kernel. Instead of verifying their algorithms directly, we rely on the HOL4 interface to MiniSat to prove gluing lemmas. To reduce the number of such lemmas and thus make the computational part of the proof feasible, we implement a generalization algorithm. We verify that its output covers all the possible cases by implementing a custom SAT-solver extended with a graph isomorphism checker.
Cite as

Thibault Gauthier and Chad E. Brown. A Formal Proof of R(4,5)=25. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gauthier_et_al:LIPIcs.ITP.2024.16,
  author =	{Gauthier, Thibault and Brown, Chad E.},
  title =	{{A Formal Proof of R(4,5)=25}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.16},
  URN =		{urn:nbn:de:0030-drops-207446},
  doi =		{10.4230/LIPIcs.ITP.2024.16},
  annote =	{Keywords: Ramsey numbers, SAT solvers, symmetry breaking, generalization, HOL4}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.3
The Complexity of Symmetry Breaking Beyond Lex-Leader

Authors: Markus Anders, Sofia Brenner, and Gaurav Rattan

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Symmetry breaking is a widely popular approach to enhance solvers in constraint programming, such as those for SAT or MIP. Symmetry breaking predicates (SBPs) typically impose an order on variables and single out the lexicographic leader (lex-leader) in each orbit of assignments. Although it is NP-hard to find complete lex-leader SBPs, incomplete lex-leader SBPs are widely used in practice. In this paper, we investigate the complexity of computing complete SBPs, lex-leader or otherwise, for SAT. Our main result proves a natural barrier for efficiently computing SBPs: efficient certification of graph non-isomorphism. Our results explain the difficulty of obtaining short SBPs for important CP problems, such as matrix-models with row-column symmetries and graph generation problems. Our results hold even when SBPs are allowed to introduce additional variables. We show polynomial upper bounds for breaking certain symmetry groups, namely automorphism groups of trees and wreath products of groups with efficient SBPs.
Cite as

Markus Anders, Sofia Brenner, and Gaurav Rattan. The Complexity of Symmetry Breaking Beyond Lex-Leader. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.CP.2024.3,
  author =	{Anders, Markus and Brenner, Sofia and Rattan, Gaurav},
  title =	{{The Complexity of Symmetry Breaking Beyond Lex-Leader}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{3:1--3:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.3},
  URN =		{urn:nbn:de:0030-drops-206881},
  doi =		{10.4230/LIPIcs.CP.2024.3},
  annote =	{Keywords: symmetry breaking, boolean satisfiability, matrix models, graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.4
Satsuma: Structure-Based Symmetry Breaking in SAT

Authors: Markus Anders, Sofia Brenner, and Gaurav Rattan

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Symmetry reduction is crucial for solving many interesting SAT instances in practice. Numerous approaches have been proposed, which try to strike a balance between symmetry reduction and computational overhead. Arguably the most readily applicable method is the computation of static symmetry breaking constraints: a constraint restricting the search-space to non-symmetrical solutions is added to a given SAT instance. A distinct advantage of static symmetry breaking is that the SAT solver itself is not modified. A disadvantage is that the strength of symmetry reduction is usually limited. In order to boost symmetry reduction, the state-of-the-art tool BreakID [Devriendt et. al] pioneered the identification and tailored breaking of a particular substructure of symmetries, the so-called row interchangeability groups. In this paper, we propose a new symmetry breaking tool called satsuma. The core principle of our tool is to exploit more diverse but frequently occurring symmetry structures. This is enabled by new practical detection algorithms for row interchangeability, row-column symmetry, Johnson symmetry, and various combinations. Based on the resulting structural description, we then produce symmetry breaking constraints. We compare this new approach to BreakID on a range of instance families exhibiting symmetry. Our benchmarks suggest improved symmetry reduction in the presence of Johnson symmetry and comparable performance in the presence of row-column symmetry. Moreover, our implementation runs significantly faster, even though it identifies more diverse structures.
Cite as

Markus Anders, Sofia Brenner, and Gaurav Rattan. Satsuma: Structure-Based Symmetry Breaking in SAT. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.SAT.2024.4,
  author =	{Anders, Markus and Brenner, Sofia and Rattan, Gaurav},
  title =	{{Satsuma: Structure-Based Symmetry Breaking in SAT}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.4},
  URN =		{urn:nbn:de:0030-drops-205269},
  doi =		{10.4230/LIPIcs.SAT.2024.4},
  annote =	{Keywords: symmetry breaking, boolean satisfiability, graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.ESA.2021.6
Parallel Computation of Combinatorial Symmetries

Authors: Markus Anders and Pascal Schweitzer

Published in: LIPIcs, Volume 204, 29th Annual European Symposium on Algorithms (ESA 2021)

Abstract
In practice symmetries of combinatorial structures are computed by transforming the structure into an annotated graph whose automorphisms correspond exactly to the desired symmetries. An automorphism solver is then employed to compute the automorphism group of the constructed graph. Such solvers have been developed for over 50 years, and highly efficient sequential, single core tools are available. However no competitive parallel tools are available for the task. We introduce a new parallel randomized algorithm that is based on a modification of the individualization-refinement paradigm used by sequential solvers. The use of randomization crucially enables parallelization. We report extensive benchmark results that show that our solver is competitive to state-of-the-art solvers on a single thread, while scaling remarkably well with the use of more threads. This results in order-of-magnitude improvements on many graph classes over state-of-the-art solvers. In fact, our tool is the first parallel graph automorphism tool that outperforms current sequential tools.
Cite as

Markus Anders and Pascal Schweitzer. Parallel Computation of Combinatorial Symmetries. In 29th Annual European Symposium on Algorithms (ESA 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 204, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.ESA.2021.6,
  author =	{Anders, Markus and Schweitzer, Pascal},
  title =	{{Parallel Computation of Combinatorial Symmetries}},
  booktitle =	{29th Annual European Symposium on Algorithms (ESA 2021)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-204-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{204},
  editor =	{Mutzel, Petra and Pagh, Rasmus 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.2021.6},
  URN =		{urn:nbn:de:0030-drops-145875},
  doi =		{10.4230/LIPIcs.ESA.2021.6},
  annote =	{Keywords: graph isomorphism, automorphism groups, algorithm engineering, parallel algorithms}
}
Document
DOI: 10.4230/LIPIcs.SEA.2018.30
Isomorphism Test for Digraphs with Weighted Edges

Authors: Adolfo Piperno

Published in: LIPIcs, Volume 103, 17th International Symposium on Experimental Algorithms (SEA 2018)

Abstract
Colour refinement is at the heart of all the most efficient graph isomorphism software packages. In this paper we present a method for extending the applicability of refinement algorithms to directed graphs with weighted edges. We use {Traces} as a reference software, but the proposed solution is easily transferrable to any other refinement-based graph isomorphism tool in the literature. We substantiate the claim that the performances of the original algorithm remain substantially unchanged by showing experiments for some classes of benchmark graphs.
Cite as

Adolfo Piperno. Isomorphism Test for Digraphs with Weighted Edges. In 17th International Symposium on Experimental Algorithms (SEA 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 103, pp. 30:1-30:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{piperno:LIPIcs.SEA.2018.30,
  author =	{Piperno, Adolfo},
  title =	{{Isomorphism Test for Digraphs with Weighted Edges}},
  booktitle =	{17th International Symposium on Experimental Algorithms (SEA 2018)},
  pages =	{30:1--30:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-070-5},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{103},
  editor =	{D'Angelo, Gianlorenzo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2018.30},
  URN =		{urn:nbn:de:0030-drops-89659},
  doi =		{10.4230/LIPIcs.SEA.2018.30},
  annote =	{Keywords: Practical Graph Isomorphism, Weighted Directed Graphs, Partition Refinement}
}
  • Refine by Author
  • 3 Anders, Markus
  • 2 Brenner, Sofia
  • 2 Rattan, Gaurav
  • 1 Brown, Chad E.
  • 1 Gauthier, Thibault
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Combinatorial algorithms
  • 1 Mathematics of computing → Graph algorithms
  • 1 Mathematics of computing → Graph theory
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Graph algorithms analysis
  • Show More...

  • Refine by Keyword
  • 3 graph isomorphism
  • 3 symmetry breaking
  • 2 boolean satisfiability
  • 1 HOL4
  • 1 Partition Refinement
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 3 2024
  • 1 2018
  • 1 2021

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