Stedman and Erin Triples encoded as a SAT Problem

EasyChair Preprint 673

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.

Keyphrases: Boolean satisfiability, Campanology, Erin, Erin Triples, HCP, Hamiltonian cycle, LFSR, Linear Feedback Shift Register, SAT, SAT solver, Stedman, Stedman Triples, bobs-only, change ringing

@booklet{EasyChair:673,
  author    = {Andrew Johnson},
  title     = {Stedman and Erin Triples encoded as a SAT Problem},
  howpublished = {EasyChair Preprint 673},
  year      = {EasyChair, 2018}}