So my first international trip since Covid happened has been to a CS/Maths Research Centre “Schloss Dagstuhl” located in a fairly rural area in Germany.

Similar to various other research centres around the world, the idea is to gather together a bunch of academics for a week in a location with few external distractions, have a few talks and tutorials, and plenty of time for working groups. The Australian version of this model is the MATRIX Research Institute in Creswick, Victoria, though as this uses former student accommodation blocks, it is not quite as comfortable.
The topic of this seminar was “Pushing the Limits on Computational Combinatorial Constructions” which gathered together a group of people working on combinatorial computing, in particular combinatorial search, generation of combinatorial catalogues and the existing, new and improved tools needed for these talks. So I felt that I really had to go, even though my body is telling me that I can no longer travel long distances for short times.
Despite the jet-lag it was great to catch up with old friends and to meet some of the younger people doing very interesting work. One of the more prominent themes that emerged during the workshop was the use of SAT solvers to solve combinatorial problems. Many combinatorial questions about the existence of combinatorial structures or substructures be modelled as a SAT instance. Often the number of clauses blows out because things such as calculating intersection sizes or testing connectivity often requires a seemingly enormous number of auxiliary variables. However SAT is very heavily studied and modern SAT solvers can cope with very large instances (at least, often enough to make it worthwhile trying). We heard about SAT being used to improve bounds on the smallest known Kochen-Specker graphs, about SAT being used (in vain) to find counterexamples to Rota’s Basis Conjecture at rank 4, and about SAT being used to verify (significant parts of) the proof of the non-existence of the projective plane of order 10.
I talked a bit about the nature of computational results, talking about the computer proof of the 4-Colour Theorem, the computer proof of the non-existence of the projective plane of order 10 and why these were (and in some circles still are) viewed with suspicion. I also described Blackburn, Crapo and Higgs construction of the catalogue of matroids on up to 8 elements in 1969. For many years, the list of “known excluded minors” for quaternary matroids omitted one matroid that was just sitting in the catalogue, and perhaps knowing this would have helped resolve the question sooner. I assume that before computers were commonplace, it was simply too hard to access the catalogue.
We had a nice excursion to a local beauty spot where the Saar River does a tight loop in steep forested terrain, with various hiking trails. Ian Wanless and I ended up doing a steep hike together with some fairly gruelling uphill stages (at least for me). David Pike saw us setting off and got a nice photo of us.

Our last couple of days were enlivened by the planned train strike on Friday disrupting everyone’s travel plans. After wasting a lot of time trying to find alternatives, I was rescued by Adolfo “Traces” Piperno, who was driving to Frankfurt Airport and took me and one other to catch our early evening flights, despite his own flight being several hours later. The trip was mostly smooth, although as we got very close to the airport, the GPS in our phones seemed to get confused by the sheer number of roads and lanes all converging and crossing over and under each other, so at various stages my GPS was instructing us to “Turn right now” at exactly the same time as Adolfo’s was saying “Gira a sinistra”.
But since this was the culmination of a week of computational combinatorics, a little back-tracking seemed entirely appropriate and we eventually found our way.