Download PDFOpen PDF in browser

Stedman and Erin Triples encoded as a SAT Problem

EasyChair Preprint 673

16 pagesDate: December 9, 2018

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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:673,
  author    = {Andrew Johnson},
  title     = {Stedman and Erin Triples encoded as a SAT Problem},
  howpublished = {EasyChair Preprint 673},
  year      = {EasyChair, 2018}}
Download PDFOpen PDF in browser