Download PDFOpen PDF in browser

Stedman and Erin Triples encoded as a SAT Problem

EasyChair Preprint no. 673

16 pagesPublished: 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: bobs-only, Boolean satisfiability, Campanology, change ringing, Erin, Erin Triples, Hamiltonian cycle, HCP, LFSR, Linear Feedback Shift Register, SAT, SAT solver, Stedman, Stedman Triples

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 no. 673},

  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser