Document Open Access Logo

Searching for Smallest Universal Graphs and Tournaments with SAT

Authors Tianwei Zhang , Stefan Szeider

PDF
Thumbnail PDF

File

LIPIcs.CP.2023.39.pdf
  • Filesize: 0.87 MB
  • 20 pages

Document Identifiers

Author Details

Tianwei Zhang
  • Algorithms and Complexity Group, TU Wien, Austria
Stefan Szeider
  • Algorithms and Complexity Group, TU Wien, Austria

Funding

The project leading to this publication has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No. 101034440, and was supported by the Vienna Science and Technology Fund (WWTF) within the project ICT19-065.

Acknowledgements

This work was carried out in part while the second author visited the Simons Institute for the Theory of Computing, University of Berkeley, within the program Extended Reunion: Satisfiability. The authors thank Ciaran McCreesh for advising them to use and modify the Glasgow subgraph solver.

Cite AsGet BibTex

Tianwei Zhang and Stefan Szeider. Searching for Smallest Universal Graphs and Tournaments with SAT. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 39:1-39:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CP.2023.39

Abstract

A graph is induced k-universal if it contains all graphs of order k as an induced subgraph. For over half a century, the question of determining smallest k-universal graphs has been studied. A related question asks for a smallest k-universal tournament containing all tournaments of order k. This paper proposes and compares SAT-based methods for answering these questions exactly for small values of k. Our methods scale to values for which a generate-and-test approach isn't feasible; for instance, we show that an induced 7-universal graph has more than 16 vertices, whereas the number of all connected graphs on 16 vertices, modulo isomorphism, is a number with 23 decimal digits Our methods include static and dynamic symmetry breaking and lazy encodings, employing external subgraph isomorphism testing.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Extremal graph theory
  • Software and its engineering → Constraint and logic languages
  • Hardware → Theorem proving and SAT solving
  • Mathematics of computing → Graph enumeration
Keywords
  • Constrained-based combinatorics
  • synthesis problems
  • symmetry breaking
  • SAT solving
  • subgraph isomorphism
  • tournament
  • directed graphs

Metrics

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

Supplementary Materials

References

  1. Noga Alon. Asymptotically optimal induced universal graphs. Geom. Funct. Anal., 27(1):1-32, 2017. URL: https://doi.org/10.1007/s00039-017-0396-9.
  2. Stephen Alstrup, Haim Kaplan, Mikkel Thorup, and Uri Zwick. Adjacency labeling schemes and induced-universal graphs. In Rocco A. Servedio and Ronitt Rubinfeld, editors, Proceedings of the Forty-Seventh Annual ACM on Symposium on Theory of Computing, STOC 2015, Portland, OR, USA, June 14-17, 2015, pages 625-634. ACM, 2015. URL: https://doi.org/10.1145/2746539.2746545.
  3. Kenneth Appel and Wolfgang Haken. The solution of the four-color-map problem. Sci. Amer., 237(4):108-121, 152, 1977. URL: https://doi.org/10.1038/scientificamerican1077-108.
  4. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51-53. University of Helsinki, 2020. URL: https://tuhat.helsinki.fi/ws/files/142452772/sc2020_proceedings.pdf.
  5. Cayden R. Codel. Verifying SAT encodings in lean. Master’s thesis, Computer Science Department School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213, May 2022. URL: http://reports-archive.adm.cs.cmu.edu/anon/2022/CMU-CS-22-106.pdf.
  6. Luís Cruz-Filipe, João Marques-Silva, and Peter Schneider-Kamp. Formally verifying the solution to the boolean Pythagorean triples problem. Journal of Automated Reasoning, 63(3):695-722, 2019. URL: https://doi.org/10.1007/s10817-018-9490-4.
  7. 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. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  8. 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.
  9. Sofia Giljegård and Johan Wennerbeck. Puzzle solving with proof - writing a verified SAT encoding chain in HOL4. Master’s thesis, Chalmers University of Technology and University of Gothenburg, 2021. URL: https://hdl.handle.net/20.500.12380/304104.
  10. Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Subgraph isomorphism meets cutting planes: Solving with certified solutions. In Christian Bessiere, editor, Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, pages 1134-1140. ijcai.org, 2020. URL: https://doi.org/10.24963/ijcai.2020/158.
  11. Geňa Hahn and Claude Tardif. Graph homomorphisms: structure and symmetry. In Geňa Hahn and Gert Sabidussi, editors, Graph Symmetry, pages 107-166. Kluwer Academic Publishers, Dortrecht, 1997. Google Scholar
  12. Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, and Nathan Wetzler. Efficient, verified checking of propositional proofs. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, volume 10499 of Lecture Notes in Computer Science, pages 269-284. Springer Verlag, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_18.
  13. Marijn J. H. Heule and Oliver Kullmann. The science of brute force. Communications of the ACM, 60(8):70-79, 2017. URL: https://doi.org/10.1145/3107239.
  14. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In SAT, pages 428-437, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
  15. 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.
  16. Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. SAT-based generation of planar graphs. 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. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  17. Markus Kirchweger and Stefan Szeider. SAT modulo symmetries for graph generation. In Laurent D. Michel, editor, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), Leibniz International Proceedings in Informatics (LIPIcs), pages 39:1-39:17. Dagstuhl, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.34.
  18. Evan Lohn, Chris Lambert, and Marijn J. H. Heule. Compact symmetry breaking for tournaments. In Alberto Griggio and Neha Rungta, editors, 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, pages 179-188. IEEE, 2022. URL: https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_24.
  19. Ciaran McCreesh, Patrick Prosser, and James Trimble. The Glasgow subgraph solver: Using constraint programming to tackle hard subgraph isomorphism problem variants. In Fabio Gadducci and Timo Kehrer, editors, Graph Transformation - 13th International Conference, ICGT 2020, Held as Part of STAF 2020, Bergen, Norway, June 25-26, 2020, Proceedings, volume 12150 of Lecture Notes in Computer Science, pages 316-324. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51372-6_19.
  20. 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.
  21. Jhon W. Moon. On minimal n-universal graphs. Proc. Glasgow Math. Assoc., 7:32-33 (1965), 1965. URL: https://doi.org/10.1017/S2040618500035139.
  22. John W. Moon. Topics on tournaments. Holt, Rinehart and Winston, New York-Montreal, Que.-London, 1968. Google Scholar
  23. OEIS Foundation Inc. The On-Line Encyclopedia of Integer Sequences. Published electronically at URL: http://oeis.org.
  24. James Preen. What is the smallest graph that contains all non-isomorphic 4-node and 5-node connected graphs as induced subgraphs? online, October 2011. Mathematics Stack Exchange, https://math.stackexchange.com/q/75513, last edited 2020-04-25.
  25. Richard Rado. Universal graphs and universal functions. Acta Arithmetica, 9(4):331-340, 1964. URL: http://eudml.org/doc/207488.
  26. James Trimble. Induced universal graphs for families of small graphs. CoRR, abs/2109.00075, 2021. URL: https://doi.org/10.48550/arXiv.2109.00075.
  27. 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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact