Constructing strong starters of orders \(3p\): triplication with SAT solver

Oleg Ogandzhanyants1, Sergey Sadov2, Margo Kondratieva1
1Dept. of Mathematics and Statistics, Memorial University, St. John’s NL, A1C~5S7, Canada
2Private Math School, Moscow, Russia

Abstract

A novel approach to building strong starters in cyclic groups of orders \(n\) divisible by 3 from starters of smaller orders is presented. A strong starter in \(\mathbb{Z}_n\) (\(n\) odd) is a partition of the set \(\{1,2,\dots,n-1\}\) into pairs \(\{a_i,b_i\}\) such that all pair sums \(a_i+b_i\) are distinct and nonzero modulo \(n\) and all differences \(\pm(a_i-b_i)\) are distinct and nonzero modulo \(n\). A special interest to strong starters of odd orders divisible by 3 is motivated by Horton’s conjecture, which claims that such starters exist (except when \(n=3\) or \(9\)) but remains unproven since 1989. We begin with a starter of order \(p\) coprime with 3 and describe an algorithm to obtain a Sudoku-type problem modulo 3 whose solution, if exists, yields a strong starter of order \(3p\). The process leading from the original to the final starter is called triplication. Besides theoretical aspects of the construction, practicality of this approach is demonstrated. A general-purpose constraint-satisfaction (SAT) solver z3 is used to solve the Sudoku-type problem; various performance statistics are presented.

Keywords: strong starter, SAT solver, triplication