Document Open Access Logo

Smart Cubing for Graph Search: A Comparative Study

Authors Markus Kirchweger , Tomáš Peitl , Stefan Szeider , Hai Xia

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.33.pdf
  • Filesize: 1.06 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Mathematics of computing → Graph enumeration
  • Mathematics of computing → Extremal graph theory
Keywords
  • cube and conquer
  • graph search
  • algorithm configuration
  • SAT solving

Metrics

Abstract

Parallel solving via cube-and-conquer is a key method for solving hard instances with SAT. While cube-and-conquer has proven successful for pure SAT problems, notably the Pythagorean triples conjecture, its application to SAT solvers augmented with propagators presents unique challenges as propagators learn constraints dynamically during the search.
We study this problem using SAT Modulo Symmetries (SMS) as our primary test case. In our setting, the SMS symmetry-breaking propagator is an ordinary IPASIR-UP propagator; the techniques below do not rely on properties specific to symmetry breaking, except in the benchmark instantiations. Through extensive experimentation comprising over 20,000 CPU hours, we systematically evaluate different cube-and-conquer variants on three well-studied combinatorial problems. Our methodology combines prerun phases to collect learned constraints, various cubing strategies, and parameter tuning via algorithm configuration.
The comprehensive empirical evaluation provides new insights into effective cubing strategies for propagator-based SAT solving. Our best method reduces total solving time by factors of 2-10x from improved cubing, and reduces the time for the hardest cubes by factors of 2-50x.

Cite As Get BibTex

Markus Kirchweger, Tomáš Peitl, Stefan Szeider, and Hai Xia. Smart Cubing for Graph Search: A Comparative Study. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.33

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
Hai Xia
  • Algorithms and Complexity Group, TU Wien, Austria

Funding

The authors acknowledge the support by the European Union’s Horizon 2020 research and innovation programme under the Maria Skłodowska-Curie grant agreement No. 101034440, and the support from the Austrian Science Fund (FWF), project 10.55776/P36688, 10.55776/P36420 and 10.55776/COE12.

Supplementary Materials

