A SAT Approach for Finding Sup-Transition-Minors

The cycle double cover conjecture is a famous longstanding unsolved conjecture in graph theory. It is related and can be reduced to the compatible circuit decomposition problem. Recently Fleischner et al. (2018) provided a sufficient condition for a compatible circuit decomposition, which is called SUD-\(K_5\)-minor freeness. In a previous work we developed an abstract mathematical model for finding SUD-\(K_5\)-minors and based on the model a mixed integer linear program (MIP). In this work we propose a respective boolean satisfiability (SAT) model and compare it with the MIP model in computational tests. Non-trivial symmetry breaking constraints are proposed, which improve the solving times of both models considerably. Compared to the MIP model the SAT approach performs significantly better. We use the faster algorithm to further test graphs of graph theoretic interest and were able to get new insights. Among other results we found snarks with 30 and 32 vertices that do not contain a perfect pseudo-matching, that is a spanning subgraph consisting of \(K_2\) and \(K_{1,3}\) components, whose contraction leads to a SUD-\(K_5\)-minor free graph.