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

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