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

*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”.*

**any**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

**, and so on. This is called**

*IN**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!

Any specific reason you’re using Minion and its weird matrix-based language over some more common CSP solvers (see http://www.minizinc.org/challenge2015/results2015.html for a list of those participating in the yearly contest)?

Good question… I think just because I saw a talk about enumerating loops (a kind of mathematical structure) where the speaker had used Mimion, and so I decided to try it. Not knowing other CSP solvers, I had no way to judge the weirdness or otherwise of the language.

But I should probably investigate others just to have a wider range of options.

Sorry to reply to an old post, but I am quite curious who was using Minion to enumerate loops. Do you happen to remember?

My first thought is Petr Vojtechovsky, but presumably you would already know if it were him. I will try to triangulate where I was when I saw the relevant talk by conferring with colleagues.

Right, it wasn’t Petr. I don’t think he’s ever heard of Minion. I only know of it from conversations with Andreas Distler when we were sharing an office in Lisbon.

Brendan McKay has done the detective work – we were together in a seminar when we learned about MINION. Our email (between Brendan and I) first featured MINION in 2009 so the conference was before then. It wasn’t the ACCMCC conference because it had not been held at UWA for many years before then. So it was Cheryl Praeger’s 60th birthday conference, and as the program is still online (http://sponsored.uwa.edu.au/gcc09/timetable?f=24709) we discovered that the talk was given by …. drum roll … Andreas Distler!

Hahaha! Thank you, Gordon (and Brendan), that’s wonderful. Looking at Andreas’ abstract, I see that this was back when he was enumerating semigroups of order 9. Maybe he mentioned loops or quasigroups in passing, because I don’t see anything in his publications that suggests he worked on them in earnest. I should probably ask him; I haven’t heard from him in a few years.

I am interested in Minion because I would like to use it (or something similar) to hunt for large counterexamples in loop theory because it is claimed that such tools scale well. The model builder I currently use, Mace4, is only practical for small loops. The steepness of the Minion learning curve is proportional to how easy it is to encode universally quantified identities, but I haven’t looked in enough detail to figure this out.

Minion’s language is indeed a bit weird (although it does pre-date Minizinc by several years!) Unfortunately the Minizinc translator is very bad at making use of many of Minion’s features, so adding support doesn’t seem useful.

A better way to get a nicer input to Minion is to use SavileRow ( http://savilerow.cs.st-andrews.ac.uk/ ) , which is similar to MiniZinc, although it only outputs Minion, Gecode and SAT output (the quality for these solvers is usually much better than MiniZinc’s however).

IMHO a linear programming certificate would be more convincing; you start off by writing the usual LP relaxation for a TSP on this graph, and add inequalities that kill off 2-factors which are not cycles, until you end up with an empty set of solutions (cf. e.g. http://www.math.uwaterloo.ca/tsp/methods/dfj/). Then you can produce Farkas certificate of infeasibility for the system of inequalities at hand…