Document Open Access Logo

The 3-Decomposition Conjecture: A SAT-Based Approach with Specialized Propagators

Authors Tianwei Zhang , Stefan Szeider

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CP.2025.39.pdf
  • Filesize: 1.7 MB
  • 19 pages
HTML5 Logo HTML (experimental)
LIPIcs.CP.2025.39.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Mathematics of computing → Graph theory
  • Theory of computation → Logic and verification
  • Mathematics of computing → Combinatorics
  • Theory of computation → Automated reasoning
  • Mathematics of computing → Graph algorithms
Keywords
  • SAT
  • Symmetry Breaking
  • Subgraphs
  • Propagators
  • Combinatorics

Metrics

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

Abstract

We investigate the 3-decomposition conjecture, which states that every connected cubic graph can be decomposed into a spanning tree, a collection of cycles, and a matching. Using a SAT-based approach enhanced with specialized propagators, we verify the conjecture for all relevant graphs up to 28 vertices. Our method extends the Satisfiability Modulo Symmetries (SMS) framework with specialized propagators that exploit theoretical properties of minimal counterexamples (counterexamples with the minimal number of vertices), enabling efficient pruning. We demonstrate that graphs containing certain substructures cannot be minimal counterexamples to the conjecture, allowing us to exclude these patterns during the search dynamically. Our experimental results quantify the impact of different propagator configurations and forbidden subgraph constraints on solving efficiency, showing significant performance improvements when leveraging these techniques. The approach scales effectively to graphs of 28 vertices. Our work illustrates how combining SAT solving with specialized constraint propagation techniques can successfully address challenging combinatorial problems in contemporary graph theory.

Cite As Get BibTex

Tianwei Zhang and Stefan Szeider. The 3-Decomposition Conjecture: A SAT-Based Approach with Specialized Propagators. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 39:1-39:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CP.2025.39

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 the grant agreement No. 101034440 and was supported by the Austrian Science Fund (FWF) within the project 10.55776/P36688.

Supplementary Materials

References

  1. Elham Aboomahigir, Milad Ahanjideh, and Saieed Akbari. Decomposing claw-free subcubic graphs and 4-chordal subcubic graphs. Discret. Appl. Math., 296:52-55, 2021. URL: https://doi.org/10.1016/J.DAM.2020.01.016.
  2. Saieed Akbari, Tommy R. Jensen, and Mark H. Siggers. Decompositions of graphs into trees, forests, and regular subgraphs. Discret. Math., 338(8):1322-1327, 2015. URL: https://doi.org/10.1016/J.DISC.2015.02.021.
  3. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks and their applications. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 167-180. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_18.
  4. Oliver Bachtler and Irene Heinrich. Reductions for the 3-decomposition conjecture. Procedia Computer Science, 223:96-103, 2023. XII Latin-American Algorithms, Graphs and Optimization Symposium (LAGOS 2023). URL: https://doi.org/10.1016/j.procs.2023.08.218.
  5. Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias S. Kotsireas, and Vijay Ganesh. A sat-based resolution of Lam’s problem. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 3669-3676. AAAI Press, 2021. URL: https://doi.org/10.1609/AAAI.V35I5.16483.
  6. Peter J. Cameron. Research problems from the BCC22. Discrete Mathematics, 311(13):1074-1083, 2011. Selected Papers from the 22nd British Combinatorial Conference. URL: https://doi.org/10.1016/j.disc.2011.02.024.
  7. Michael Codish, Michael Frank, Avraham Itzhakov, and Alice Miller. Computing the Ramsey number R(4, 3, 3) using abstraction and symmetry breaking. Constraints An Int. J., 21(3):375-393, 2016. URL: https://doi.org/10.1007/S10601-016-9240-3.
  8. 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.
  9. Genghua Fan and Chuixiang Zhou. Hoffmann-Ostenhof’s 3-decomposition conjecture. Discrete Mathematics, 348(7):114454, 2025. URL: https://doi.org/10.1016/j.disc.2025.114454.
  10. Johannes K. Fichte, Markus Hecher, Daniel Le Berre, 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.
  11. The OEIS Foundation. Number of connected cubic unlabeled graphs with n nodes. URL: https://oeis.org/A002851.
  12. Marijn Heule, Warren Hunt, 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, pages 269-284, Cham, 2017. Springer International Publishing. Google Scholar
  13. Marijn J. H. Heule, Oliver Kullmann, and Armin Biere. Cube-and-conquer for satisfiability. In Youssef Hamadi and Lakhdar Sais, editors, Handbook of Parallel Constraint Reasoning, pages 31-59. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-63516-3_2.
  14. Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the Boolean Pythagorean Triples problem via cube-and-conquer. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 228-245. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  15. Arthur Hoffmann-Ostenhof, Tomáš Kaiser, and Kenta Ozeki. Decomposing planar cubic graphs. Journal of Graph Theory, 88(4):631-640, 2018. URL: https://doi.org/10.1002/jgt.22234.
  16. Markus Kirchweger, Tomáš Peitl, and Stefan Szeider. Co-certificate learning with SAT modulo symmetries. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 1944-1953. ijcai.org, 2023. Main Track. URL: https://doi.org/10.24963/IJCAI.2023/216.
  17. 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.
  18. Markus Kirchweger and Stefan Szeider. SAT modulo symmetries for graph generation and enumeration. ACM Trans. Comput. Log., 25(3):1-30, 2024. URL: https://doi.org/10.1145/3670405.
  19. Panpan Li and Wenzhong Liu. Decompositions of cubic traceable graphs. Discuss. Math. Graph Theory, 40(1):35-49, 2020. URL: https://doi.org/10.7151/DMGT.2132.
  20. João P. Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, pages 131-153. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-131.
  21. 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 Verlag, 2020. URL: https://doi.org/10.1007/978-3-030-51372-6_19.
  22. Bernardino Romera-Paredes et al. Mathematical discoveries from program search with large language models. Nature, 625(7995):468-475, 2024. URL: https://doi.org/10.1038/S41586-023-06924-6.
  23. Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476-482, 2024. URL: https://doi.org/10.1038/S41586-023-06747-5.
  24. 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.
  25. Tianwei Zhang and Stefan Szeider. Searching for smallest universal graphs and tournaments with SAT. In Roland H. C. Yap, editor, 29th International Conference on Principles and Practice of Constraint Programming, CP 2023, August 27-31, 2023, Toronto, Canada, volume 280 of LIPIcs, pages 39:1-39:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CP.2023.39.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact