<div class="csl-bib-body">
<div class="csl-entry">Kirchweger, M., Peitl, T., & Szeider, S. (2023). A SAT Solver’s Opinion on the Erdos-Faber-Lovász Conjecture. In M. Mahajan (Ed.), <i>26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)</i> (pp. 1–17). Schloss-Dagstuhl - Leibniz Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SAT.2023.13</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/190010
-
dc.description.abstract
In 1972, Paul Erdos, 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. Erdos 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.
en
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
Leibniz International Proceedings in Informatics (LIPIcs)
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
graph coloring
en
dc.subject
hypergraphs
en
dc.subject
SAT modulo symmetries
en
dc.title
A SAT Solver's Opinion on the Erdos-Faber-Lovász Conjecture
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.contributor.editoraffiliation
Institute of Mathematical Sciences, HBNI,India
-
dc.relation.isbn
978-3-95977-286-0
-
dc.relation.issn
1868-8969
-
dc.description.startpage
1
-
dc.description.endpage
17
-
dc.relation.grantno
ICT19-065
-
dc.relation.grantno
P32441-N35
-
dc.rights.holder
Markus Kirchweger, Tomáš Peitl, and Stefan Szeider;
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
-
tuw.container.volume
271
-
tuw.peerreviewed
true
-
tuw.book.ispartofseries
Leibniz International Proceedings in Informatics
-
tuw.relation.publisher
Schloss-Dagstuhl - Leibniz Zentrum für Informatik
-
tuw.book.chapter
13
-
tuw.project.title
Revealing and Utilizing the Hidden Structure for Solving Hard Problems in AI