Enumeration of Complex Golay Pairs via Programmatic SAT

TL;DR

This paper completely enumerates complex Golay pairs up to length 25, confirming their non-existence at lengths 23 and 25 and existence at length 24, using a novel SAT+CAS computational approach.

Contribution

It introduces a new enumeration method combining computer algebra systems with SAT solvers to classify complex Golay pairs up to length 25.

Findings

Complex Golay pairs exist at length 24.

No complex Golay pairs exist at lengths 23 and 25.

Verification of a 2002 conjecture about Golay pairs.

Abstract

We provide a complete enumeration of all complex Golay pairs of length up to 25, verifying that complex Golay pairs do not exist in lengths 23 and 25 but do exist in length 24. This independently verifies work done by F. Fiedler in 2013 that confirms the 2002 conjecture of Craigen, Holzmann, and Kharaghani that complex Golay pairs of length 23 don't exist. Our enumeration method relies on the recently proposed SAT+CAS paradigm of combining computer algebra systems with SAT solvers to take advantage of the advances made in the fields of symbolic computation and satisfiability checking. The enumeration proceeds in two stages: First, we use a fine-tuned computer program and functionality from computer algebra systems to construct a list containing all sequences which could appear as the first sequence in a complex Golay pair (up to equivalence). Second, we use a programmatic SAT solver to construct all sequences (if any) that pair off with the sequences constructed in the first stage to form a complex Golay pair.