Document Open Access Logo

A SAT Attack on Rota’s Basis Conjecture

Authors Markus Kirchweger , Manfred Scheucher , Stefan Szeider

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.4.pdf
  • Filesize: 0.82 MB
  • 18 pages

Document Identifiers

Author Details

Markus Kirchweger
  • Algorithms and Complexity Group, TU Wien, Autria
Manfred Scheucher
  • Institut für Mathematik, Technische Universität Berlin, Germany
Stefan Szeider
  • Algorithms and Complexity Group, TU Wien, Autria

Funding

M.K. and S.S. were supported by the Austrian Science Fund (FWF), project P32441, and from the Vienna Science and Technology Fund (WWTF), project ICT19-065. M.S. was supported by the DFG Grant SCHE 2214/1-1.

Cite AsGet BibTex

Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. A SAT Attack on Rota’s Basis Conjecture. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.4

Abstract

The SAT modulo Symmetries (SMS) is a recently introduced framework for dynamic symmetry breaking in SAT instances. It combines a CDCL SAT solver with an external lexicographic minimality checking algorithm. We extend SMS from graphs to matroids and use it to progress on Rota’s Basis Conjecture (1989), which states that one can always decompose a collection of r disjoint bases of a rank r matroid into r disjoint rainbow bases. Through SMS, we establish that the conjecture holds for all matroids of rank 4 and certain special cases of matroids of rank 5. Furthermore, we extend SMS with the facility to produce DRAT proofs. External tools can then be used to verify the validity of additional axioms produced by the lexicographic minimality check. As a byproduct, we have utilized our framework to enumerate matroids modulo isomorphism and to support the investigation of various other problems on matroids.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Matroids and greedoids
  • Mathematics of computing → Solvers
  • Hardware → Theorem proving and SAT solving
Keywords
  • SAT modulo Symmetry (SMS)
  • dynamic symmetry breaking
  • Rota’s basis conjecture
  • matroid

Metrics

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

Supplementary Materials

