Minion and hamiltonicity

Over the last few years, Minion (I’m giving the link because if you try to search for it, you’ll be swamped by Despicable Me merchandise) has become one of my “go-to” tools, mostly because for certain specific types of searches it seems to perform just as well as, or even better than, a bespoke program. And of course, writing, debugging and optimising a bespoke program is enormously time-consuming, while writing a Minion model is usually very quick.

Most recently, I had an email from Brendan (McKay), who has found three planar cubic graphs of girth 5 that are hypohamiltonian – a graph is hypohamiltonian if it is not hamiltonian, but for every vertex , the graph is hamiltonian. Brendan’s graphs had 76 vertices, so not huge, but big enough.

How do you convince someone, say a referee, that a particular 76-vertex graph is hypohamiltonian? Well it is easy to convince them that all the vertex-deleted subgraphs are hamiltonian, because you can show them 76 cycles, each of length 75, and each missing a different vertex of , and because the graph is planar it is easy enough to see that they are correct from a picture.

But how can you convince them that the original graph is not hamiltonian?  As hamiltonicity is (almost certainly) not in co-NP, there is no reason to suppose that there is any short certificate demonstrating that a graph is not hamiltonian. So of course, we have to resort to the computer to tell us that a particular graph is not hamiltonian, essentially by looking for a hamilton cycle and failing to find one. But there is something unsatisfactory about a paper where everything relies on a single program written by the author of the paper, especially when the program runs for a while, and then says “No”.

So Brendan sent me three graphs, each on 76 vertices, and asked whether I could show that they are not hamiltonian using my own programs. Of course I’d like to help, but mostly when I want to check a cubic graph for hamiltonicity, I use one of Brendan’s programs!

But in a spare few minutes, I decided to just explore the idea of writing a Minion model that would find spanning 2-regular subgraphs (that is, 2-factors) of the graph. If the graph is hamiltonian then one of the 2-factors subgraphs will be a 76-cycle and otherwise all the 2-factors will have multiple cycles. I didn’t really expect this to work immediately as I anticipated a vast number of 2-factors with multiple short cycles to dominate the output.

So here’s the Minion model for the first graph

MINION 3
**VARIABLES**
BOOL e[114]

This declares a boolean array with 114 variables, one for each edge of the graph. The value e[i] will be 1 if the i’th edge is in the 2-factor and 0 otherwise.

**CONSTRAINTS**
sumgeq([e[0],e[1],e[2]],2)
sumleq([e[0],e[1],e[2]],2)
sumgeq([e[0],e[3],e[4]],2)
sumleq([e[0],e[3],e[4]],2)
...
...
sumgeq([e[110],e[112],e[113]],2)
sumleq([e[110],e[112],e[113]],2)
**EOF**

The constraints are simplicity itself – for each vertex, exactly two of the three edges incident with it will be in the 2-factor, and so the sum of the three variables must be greater-than-or-equal-to 2 and less-than-or-equal-to 2 (no, Minion doesn’t allow this to be done with a single equality check).

So the Minion program will read this model and then try to assign values to the variables in order to satisfy all the constraints, branching where necessary, and following every branch to its conclusion if desired (finding all solutions versus finding a single solution). Every decision made to satisfy one of the constraints has consequences for all the other constraints – at its simplest, assigning one edge to be OUT of the 2-factor forces the other two edges at that vertex to be IN, and so on. This is called constraint propagation, and is exactly the kind of thing you don’t want to program separately for each application.

So without any great expectations, I set it running with:

$ minion -findallsols -noprintsols x1.min

and it returned

Total System Time: 0.001235
Total Wall Time: 0.204282
Maximum RSS (kB): 4044
Total Nodes: 184098
Problem solvable?: yes
Solutions Found: 77161

Yes – in 0.2s it had found all 2-factors and there were only 77161 of them, which is several orders of magnitude less than either Brendan or I expected. In fact, we’d never bothered to do this exactly because our instincts told us that it couldn’t possibly work.

Now counting the number of connected components in each of 77161 2-factors is a trivial task, and unsurprisingly, none of the 2-factors was a hamiltonian cycle. The other two graphs were similarly easy.

This is also something that anyone can easily replicate, and given that Minion is a general purpose CSP solver, it is unlikely that any bugs in it would crop up in exactly this application and this application alone. In addition, the fact that the output is a large list of 2-factors, none of which are hamilton cycles, is much more reassuring than a program that simply produces no output at all.

So even if I had not been convinced before, I am certainly convinced now that Brendan’s 76-vertex cubic planar graphs of girth 5 are hypohamiltonian.

I’m currently at the 39ACCMCC and Brendan spoke today, and we learned that he found these graphs using an exhaustive search of planar cubic girth 5 graphs on 76 vertices. Of the 5,925,181,102,878 such graphs, only 151,274 are not hamiltonian and only 3 are hypohamiltonian.

I’m just glad that this computation is not the one he wanted me to verify!