**2019**

Solving Hamiltonian Cycle problems using Boolean satisfiability
Andrew Johnson
*30th European Conference on Operational Research*, 2019
Abstract
A classic NP-complete problem is finding a cycle visiting all nodes in a graph exactly once. This talk details the techniques used by the author to solve 614 of the 1001 graphs of Flinders Hamiltonian Cycle Problem Challenge Set, varying from 96 to 9528 nodes. One of the powerful techniques given here is the author's very efficient general reduction of the Hamiltonian Cycle Problem (HCP) to Boolean Satisfiability (SAT) converting any Hamiltonian Cycle problem with n vertices and m directed edges to a SAT problem with approximately n.log2(m) variables and 2m.(log2(n)+1) clauses. This reduction is significantly smaller and more efficient than any other published reductions, which are impractical for more than a few hundred nodes. For each graph the SAT problem was submitted to a SAT solver and any solution converted back to the HCP domain. Generating certain additional constraints with additional clauses or variables for the SAT problem actually improved the solve time with existing SAT solvers and so helped to solve more graphs. Graph manipulations allowed still more graphs to be solved. The HCP to SAT reduction may have other uses for scheduling and permutation type problems.

Change ringing and Hamiltonian cycles: The search for Erin and Stedman triples
Michael Haythorpe, and Andrew Johnson and
*Electronic Journal of Graph Theory and Applications* *7*(*1*), 61--75, The Institute for Research and Community Services (LPPM) ITB, 2019
Abstract
A very old problem in campanology is the search for peals. The latter can be thought of as a
heavily constrained sequence of all possible permutations of a given size, where the exact nature
of the constraints depends on which method of ringing is desired. In particular, we consider the
methods of bobs-only Stedman Triples and Erin Triples; the existence of the latter is still an open
problem. We show that this problem can be viewed as a similarly constrained (but not previously
considered) form of the Hamiltonian cycle problem (HCP). Through the use of special subgraphs,
we convert this to a standard instance of HCP. The original problem can be partitioned into smaller
instances, and so we use this technique to produce smaller instances of HCP as well. We note that
the instances known to have solutions provide exceptionally difficult instances of HCP.

**2018**

Stedman and Erin Triples encoded as a SAT Problem
Andrew Johnson
*EasyChair Preprint* *pp. 673*, EasyChair, 2018
Abstract Preprint paper associate with POS 2018 presentation
A very old quest in campanology is the search for peals, which can be considered as constrained searches for Hamiltonian cycles of a Cayley graph. Two particularly hard problems are finding bobs-only peals of Stedman Triples and Erin Triples. We show how to efficiently reduce them to boolean satisfiability and use a SAT solver to help find bobs-only peals of Stedman Triples, and express the unsolved problem of bobs-only Erin Triples as an unsolved SAT problem. This approach is based on the author's very efficient general reduction of the Hamiltonian Cycle Problem (HCP) to Boolean Satisfiability (SAT) converting any Hamiltonian Cycle problem with n vertices and m directed edges to a SAT problem with approximately n.log2(m) variables and 2m.(log2(n)+1) clauses.

Preprint paper associate with POS 2018 presentation

Stedman and Erin Triples encoded as a SAT problem
Andrew Johnson
*Federated Logic Conference 2018: Pragmatics of SAT*
Abstract
A very old quest in campanology is the search for peals, which can be considered as constrained searches for Hamiltonian cycles of a Cayley graph. Two particularly hard problems are finding bobs-only peals of Stedman Triples and Erin Triples. We show how to efficiently reduce them to boolean satisfiability and use a SAT solver to help find bobs-only peals of Stedman Triples, and express the unsolved problem of bobs-only Erin Triples as an unsolved SAT problem. This approach is based on the author's very efficient general reduction of the Hamiltonian Cycle Problem (HCP) to Boolean Satisfiability (SAT) converting any Hamiltonian Cycle problem with n vertices and m directed edges to a SAT problem with approximately n.log2(m) variables and 2m.(log2(n)+1) clauses.

**2017**

Change Ringing and Hamiltonian Cycles: The Search for Erin and Stedman Triples
Haythorpe, Michael and Johnson, Andrew
*arXiv preprint arXiv:1702.02623 [math.co]*, 2017
Abstract
Abstract: A very old problem in campanology is the search for peals. The latter can be thought of as a heavily constrained sequence of all possible permutations of a given size, where the exact nature of the constraints depends on which method of ringing is desired. In particularr, we consider the methods of bobs-only Stedman Triples and Erin Triples; the existence of the latter is still an open problem. We show that this problem can be viewed as a similarly constrained form of the Hamiltonian cycle problem (HCP). Through the use of special subgraphs, we convert this to a standard instance of HCP. The original problem can be partitioned into smaller instances, and so we use this technique to produce smaller instances of HCP as well. We note that the instances known to have solutions provide exceptionally difficult instances of HCP.

**2014**

Quasi-linear reduction of Hamiltonian Cycle Problem (HCP) to Satisfiability Problem (SAT)
Andrew Johnson
*The IP.com Prior Art Database* *pp. IPCOM000237123D*, 16, IP.com, 2014
Abstract
This paper shows a way of converting any Hamiltonian Cycle problem (HCP) with n vertices and m directed edges to a Boolean Satisfiability problem (SAT) problem with approximately n.log2(m) variables and 2m.(log2(n)+1) clauses. It uses vertex numbering using a linear feedback shift register (LFSR) sequence together with variables identifying active edges, and simple algebraic constraints between a vertex number and its successors' vertex number based on active edges. By adding redundant constraints on the edges a SAT solver can now solve HCP problems with 500 to 1000 vertices.