More Web Proxy on the site http://driver.im/

research-article

Enumeration of Complex Golay Pairs via Programmatic SAT

Authors:

Ilias Kotsireas,

Vijay GaneshAuthors Info & Claims

ISSAC '18: Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation

Pages 111 - 118

https://doi.org/10.1145/3208976.3209006

Published: 11 July 2018 Publication History

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.

References

[1]

Erika Ábrahám. 2015. Building bridges between symbolic computation and satisfiability checking Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation. ACM, New York, 1--6.

Digital Library

[2]

Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, and Thomas Sturm. 2016. SC2: Satisfiability Checking meets Symbolic Computation (Project Paper). In Intelligent Computer Mathematics: 9th International Conference, CICM 2016, Bialystok, Poland, July 25--29, 2016, Proceedings. Springer International Publishing, Cham, 28--43. http://www.sc-square.org/

[3]

Curtis Bright. 2017. Computational Methods for Combinatorial and Number Theoretic Problems. Ph.D. Dissertation. University of Waterloo.

[4]

Curtis Bright, Vijay Ganesh, Albert Heinle, Ilias S. Kotsireas, Saeed Nejati, and Krzysztof Czarnecki. 2016. textscMathCheck2: A SAT

[5]

CAS Verifier for Combinatorial Conjectures Computer Algebra in Scientific Computing - 18th International Workshop, CASC 2016, Bucharest, Romania, September 19--23, 2016, Proceedings. 117--133.

[6]

Curtis Bright, Ilias Kotsireas, and Vijay Ganesh. 2018. A SAT+CAS Method for Enumerating Williamson Matrices of Even Order Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence.

[7]

Curtis Bright, Ilias Kotsireas, Albert Heinle, and Vijay Ganesh. 2018. Complex Golay Pairs via SAT. https://cs.uwaterloo.ca/ cbright/cgpsat/. Complex Golay pairs archived at https://zenodo.org/record/1246337, code available at https://bitbucket.org/cbright/mathcheck2

[8]

R. Craigen. 1994. Complex Golay sequences. J. Combin. Math. Combin. Comput. Vol. 15 (1994), 161--169.

[9]

R. Craigen, W. Holzmann, and H. Kharaghani. 2002. Complex Golay sequences: structure and applications. Discrete Math. Vol. 252, 1--3 (2002), 73--89. showCODENDSMHA4

[10]

James A Davis and Jonathan Jedwab. 1999. Peak-to-mean power control in OFDM, Golay complementary sequences, and Reed-Muller codes. IEEE Transactions on Information Theory Vol. 45, 7 (1999), 2397--2417.

Digital Library

[11]

P. G. Donato, J. Urena, M. Mazo, and F. Alvarez. 2004. Train wheel detection without electronic equipment near the rail line IEEE Intelligent Vehicles Symposium, 2004. 876--880.

[12]

Frank Fiedler. 2013. Small Golay sequences. Advances in Mathematics of Communications Vol. 7, 4 (2013).

[13]

Frank Fiedler, Jonathan Jedwab, and Matthew G Parker. 2008. A Framework for the Construction of Golay Sequences. IEEE Transactions on Information Theory Vol. 54, 7 (2008), 3114--3129.

Digital Library

[14]

Frank Fiedler, Jonathan Jedwab, and Matthew G Parker. 2008. A multi-dimensional approach to the construction and enumeration of Golay complementary sequences. Journal of Combinatorial Theory, Series A Vol. 115, 5 (2008), 753--776.

Digital Library

[15]

Matteo Frigo and Steven G Johnson. 2005. The design and implementation of FFTW3. Proc. IEEE Vol. 93, 2 (2005), 216--231.

[16]

Vijay Ganesh, Charles W O'Donnell, Mate Soos, Srinivas Devadas, Martin C Rinard, and Armando Solar-Lezama. 2012. Lynx: A programmatic SAT solver for the RNA-folding problem International Conference on Theory and Applications of Satisfiability Testing. Springer, 143--156.

