Document Open Access Logo

A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture

Authors Markus Kirchweger , Tomáš Peitl, Stefan Szeider

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.13.pdf
  • Filesize: 0.75 MB
  • 17 pages

Document Identifiers

Author Details

Markus Kirchweger
  • Algorithms and Complexity Group, TU Wien, Austria
Tomáš Peitl
  • Algorithms and Complexity Group, TU Wien, Austria
Stefan Szeider
  • Algorithms and Complexity Group, TU Wien, Austria

Funding

This work was supported by the Austrian Science Fund (FWF, project P32441), and the Vienna Science and Technology Fund (WWTF, project ICT19-065).

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.SAT.2023.13

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Mathematics of computing → Hypergraphs
  • Mathematics of computing → Graph coloring
  • Mathematics of computing → Graph enumeration
  • Mathematics of computing → Matchings and factors
Keywords
  • hypergraphs
  • graph coloring
  • SAT modulo symmetries

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Claude Berge. On the chromatic index of a linear hypergraph and the Chvátal conjecture. Annals of the New York Academy of Sciences, 555(1):40-44, 1989. Google Scholar
  2. Anton Betten and Dieter Betten. Linear spaces with at most 12 points. Journal of Combinatorial Designs, 7(2):119-145, 1999. Google Scholar
  3. William I. Chang and Eugene L. Lawler. Edge coloring of hypergraphs and a conjecture of Erdős, Faber, Lovász. Combinatorica, 8(3):293-295, 1988. Google Scholar
  4. Michael Codish, Alice Miller, Patrick Prosser, and Peter J. Stuckey. Constraints for symmetry breaking in graph representation. Constraints, 24(1):1-24, 2019. URL: https://doi.org/10.1007/s10601-018-9294-5.
  5. James M. Crawford, Matthew L. Ginsberg, Eugene M. Luks, and Amitabha Roy. Symmetry-breaking predicates for search problems. In Stuart C. Shapiro Luigia Carlucci Aiello, Jon Doyle, editor, Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR'96), Cambridge, Massachusetts, USA, November 5-8, 1996, pages 148-159. Morgan Kaufmann, 1996. Google Scholar
  6. Paul Erdős. Problems and results in graph theory and combinatorial analysis. Proc. British Combinatorial Conj., 5th, pages 169-192, 1975. Google Scholar
  7. Pául Erdős. On the combinatorial problems which I would most like to see solved. Combinatorica, 1(1):25-42, 1981. Google Scholar
  8. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: User propagators for CDCL. In Meena Mahajan and Friedrich Slivovsky, editors, The 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), July 04-08, 2023, Alghero, Italy, LIPIcs, pages 8:1-8:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.8.
  9. Johannes K. Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r)evolution of SAT. Communications of the ACM, 66(6):64-72, June 2023. URL: https://doi.org/10.1145/3560469.
  10. Zoltán Füredi. The chromatic index of simple hypergraphs. Graphs and Combinatorics, 2(1):89-92, 1986. Google Scholar
  11. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  12. Neil Hindman. On a conjecture of Erdős, Faber, and Lovász about n-colorings. Canadian Journal of Mathematics, 33(3):563-570, 1981. URL: https://doi.org/10.4153/CJM-1981-046-9.
  13. Jeff Kahn. Coloring nearly-disjoint hypergraphs with n+ o (n) colors. Journal of combinatorial theory, Series A, 59(1):31-39, 1992. Google Scholar
  14. Jeff Kahn. Asymptotics of hypergraph matching, covering and coloring problems. In Proceedings of the International Congress of Mathematicians: August 3-11, 1994 Zürich, Switzerland, pages 1353-1362. Springer, 1995. Google Scholar
  15. Jeff Kahn. On some hypergraph problems of Paul Erdős and the asymptotics of matchings, covers and colorings. The Mathematics of Paul Erdős I, pages 345-371, 1997. Google Scholar
  16. Jeff Kahn and Paul D. Seymour. A fractional version of the Erdős-Faber-Lovász conjecture. Combinatorica, 12(2):155-160, 1992. Google Scholar
  17. Dong Yeap Kang, Tom Kelly, Daniela Kühn, Abhishek Methuku, and Deryk Osthus. A proof of the Erdős-Faber-Lovász conjecture, 2021. URL: https://doi.org/10.48550/arXiv.2101.04698.
  18. Markus Kirchweger, Tomáš Peitl, and Stefan Szeider. Co-certificate learning with SAT modulo symmetries. In Proceedings of the 34th International Joint Conference on Artificial Intelligence, IJCAI 2023. AAAI Press/IJCAI, 2023. To appear. Google Scholar
  19. Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. A SAT attack on Rota’s Basis Conjecture. In Theory and Applications of Satisfiability Testing - SAT 2022 - 25th International Conference, Haifa, Israel, August 2-5, 2022, Proceedings, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.4.
  20. Markus Kirchweger and Stefan Szeider. SAT modulo symmetries for graph generation. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), LIPIcs, pages 39:1-39:17. Dagstuhl, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.34.
  21. Brendan D. McKay and Adolfo Piperno. Practical graph isomorphism, II. J. Symbolic Comput., 60:94-112, 2014. URL: https://doi.org/10.1016/j.jsc.2013.09.003.
  22. David Romero and Federico Alonso-Pecina. The Erdős–Faber–Lovász conjecture is true for n ≤ 12. Discrete Mathematics, Algorithms and Applications, 06(03):1450039, 2014. URL: https://doi.org/10.1142/S1793830914500396.
  23. Paul D. Seymour. Packing nearly-disjoint sets. Combinatorica, 2:91-97, 1982. Google Scholar
  24. Carsten Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. In Peter van Beek, editor, Principles and Practice of Constraint Programming - CP 2005, 11th International Conference, CP 2005, Sitges, Spain, October 1-5, 2005, Proceedings, volume 3709 of Lecture Notes in Computer Science, pages 827-831. Springer Verlag, 2005. URL: https://doi.org/10.1007/11564751_73.
  25. Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Theory and Applications of Satisfiability Testing - SAT 2014, volume 8561 of Lecture Notes in Computer Science, pages 422-429. Springer Verlag, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
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 About DROPS Imprint Privacy Contact