Using Integer Programming to Search for Counterexamples: A Case Study

It is known that there exist 4-regular, 1-tough graphs which are non-hamiltonian. The smallest such graph known has$$n=18$$ nodes and was found by Bauer et al., who conjectured that all 4-regular, 1-tough graphs with$$nle 17$$ are hamiltonian. They in fact proved that this is true for$$nle 15$$, but left open the possibility of non-hamiltonian graphs of 16 or 17 nodes. By using ILP for modeling a counterexample, and then finding out that the model has no solutions, we give an algorithmic proof that their conjecture was indeed correct.