References

  1. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  2. Costantino Budroni, Adán Cabello, Otfried Gühne, Matthias Kleinmann, and Jan-Åke Larsson. Kochen-Specker contextuality. Rev. Mod. Phys., 94:045007, 2022. URL: https://doi.org/10.1103/RevModPhys.94.045007.
  3. Louis Caccetta and Roland Häggkvist. On diameter critical graphs. Discrete Math., 28(3):223-229, 1979. URL: https://doi.org/10.1016/0012-365X(79)90129-8.
  4. Ya-Chen Chen and Zoltán Füredi. Minimum vertex-diameter-2-critical graphs. J. Graph Theory, 50(4):293-315, 2005. URL: https://doi.org/10.1002/jgt.20111.
  5. 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.
  6. 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
  7. Antoine Dailly, Florent Foucaud, and Adriana Hansberg. Strengthening the Murty-Simon conjecture on diameter 2 critical graphs. Discrete Math., 342(11):3142-3159, 2019. URL: https://doi.org/10.1016/j.disc.2019.06.023.
  8. P. Erdős. Some remarks on chromatic graphs. Colloq. Math., 16:253-256, 1967. URL: https://doi.org/10.4064/cm-16-1-253-256.
  9. P. Erdős and A. Rényi. On a problem in the theory of graphs. A Magyar Tudományos Akadémia Matematikai Kutató Intézetének Közleményei, 7(4):623-641 (1963), 1962. Google Scholar
  10. Genghua Fan. On diameter 2-critical graphs. Discret. Math., 67(3):235-240, 1987. URL: https://doi.org/10.1016/0012-365X(87)90174-9.
  11. 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. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.8.
  12. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. Satisfiability modulo user propagators. J. Artif. Intell. Res., 81:989-1017, 2024. URL: https://doi.org/10.1613/JAIR.1.16163.
  13. 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.
  14. Ian P. Gent, Karen E. Petrie, and Jean-François Puget. Symmetry in constraint programming. In Francesca Rossi, Peter van Beek, and Toby Walsh, editors, Handbook of Constraint Programming, volume 2 of Foundations of Artificial Intelligence, pages 329-376. Elsevier, 2006. URL: https://doi.org/10.1016/S1574-6526(06)80014-3.
  15. Jan Goedgebeur. On minimal triangle-free 6-chromatic graphs. J. Graph Theory, 93(1):34-48, 2020. URL: https://doi.org/10.1002/jgt.22467.
  16. Teresa W. Haynes, Michael A. Henning, Lucas C. van der Merwe, and Anders Yeo. Progress on the Murty-Simon Conjecture on diameter-2 critical graphs: a survey. J. Comb. Optim., 30(3):579-595, 2015. URL: https://doi.org/10.1007/s10878-013-9651-7.
  17. Marijn Heule, Mark Dufour, Joris E. van Zwieten, and Hans van Maaren. March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver. In Holger H. Hoos and David G. Mitchell, editors, Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers, volume 3542 of Lecture Notes in Computer Science, pages 345-359. Springer, 2004. URL: https://doi.org/10.1007/11527695_26.
  18. Marijn Heule and Hans van Maaren. March_dl: Adding adaptive heuristics and a new branching strategy. J. Satisf. Boolean Model. Comput., 2(1-4):47-59, 2006. URL: https://doi.org/10.3233/SAT190016.
  19. Marijn Heule and Hans van Maaren. Look-ahead based SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 155-184. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-155.
  20. 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.
  21. 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 Verlag, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  22. Mikoláš Janota, Markus Kirchweger, Tomáš Peitl, and Stefan Szeider. Breaking symmetries in quantified graph search: A comparative study. In AAAI 2025: The 39th Annual AAAI Conference on Artificial Intelligence, 2025. Google Scholar
  23. Matti Järvisalo, Armin Biere, and Marijn Heule. Blocked clause elimination. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 129-144. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_10.
  24. Markus Kirchweger, Tomás 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. URL: https://doi.org/10.24963/IJCAI.2023/216.
  25. Markus Kirchweger, Tomás 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, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 13:1-13:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.13.
  26. 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.
  27. 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. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.14.
  28. 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.
  29. 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.
  30. Simon Kochen and Ernst Specker. The problem of hidden variables in quantum mechanics. J. Math. Mech., 17(1):59-87, 1967. Google Scholar
  31. Zhengyu Li, Curtis Bright, and Vijay Ganesh. A SAT solver + computer algebra attack on the minimum Kochen–Specker problem. In Kate Larson, editor, Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24, pages 1898-1906. International Joint Conferences on Artificial Intelligence Organization, August 2024. Main Track. URL: https://doi.org/10.24963/ijcai.2024/210.
  32. Marius Lindauer, Katharina Eggensperger, Matthias Feurer, André Biedenkapp, Difan Deng, Carolin Benjamins, Tim Ruhkopf, René Sass, and Frank Hutter. Smac3: A versatile bayesian optimization package for hyperparameter optimization. Journal of Machine Learning Research, 23(54):1-9, 2022. URL: http://jmlr.org/papers/v23/21-0888.html.
  33. Po-Shen Loh and Jie Ma. Diameter critical graphs. J. Combin. Theory Ser. B, 117:34-58, 2016. URL: https://doi.org/10.1016/j.jctb.2015.11.004.
  34. W. Mantel. Problem 28. Wiskundige Opgaven, 10:60-61, 1907. Google Scholar
  35. João 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 - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 133-182. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200987.
  36. 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.
  37. Jan Mycielski. Sur le coloriage des graphs. Colloquium Mathematicae, 3(2):161-162, 1955. Google Scholar
  38. A Peres. Two simple proofs of the Kochen-Specker theorem. J. Phys. A Math. Theor., 24(4):L175, February 1991. URL: https://doi.org/10.1088/0305-4470/24/4/003.
  39. Jovan Radosavljević and Miodrag Živković. The list of diameter-2-critical graphs with at most 10 nodes. IPSI Transactions on Advanced Research, 16(1):1-5, January 2020. URL: http://ipsitransactions.org/journals/papers/tar/2020jan/p9.pdf.
  40. Vaidyanathan Peruvemba Ramaswamy, Stefan Szeider, and Hai Xia. The power of collaboration: Learning large bayesian networks at scale. In 2024 IEEE 36th International Conference on Tools with Artificial Intelligence (ICTAI), pages 371-378, 2024. URL: https://doi.org/10.1109/ICTAI62512.2024.00061.
  41. Amalee Wilson, Andres Noetzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, and Clark Barrett. Partitioning strategies for distributed SMT solving. In 2023 Formal Methods in Computer-Aided Design (FMCAD), pages 199-208. IEEE, 2023. Google Scholar
  42. Haoze Wu, Clark Barrett, and Nina Narodytska. Cubing for tuning. arXiv preprint arXiv:2504.19039, 2025. URL: https://doi.org/10.48550/arXiv.2504.19039.
  43. Hai Xia and Stefan Szeider. SAT-Based tree decomposition with iterative cascading policy selection. Proceedings of the AAAI Conference on Artificial Intelligence, 38(8):8191-8199, March 2024. URL: https://doi.org/10.1609/aaai.v38i8.28659.
  44. Tianwei Zhang, Tomás Peitl, and Stefan Szeider. Small unsatisfiable k-cnfs with bounded literal occurrence. In Supratik Chakraborty and Jie-Hong Roland Jiang, editors, 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, 2024, Pune, India, volume 305 of LIPIcs, pages 31:1-31:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.31.
  45. 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, 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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact