License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.4
URN: urn:nbn:de:0030-drops-166780
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16678/
Go to the corresponding LIPIcs Volume Portal

Kirchweger, Markus ; Scheucher, Manfred ; Szeider, Stefan

A SAT Attack on Rota’s Basis Conjecture

pdf-format:
LIPIcs-SAT-2022-4.pdf (0.8 MB)

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.

BibTeX - Entry

@InProceedings{kirchweger_et_al:LIPIcs.SAT.2022.4,
  author =	{Kirchweger, Markus and Scheucher, Manfred and Szeider, Stefan},
  title =	{{A SAT Attack on Rota’s Basis Conjecture}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{4:1--4:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16678},
  URN =		{urn:nbn:de:0030-drops-166780},
  doi =		{10.4230/LIPIcs.SAT.2022.4},
  annote =	{Keywords: SAT modulo Symmetry (SMS), dynamic symmetry breaking, Rota’s basis conjecture, matroid}
}

Keywords: SAT modulo Symmetry (SMS), dynamic symmetry breaking, Rota’s basis conjecture, matroid
Collection: 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Issue Date: 2022
Date of publication: 28.07.2022
Supplementary Material: Software (Source Code): https://doi.org/10.5281/zenodo.6616343
Dataset (Data for Rank 4): https://doi.org/10.5281/zenodo.6616373

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI