Using integer programming to search for counterexamples: a case study (Q2663722)

In 1990, among other results, \textit{D. Bauer} et al. [Discrete Appl. Math. 28, No. 3, 191--195 (1990; Zbl 0706.68052)] constructed a 4-regular 1-tough non-Hamiltonian graph of 18 nodes and conjectured that all 4-regular 1-tough graphs with at most \(n \leq 17\) nodes are Hamiltonian. On the other hand, a result of \textit{F. Hilbig} [Kantenstrukturen in nichthamiltonschen Graphen. Berlin: Fachbereich Mathematik der Technischen Universität Berlin (PhD Thesis) (1986; Zbl 0614.05033)] implies that the conjecture is true for \(n \leq 15\). In this paper, ``by using ILP for modeling a counterexample, and then finding out that the model has no solutions'', the authors give an algorithmic proof that each 4-regular 1-tough graph of 16 or 17 nodes is Hamiltonian and therefore prove that the conjecture is indeed true. For the entire collection see [Zbl 1458.90004].