References

  1. Dragan Acketa. The catalogue of all nonisomorphic matroids on at most 8 elements. Special Issue, University of Novi Sad Institute of Mathematics Faculty of Science, 1, 1983. Google Scholar
  2. Noga Alon and Michael Tarsi. Colorings and orientations of graphs. Combinatorica, 12(2):125-134, 1992. URL: https://doi.org/10.1007/BF01204715.
  3. Martin Balko and Pavel Valtr. A SAT attack on the Erdős-Szekeres conjecture. European Journal of Combinatorics, 66:13-23, 2017. URL: https://doi.org/10.1016/j.ejc.2017.06.010.
  4. Armin Biere. CaDiCaL at the SAT Race 2019. In Proc. of SAT Race 2019 - Solver and Benchmark Descriptions, volume B-2019-1 of Department of Computer Science Series, pages 8-9. University of Helsinki, 2019. URL: http://researchportal.helsinki.fi/en/publications/proceedings-of-sat-race-2019-solver-and-benchmark-descriptions.
  5. Matija Bucić, Matthew Kwan, Alexey Pokrovskiy, and Benny Sudakov. Halfway to Rota’s basis conjecture. Int. Math. Res. Not., 2020. URL: https://doi.org/10.1093/imrn/rnaa004.
  6. Wendy Chan. An exchange property of matroid. Discrete Math., 146(1):299-302, 1995. URL: https://doi.org/10.1016/0012-365X(94)00071-3.
  7. Micheal S. Cheung. Computational proof of Rota’s basis conjecture for matroids of rank 4. Unpublished manuscript, available at Joshua E. Ducey’s website http://educ.jmu.edu/~duceyje/undergrad/2012/mike.pdf, 2012.
  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. Karl Däubel, Sven Jäger, Torsten Mütze, and Manfred Scheucher. On orthogonal symmetric chain decompositions. Electron. J. Combin., 26(3):Article Number P3.64, 32, 2019. URL: https://doi.org/10.37236/8531.
  10. Jo Devriendt, Bart Bogaerts, and Maurice Bruynooghe. Symmetric explanation learning: Effective dynamic symmetry handling for SAT. In Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, volume 10491 of Lecture Notes in Computer Science, pages 83-100. Springer Verlag, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_6.
  11. Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe, and Marc Denecker. Improved static symmetry breaking for SAT. In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, volume 9710 of Lecture Notes in Computer Science, pages 104-122. Springer Verlag, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_8.
  12. Michael R. Dransfield, Lengning Liu, Victor W. Marek, and Miroslaw Truszczyński. Satisfiability and computing van der Waerden numbers. Electron. J. Combin., 11(1):Article Number R41, 15, 2004. URL: https://doi.org/10.37236/1794.
  13. Arthur A. Drisko. On the number of even and odd Latin squares of order p+1. Adv. Math., 128(1):20-35, 1997. URL: https://doi.org/10.1006/aima.1997.1623.
  14. Mark Dukes. On the number of matroids on a finite set. Séminaire Lotharingien de Combinatoire, 51:Article B51g, 12, 2004. URL: https://www.mat.univie.ac.at/~slc/wpapers/s51dukes.html.
  15. Benjamin Friedman and Sean McGuinness. Girth conditions and Rota’s basis conjecture, 2020. URL: http://arxiv.org/abs/1908.01216.
  16. Hiroshi Fujita. A new lower bound for the Ramsey number R(4,8). http://arXiv.org/abs/1212.1328, 2012.
  17. Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub, and Philipp Wanko. Theory solving made easy with Clingo 5. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016), volume 52 of OASICS, pages 2:1-2:15. Dagstuhl, 2016. URL: https://doi.org/10.4230/OASIcs.ICLP.2016.2.
  18. Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. Clingo = ASP + control: Preliminary report, 2014. URL: http://arxiv.org/abs/1405.3694.
  19. Jim Geelen and Peter J. Humphries. Rota’s basis conjecture for paving matroids. SIAM J. Discrete Math., 20(4):1042-1045, 2006. URL: https://doi.org/10.1137/060655596.
  20. Jim Geelen and Kerri Webb. On Rota’s basis conjecture. SIAM J. Discrete Math., 21(3):802-804, 2007. URL: https://doi.org/10.1137/060666494.
  21. P. R. Herwig, Marijn J. H. Heule, P. M. van Lambalgen, and H. van Maaren. A new method to construct lower bounds for van der Waerden numbers. Electron. J. Combin., 14(1):Article Number R6, 18, 2007. URL: https://doi.org/10.37236/925.
  22. Marijn J. H. Heule. The DRAT format and DRAT-trim checker, 2016. URL: http://arxiv.org/abs/1610.06229.
  23. Rosa Huang and Gian-Carlo Rota. On the relations of various conjectures on Latin squares and straightening coefficients. Discrete Math., 128(1-3):225-236, 1994. URL: https://doi.org/10.1016/0012-365X(94)90114-7.
  24. Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. A SAT Attack on Rota’s Basis Conjecture: Supplemental data for rank 4. URL: https://doi.org/10.5281/zenodo.6616373.
  25. Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. A SAT Attack on Rota’s Basis Conjecture: Supplemental source code. URL: https://doi.org/10.5281/zenodo.6616343.
  26. 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.
  27. Boris Konev and Alexei Lisitsa. A SAT attack on the Erdős discrepancy conjecture. In Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, volume 8561 of Lecture Notes in Computer Science, pages 219-226. Springer Verlag, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_17.
  28. Michal Kouril and Jerome L. Paul. The van der Waerden number W(2,6) is 1132. Experiment. Math., 17(1):53-61, 2008. URL: http://projecteuclid.org/euclid.em/1227031896.
  29. Filip Marić. Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points. Journal of Automated Reasoning, 62:301-329, 2019. URL: https://doi.org/10.1007/s10817-017-9423-7.
  30. Dillon Mayhew and Gordon F. Royle. Matroids with nine elements. J. Combin. Theory Ser. B, 98(2):415-431, 2008. URL: https://doi.org/10.1016/j.jctb.2007.07.005.
  31. Hakan Metin, Souheib Baarir, Maximilien Colange, and Fabrice Kordon. CDCLSym: Introducing effective symmetry breaking in SAT solving. In Tools and Algorithms for the Construction and Analysis of Systems, pages 99-114. Springer Verlag, 2018. URL: https://doi.org/10.1007/978-3-319-89960-2_6.
  32. Torsten Mütze and Manfred Scheucher. On L-shaped point set embeddings of trees: first non-embeddable examples. J. Graph Algorithms Appl., 24(3):343-369, 2020. URL: https://doi.org/10.7155/jgaa.00537.
  33. OEIS Foundation Inc. The On-Line Encyclopedia of Integer Sequences. Published electronically at URL: http://oeis.org.
  34. Shmuel Onn. A colorful determinantal identity, a conjecture of Rota, and Latin squares. Amer. Math. Monthly, 104(2):156-159, 1997. URL: https://doi.org/10.2307/2974985.
  35. Open Problem Garden. Rota’s basis conjecture, 2009. URL: http://www.openproblemgarden.org/op/rotas_basis_conjecture.
  36. James Oxley. Matroid theory, volume 21 of Oxford Graduate Texts in Mathematics. Oxford University Press, second edition, 2011. URL: https://doi.org/10.1093/acprof:oso/9780198566946.001.0001.
  37. Alexey Pokrovskiy. Rota’s basis conjecture holds asymptotically, 2020. URL: http://arxiv.org/abs/2008.06045.
  38. Bas Schaafsma, Marijn Heule, and Hans van Maaren. Dynamic symmetry breaking by simulating Zykov contraction. In Theory and Applications of Satisfiability Testing - SAT 2009, volume 5584 of Lecture Notes in Computer Science, pages 223-236. Springer Verlag, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_22.
  39. Manfred Scheucher. Two disjoint 5-holes in point sets. Comput. Geom., 91:101670, 2020. URL: https://doi.org/10.1016/j.comgeo.2020.101670.
  40. Manfred Scheucher, Hendrik Schrezenmaier, and Raphael Steiner. A note on universal point sets for planar graphs. J. Graph Algorithms Appl., 24(3):247-267, 2020. URL: https://doi.org/10.7155/jgaa.00529.
  41. Toby Walsh. General symmetry breaking constraints. In Principles and Practice of Constraint Programming - CP 2006, 12th International Conference, CP 2006, volume 4204 of Lecture Notes in Computer Science, pages 650-664. Springer Verlag, 2006. URL: https://doi.org/10.1007/11889205_46.
  42. 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.
  43. O. Zaikin, S. Kochemazov, and A. A. Semenov. SAT-based search for systems of diagonal Latin squares in volunteer computing project SAT@home. In 39th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO 2016), pages 277-281, 2016. URL: https://doi.org/10.1109/MIPRO.2016.7522152.
  44. I. Zinovik, D. Kroening, and Y. Chebiryak. Computing binary combinatorial Gray codes via exhaustive search with SAT solvers. Institute of Electrical and Electronics Engineers. Transactions on Information Theory, 54(4):1819-1823, 2008. URL: https://doi.org/10.1109/TIT.2008.917695.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact