Constructing strong starters of orders $3p$: triplication with SAT solver

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 $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 strong 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 {\em 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.