Enumeration of complex Golay pairs via programmatic SAT

DOI10.1145/3208976.3209006MaRDI QIDQ5120185zbMATH OpenOpenAlexWikidataFDO

Authors Curtis Bright, Albert Heinle, Vijay Ganesh, Ilias S. Kotsireas

Publication date 9 September 2020

Published in Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1805.05488

zbMATH Keywords

autocorrelationBoolean satisfiabilitycomplex Golay pairsexhaustive searchSAT solvers

Mathematics Subject Classification ID

Exact enumeration problems, generating functions (05A15) Special sequences and polynomials (11B83) Computational aspects of satisfiability (68R07) Computer assisted proofs of proofs-by-exhaustion type (68V05) Symbolic computation and algebraic computation (68W30) Shift register sequences and sequences over finite alphabets in information and communication theory (94A55)

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.

Recommendations

• Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT
• A complete description of Golay pairs for lengths up to 100
• scientific article; zbMATH DE number 731864
• Small Golay sequences
• The SAT+CAS method for combinatorial search with applications to best matrices

Cited in

(5)

• Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT
• The SAT+CAS method for combinatorial search with applications to best matrices
• Generalizing pairs of complementary sequences and a construction of combinatorial structures
• Applying computer algebra systems with SAT solvers to the Williamson conjecture
• A nonexistence certificate for projective planes of order ten with weight 15 codewords

Describes a project that uses

Uses Software

• Maple
• FFTW
• MathCheck
• nsoks

This page was built for publication: Enumeration of complex Golay pairs via programmatic SAT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5120185)