Digital Library

[17]

Richard G Gibson and Jonathan Jedwab. 2011. Quaternary Golay sequence pairs I: Even length. Designs, Codes and Cryptography Vol. 59, 1--3 (2011), 131--146.

Digital Library

[18]

Marcel Golay. 1961. Complementary series. IRE Transactions on Information Theory Vol. 7, 2 (1961), 82--87.

[19]

Marcel J.E. Golay. 1949. Multi-slit spectrometry. JOSA Vol. 39, 6 (1949), 437--444.

[20]

W. H. Holzmann and H. Kharaghani. 1994. A computer search for complex Golay sequences. Australas. J. Combin. Vol. 10 (1994), 251--258.

[21]

Aamir Hussain, Zeashan H. Khan, Azfar Khalid, and Muhammad Iqbal. 2014. A Comparison of Pulse Compression Techniques for Ranging Applications. Springer Singapore, Singapore, 169--191.

[22]

Hadi Kharaghani and Behruz Tayfeh-Rezaie. 2005. A Hadamard matrix of order 428. Journal of Combinatorial Designs Vol. 13, 6 (2005), 435--440.

[23]

Ilias S Kotsireas. 2013. Algorithms and metaheuristics for combinatorial matrices. In Handbook of Combinatorial Optimization. Springer, 283--309.

[24]

Ying Li and Wen Bin Chu. 2005. More Golay sequences. IEEE Transactions on Information Theory Vol. 51, 3 (2005), 1141--1145.

Digital Library

[25]

Jia Hui Liang, Pascal Poupart, Krzysztof Czarnecki, and Vijay Ganesh. 2017. An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate International Conference on Theory and Applications of Satisfiability Testing. Springer, 119--135.

[26]

A. Lomayev, Y.P. Gagiev, A. Maltsev, A. Kasher, M. Genossar, and C. Cordeiro. 2017. Golay sequences for wireless networks. https://www.google.com/patents/US20170324461 US Patent App. 15/280,635.

[27]

Michael B. Monagan, Keith O. Geddes, K. Michael Heal, George Labahn, Stefan M. Vorkoetter, James McCarron, and Paul DeMarco. 2005. Maple 10 Programming Guide. Maplesoft, Waterloo ON, Canada.

[28]

Moshe Nazarathy, Steven A Newton, RP Giffard, DS Moberly, F Sischka, WR Trutna, and S Foster. 1989. Real-time long range complementary correlation optical time domain reflectometer. Journal of Lightwave Technology Vol. 7, 1 (1989), 24--38.

[29]

A Nowicki, W Secomski, J Litniewski, I Trots, and PA Lewin. 2003. On the application of signal compression using Golay's codes sequences in ultrasound diagnostic. Archives of Acoustics Vol. 28, 4 (2003).

[30]

Kenneth G Paterson. 2000. Generalized Reed-Muller codes and power control in OFDM modulation. IEEE Transactions on Information Theory Vol. 46, 1 (2000), 104--120.

Digital Library

[31]

Joe Riel. 2006. nsoks: A Maple script for writing n as a sum of k squares. http://www.swmath.org/software/21060.

[32]

Edward Zulkoski, Curtis Bright, Albert Heinle, Ilias S. Kotsireas, Krzysztof Czarnecki, and Vijay Ganesh. 2017. Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures. J. Autom. Reasoning Vol. 58, 3 (2017), 313--339.

Digital Library

Cited By

Brodzik A(2025)Almost Two-Valued Periodic Golay Sequence Pairs Derived From the Legendre SymbolIEEE Transactions on Information Theory10.1109/TIT.2024.349142271:1(737-751)Online publication date: Jan-2025
https://doi.org/10.1109/TIT.2024.3491422
Bright CKotsireas IGanesh V(2020)Applying computer algebra systems with SAT solvers to the Williamson conjectureJournal of Symbolic Computation10.1016/j.jsc.2019.07.024100:C(187-209)Online publication date: 1-Jul-2020
https://dl.acm.org/doi/10.1016/j.jsc.2019.07.024
Bright CCheung KStevens BRoy DKotsireas IGanesh V(2020)A nonexistence certificate for projective planes of order ten with weight 15 codewordsApplicable Algebra in Engineering, Communication and Computing10.1007/s00200-020-00426-yOnline publication date: 15-Apr-2020
https://doi.org/10.1007/s00200-020-00426-y
Show More Cited By

