zbMATH — the first resource for mathematics

Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT. (English) Zbl 07249901
Summary: We use techniques from the fields of computer algebra and satisfiability checking to develop a new algorithm to search for complex Golay pairs. We implement this algorithm and use it to perform a complete search for complex Golay pairs of lengths up to 28. In doing so, we find that complex Golay pairs exist in the lengths 24 and 26 but do not exist in the lengths 23, 25, 27, and 28. This independently verifies work done by F. Fiedler [Adv. Math. Commun. 7, No. 4, 379–407 (2013; Zbl 1283.94043)] and confirms the conjecture of R. Craigen et al. [Discrete Math. 252, No. 1–3, 73–89 (2002; Zbl 0993.05034)] that complex Golay pairs of length 23 don’t exist. Our algorithm is based on the recently proposed SAT+CAS paradigm of combining SAT solvers with computer algebra systems to efficiently search large spaces specified by both algebraic and logical constraints. The algorithm has two stages: first, a fine-tuned computer program uses functionality from computer algebra systems and numerical libraries to construct a list containing every sequence that could appear as the first sequence in a complex Golay pair up to equivalence. Second, a programmatic SAT solver constructs every sequence (if any) that pair off with the sequences constructed in the first stage to form a complex Golay pair.
This extends work originally presented by the authors [in: Proceedings of the 43rd international symposium on symbolic and algebraic computation, ISSAC 2018. New York, NY: Association for Computing Machinery (ACM). 111–118 (2018; Zbl 1467.68202)]; we discuss and implement several improvements to our algorithm that enabled us to improve the efficiency of the search and increase the maximum length we search from length 25 to 28.
MSC:
 68V05 Computer assisted proofs of proofs-by-exhaustion type 05A15 Exact enumeration problems, generating functions 11B83 Special sequences and polynomials 68R07 Computational aspects of satisfiability 68W30 Symbolic computation and algebraic computation 94A55 Shift register sequences and sequences over finite alphabets in information and communication theory
