State Canonization and Early Pruning in Width-Based Automated Theorem Proving

Authors Mateus de Oliveira Oliveira , Farhad Vadiee



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.33.pdf
  • Filesize: 0.87 MB
  • 17 pages

Document Identifiers

Author Details

Mateus de Oliveira Oliveira
  • Department of Computer and Systems Sciences, Stockholm University, Sweden
  • Department of Informatics, University of Bergen, Norway
Farhad Vadiee
  • Department of Informatics, University of Bergen, Norway

Cite AsGet BibTex

Mateus de Oliveira Oliveira and Farhad Vadiee. State Canonization and Early Pruning in Width-Based Automated Theorem Proving. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 33:1-33:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.33

Abstract

Width-based automated theorem proving is a framework where counter-examples for graph theoretic conjectures are searched width-wise relative to some graph width measure, such as treewidth or pathwidth. In a recent work it has been shown that dynamic programming algorithms operating on tree decompositions can be combined together with the purpose of width-based theorem proving. This approach can be used to show that several long-standing conjectures in graph theory can be tested in time 2^{2^{k^{O(1)}}} on the class of graphs of treewidth at most k. In this work, we give the first steps towards evaluating the viability of this framework from a practical standpoint. At the same time, we advance the framework in two directions. First, we introduce a state-canonization technique that significantly reduces the number of states evaluated during the search for a counter-example of the conjecture. Second, we introduce an early-pruning technique that can be applied in the study of conjectures of the form ℙ₁ → ℙ₂, for graph properties ℙ₁ and ℙ₂, where ℙ₁ is a property closed under subgraphs. As a concrete application, we use our framework in the study of graph theoretic conjectures related to coloring triangle free graphs. In particular, our algorithm is able to show that Reed’s conjecture for triangle free graphs is valid on the class of graphs of pathwidth at most 5, and on graphs of treewidth at most 3. Perhaps more interestingly, our algorithm is able to construct in a completely automated way counter-examples for non-valid strengthenings of Reed’s conjecture. These are the first results showing that width-based automated theorem proving is a promising avenue in the study of graph-theoretic conjectures.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Parameterized complexity and exact algorithms
Keywords
  • Width-Based Automated Theorem Proving
  • Dynamic Programming
  • Parameterized Complexity

Metrics

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

References

  1. Therese C. Biedl. On triangulating k-outerplanar graphs. Discret. Appl. Math., 181(1):275-279, 2015. URL: https://doi.org/10.1016/j.dam.2014.10.017.
  2. Hans L. Bodlaender. Classes of graphs with bounded tree-width, volume 86. Unknown Publisher, 1986. Google Scholar
  3. Hans L Bodlaender and Fedor V Fomin. Equitable colorings of bounded treewidth graphs. Theoretical Computer Science, 349(1):22-30, 2005. Google Scholar
  4. Béla Bollobás, Paul A Catlin, and Paul Erdös. Hadwiger’s conjecture is true for almost every graph. Eur. J. Comb., 1(3):195-199, 1980. Google Scholar
  5. Andreas Brandstädt, Van Bang Le, and Jeremy P Spinrad. Graph classes: a survey. SIAM, 1999. Google Scholar
  6. CN Campos and Yoshiko Wakabayashi. On dominating sets of maximal outerplanar graphs. Discrete Applied Mathematics, 161(3):330-335, 2013. Google Scholar
  7. Bruno Courcelle. The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Information and Computation, 85(1):12-75, 1990. URL: https://doi.org/10.1016/0890-5401(90)90043-H.
  8. Bruno Courcelle and Irène Durand. Automata for the verification of monadic second-order graph properties. Journal of applied logic, 10(4):368-409, 2012. Google Scholar
  9. Mateus de Oliveira Oliveira and Farhad Vadiee. From width-based model checking to width-based automated theorem proving. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 37(5), pages 6297-6304, 2023. Google Scholar
  10. Zdeněk Dvořák and Ken-ichi Kawarabayashi. Triangle-free graphs of tree-width t are ⌈ (t+ 3)/ 2 ⌉-colorable. European Journal of Combinatorics, 66:95-100, 2017. Google Scholar
  11. DJ Guan and Xuding Zhu. Game chromatic number of outerplanar graphs. Journal of Graph Theory, 30(1):67-70, 1999. Google Scholar
  12. Daniel Heldt, Kolja Knauer, and Torsten Ueckerdt. On the bend-number of planar and outerplanar graphs. Discrete Applied Mathematics, 179:109-119, 2014. Google Scholar
  13. Pavol Hell and Xuding Zhu. The circular chromatic number of series-parallel graphs. Journal of Graph Theory, 33(1):14-24, 2000. Google Scholar
  14. Jesper Lykke Jacobsen and Jesús Salas. Is the five-flow conjecture almost false? Journal of Combinatorial Theory, Series B, 103(4):532-565, 2013. Google Scholar
  15. Frank Kammer. Determining the smallest k such that g is k-outerplanar. In European Symposium on Algorithms, pages 359-370. Springer, 2007. Google Scholar
  16. Ton Kloks. Treewidth: computations and approximations. Springer, 1994. Google Scholar
  17. Zhishi Pan and Xuding Zhu. Tight relation between the circular chromatic number and the girth of series-parallel graphs. Discrete mathematics, 254(1-3):393-404, 2002. Google Scholar
  18. Léo Vieira Peres and Ricardo Dahab. Tutte’s 3-flow conjecture for almost even graphs. Procedia Computer Science, 195:280-288, 2021. Google Scholar
  19. Alexandre Pinlou and Éric Sopena. Oriented vertex and arc colorings of outerplanar graphs. Information Processing Letters, 100(3):97-104, 2006. Google Scholar
  20. Andrzej Proskurowski and Jan Arne Telle. From bandwidth to pathwidth k. _THEORETICAL-E, page 90, 1996. Google Scholar
  21. Bruce Reed. ω, δ, and χ. Journal of Graph Theory, 27(4):177-212, 1998. Google Scholar
  22. Bo Zhou. Upper bounds for the zagreb indices and the spectral radius of series-parallel graphs. International Journal of Quantum Chemistry, 107(4):875-878, 2007. Google Scholar