Recommendations

Applying computer algebra systems with SAT solvers to the Williamson conjecture
Abstract
We employ tools from the fields of symbolic computation and satisfiability checking—namely, computer algebra systems and SAT solvers—to study the Williamson conjecture from combinatorial design theory and increase the bounds to which ...
A modular CNF-based SAT solver
SBCCI '10: Proceedings of the 23rd symposium on Integrated circuits and system design

The state-of-the-art SAT solvers, such as Chaff [11], zChaff [18], BerkMin [5], and Minisat [2] usually share the same core techniques, for instance: the watched literals structures conflict clause recording and non-chronological backtracking. ...
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)

We first introduce Abstract DPLL, a rule-based formulation of the Davis--Putnam--Logemann--Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and to formally reason ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

ISSAC '18: Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation

July 2018

418 pages

ISBN:9781450355506

DOI:10.1145/3208976

Editor:
Carlos Arreche
University of Texas at Dallas, USA
,
General Chairs:
Manuel Kauers
Johannes Kepler University, Austria
,
Alexey Ovchinnikov
City University of New York, USA
,
Program Chair:
Éric Schost
University of Waterloo, Canada

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

In-Cooperation

SIGSAM: ACM Special Interest Group on Symbolic and Algebraic Manipulation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 July 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ISSAC '18

ISSAC '18: International Symposium on Symbolic and Algebraic Computation

July 16 - 19, 2018

NY, New York, USA

Acceptance Rates

Overall Acceptance Rate 395 of 838 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
70
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)1

Reflects downloads up to 17 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Brodzik A(2025)Almost Two-Valued Periodic Golay Sequence Pairs Derived From the Legendre SymbolIEEE Transactions on Information Theory10.1109/TIT.2024.349142271:1(737-751)Online publication date: Jan-2025
https://doi.org/10.1109/TIT.2024.3491422
Bright CKotsireas IGanesh V(2020)Applying computer algebra systems with SAT solvers to the Williamson conjectureJournal of Symbolic Computation10.1016/j.jsc.2019.07.024100:C(187-209)Online publication date: 1-Jul-2020
https://dl.acm.org/doi/10.1016/j.jsc.2019.07.024
Bright CCheung KStevens BRoy DKotsireas IGanesh V(2020)A nonexistence certificate for projective planes of order ten with weight 15 codewordsApplicable Algebra in Engineering, Communication and Computing10.1007/s00200-020-00426-yOnline publication date: 15-Apr-2020
https://doi.org/10.1007/s00200-020-00426-y
Bright CKotsireas IGanesh V(2019)SAT solvers and computer algebra systemsProceedings of the 29th Annual International Conference on Computer Science and Software Engineering10.5555/3370272.3370309(323-328)Online publication date: 4-Nov-2019
https://dl.acm.org/doi/10.5555/3370272.3370309
Huang PLiu MGe CMa FZhang JDavenport JWang DKauers MBradford R(2019)Investigating the Existence of Orthogonal Golf Designs via Satisfiability TestingProceedings of the 2019 International Symposium on Symbolic and Algebraic Computation10.1145/3326229.3326232(203-210)Online publication date: 8-Jul-2019
https://dl.acm.org/doi/10.1145/3326229.3326232
Bright CKotsireas IHeinle AGanesh V(2019)Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SATJournal of Symbolic Computation10.1016/j.jsc.2019.10.013Online publication date: Oct-2019
https://doi.org/10.1016/j.jsc.2019.10.013

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents