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

TL;DR

This paper introduces a novel triplication method using SAT solvers to construct strong starters of order 3p from smaller ones, addressing a longstanding conjecture in combinatorial design theory.

Contribution

It presents a new triplication algorithm for strong starters of order 3p, combining theoretical construction with practical SAT solver implementation.

Findings

Successfully constructed strong starters for new orders using SAT-based triplication.

Demonstrated the effectiveness of SAT solvers in solving Sudoku-type problems related to combinatorial designs.

Provided performance data on the proposed method's efficiency and practicality.

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 $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.