Software:
SMT-LIB; nsoks; Maple; Lynx; FFTW; MathCheck
Full Text:
References:
 [1] Ábrahám, E., Building bridges between symbolic computation and satisfiability checking, (Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation (2015), ACM: ACM New York), 1-6 · Zbl 1345.68279 [2] Ábrahám, E.; Abbott, J.; Becker, B.; Bigatti, A. M.; Brain, M.; Buchberger, B.; Cimatti, A.; Davenport, J. H.; England, M.; Fontaine, P.; Forrest, S.; Griggio, A.; Kroening, D.; Seiler, W. M.; Sturm, T., $$\text{SC}^2$$: satisfiability checking meets symbolic computation, (Intelligent Computer Mathematics: 9th International Conference. Intelligent Computer Mathematics: 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings (2016), Springer International Publishing: Springer International Publishing Cham), 28-43 · Zbl 1344.68198 [3] Barrett, C.; Fontaine, P.; Tinelli, C., The Satisfiability Modulo Theories Library (SMT-LIB) (2016) [4] Bright, C., Computational Methods for Combinatorial and Number Theoretic Problems (2017), University of Waterloo, Ph.D. thesis [5] Bright, C.; Ganesh, V.; Heinle, A.; Kotsireas, I. S.; Nejati, S.; Czarnecki, K., MathCheck2: a SAT+CAS verifier for combinatorial conjectures, (Computer Algebra in Scientific Computing-18th International Workshop. Computer Algebra in Scientific Computing-18th International Workshop, CASC 2016, Bucharest, Romania, September 19-23, 2016, Proceedings (2016)), 117-133 · Zbl 1453.05001 [6] Bright, C.; Kotsireas, I.; Ganesh, V., A SAT+CAS method for enumerating Williamson matrices of even order, (Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence. Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, New Orleans, Louisiana, USA, February 2-7, 2018 (2018)), 6573-6580 [7] Bright, C.; Kotsireas, I. S.; Heinle, A.; Ganesh, V., Enumeration of complex Golay pairs via programmatic SAT, (Proceedings of the 2018 ACM on International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2018 ACM on International Symposium on Symbolic and Algebraic Computation, ISSAC 2018, New York, NY, USA, July 16-19, 2018. (2018)), 111-118 [8] Bright, C.; Đoković, D.Ž.; Kotsireas, I.; Ganesh, V., A SAT+CAS approach to finding good matrices: new examples and counterexamples, (Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence. Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, Honolulu, Hawaii, USA, January 27-February 1, 2019 (2019)), 1435-1442 [9] Craigen, R., Complex Golay sequences, J. Comb. Math. Comb. Comput., 15, 161-169 (1994) · Zbl 0808.05020 [10] Craigen, R.; Holzmann, W.; Kharaghani, H., Complex Golay sequences: structure and applications, Discrete Math., 252, 1-3, 73-89 (2002) · Zbl 0993.05034 [11] Davis, J. A.; Jedwab, J., Peak-to-mean power control in OFDM, Golay complementary sequences, and Reed-Muller codes, IEEE Trans. Inf. Theory, 45, 7, 2397-2417 (1999) · Zbl 0960.94012 [12] Donato, P. G.; Urena, J.; Mazo, M.; Alvarez, F., Train wheel detection without electronic equipment near the rail line, (IEEE Intelligent Vehicles Symposium (2004)), 876-880 [13] Fiedler, F., Small Golay sequences, Adv. Math. Commun., 7, 4, Article 10.3934/amc.2013.7.379 pp. (2013) [14] Fiedler, F.; Jedwab, J.; Parker, M. G., A framework for the construction of Golay sequences, IEEE Trans. Inf. Theory, 54, 7, 3114-3129 (2008) · Zbl 1328.94056 [15] Fiedler, F.; Jedwab, J.; Parker, M. G., A multi-dimensional approach to the construction and enumeration of Golay complementary sequences, J. Comb. Theory, Ser. A, 115, 5, 753-776 (2008) · Zbl 1154.05012 [16] Frank, R., Polyphase complementary codes, IEEE Trans. Inf. Theory, 26, 6, 641-647 (1980) [17] Frigo, M.; Johnson, S. G., The design and implementation of FFTW3, Proc. IEEE, 93, 2, 216-231 (2005) [18] Ganesh, V.; O’Donnell, C. W.; Soos, M.; Devadas, S.; Rinard, M. C.; Solar-Lezama, A., Lynx: a programmatic SAT solver for the RNA-folding problem, (International Conference on Theory and Applications of Satisfiability Testing (2012), Springer), 143-156 [19] Gersho, A.; Gopinath, B.; Odlyzko, A., Coefficient inaccuracy in transversal filtering, Bell Syst. Tech. J., 58, 10, 2301-2316 (1979) · Zbl 0423.93053 [20] Gibson, R. G.; Jedwab, J., Quaternary Golay sequence pairs I: even length, Des. Codes Cryptogr., 59, 1-3, 131-146 (2011) · Zbl 1233.94013 [21] Golay, M., Complementary series, IRE Trans. Inf. Theory, 7, 2, 82-87 (1961) [22] Golay, M. J., Multi-slit spectrometry, J. Opt. Soc. Am., 39, 6, 437-444 (1949) [23] Holzmann, W. H.; Kharaghani, H., A computer search for complex Golay sequences, Australas. J. Comb., 10, 251-258 (1994) · Zbl 0818.05022 [24] Kotsireas, I. S., Algorithms and metaheuristics for combinatorial matrices, (Handbook of Combinatorial Optimization (2013), Springer), 283-309 [25] Kotsireas, I. S.; Koukouvinos, C.; Seberry, J., Weighing matrices and string sorting, Ann. Comb., 13, 3, 305-313 (2009) · Zbl 1229.05055 [26] Krone, S.; Sarwate, D., Quadriphase sequences for spread-spectrum multiple-access communication, IEEE Trans. Inf. Theory, 30, 3, 520-529 (1984) · Zbl 0544.94006 [27] Li, S.; Chen, J.; Zhang, L.; Zhou, Y., Construction of quadri-phase complete complementary pairs applied in MIMO radar systems, (ICSP 2008: 9th International Conference on Signal Processing (2008), IEEE), 2298-2301 [28] Li, Y.; Chu, W. B., More Golay sequences, IEEE Trans. Inf. Theory, 51, 3, 1141-1145 (2005) · Zbl 1309.94128 [29] Liang, J. H.; Poupart, P.; Czarnecki, K.; Ganesh, V., An empirical study of branching heuristics through the lens of global learning rate, (International Conference on Theory and Applications of Satisfiability Testing (2017), Springer), 119-135 · Zbl 06807222 [30] Lomayev, A.; Gagiev, Y.; Maltsev, A.; Kasher, A.; Genossar, M.; Cordeiro, C., Golay sequences for wireless networks (2017), US Patent App. 15/280,635 [31] Monagan, M. B.; Geddes, K. O.; Heal, K. M.; Labahn, G.; Vorkoetter, S. M.; McCarron, J.; DeMarco, P., Maple 10 Programming Guide (2005), Maplesoft: Maplesoft Waterloo ON, Canada [32] Nazarathy, M.; Newton, S. A.; Giffard, R.; Moberly, D.; Sischka, F.; Trutna, W.; Foster, S., Real-time long range complementary correlation optical time domain reflectometer, J. Lightwave Technol., 7, 1, 24-38 (1989) [33] Nowicki, A.; Secomski, W.; Litniewski, J.; Trots, I.; Lewin, P., On the application of signal compression using Golay’s codes sequences in ultrasound diagnostic, Arch. Acoust., 28, 4 (2003) [34] Popović, B. M., Synthesis of power efficient multitone signals with flat amplitude spectrum, IEEE Trans. Commun., 39, 7, 1031-1033 (1991) [35] Riel, J., nsoks: a Maple script for writing n as a sum of k squares (2006) [36] Seberry, J. R.; Wysocki, B. J.; Wysocki, T. A., On a use of Golay sequences for asynchronous DS CDMA applications, (Advanced Signal Processing for Communication Systems (2002), Springer), 183-196 [37] Sivaswamy, R., Multiphase complementary codes, IEEE Trans. Inf. Theory, 24, 5, 546-552 (1978) · Zbl 0383.94024 [38] Sun, W.; Yuan, Y., Optimization Theory and Methods: Nonlinear Programming (2006), Springer Science & Business Media [39] Tseng, C. C., Signal multiplexing in surface-wave delay lines using orthogonal pairs of Golay’s complementary sequences, IEEE Trans. Sonics Ultrason., 18, 2, 103-107 (1971) [40] Zulkoski, E.; Bright, C.; Heinle, A.; Kotsireas, I. S.; Czarnecki, K.; Ganesh, V., Combining SAT solvers with computer algebra systems to verify combinatorial conjectures, J. Autom. Reason., 58, 3, 313-339 (2017) · Zbl 1410.68413
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.