×

The SAT+CAS method for combinatorial search with applications to best matrices. (English) Zbl 1434.05001

Authors’ abstract: “In this paper, we provide an overview of the SAT+CAS method that combines satisfiability checkers (SAT solvers) and computer algebra systems (CAS) to resolve combinatorial conjectures, and present new results on vis-à-vis best matrices. The SAT+CAS method is a variant of the Davis-Putnam-Logemann-Loveland DPLL(\(T\) ) architecture, where the \(T\) solver is replaced by a CAS. We describe how the SAT+CAS method has been previously used to resolve many open problems from graph theory, combinatorial design theory, and number theory, showing that the method has broad applications across a variety of fields. Additionally, we apply the method to construct the largest best matrices yet known and present new skew Hadamard matrices constructed from best matrices. We show the best matrix conjecture (that best matrices exist in all orders of the form \(r^{2}+r+1\)) which was previously known to hold for \(r\leq 6\) also holds for \(r = 7\). We also confirmed the results of the exhaustive searches that have been previously completed for \(r\leq 6\).”
The authors proved for the first time that best matrices exist for \(r = 7\) by explicitly constructing best matrices of order 57 – the largest best matrices currently known.

MSC:

05-04 Software, source code, etc. for problems pertaining to combinatorics
05B20 Combinatorial aspects of matrices (incidence, Hadamard, etc.)
68R05 Combinatorics in computer science
68T27 Logic in artificial intelligence
68W30 Symbolic computation and algebraic computation
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Ábrahám, E.: Building bridges between symbolic computation and satisfiability checking. In: Linton, S. (ed.) Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation, pp 1-6. ACM (2015) · 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.: SC^2: satisfiability checking meets symbolic computation. Intelligent Computer Mathematics: Proceedings CICM, 28-43 (2016) · Zbl 1344.68198
[3] Ahmed, T.; Kullmann, O.; Snevily, H., On the van der Waerden numbers w(2; 3,t), Discret. Appl. Math., 174, 27-51 (2014) · Zbl 1298.05313
[4] Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chap. 26, pp. 825-885. IOS Press (2009)
[5] Bernardin, L., Chin, P., DeMarco, P., Geddes, K.O., Hare, D.E.G., Heal, K.M., Labahn, G., May, J.P., McCarron, J., Monagan, M.B., Ohashi, D., Vorkoetter, S.M.: Maple programming guide (2018)
[6] Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009) · Zbl 1183.68568
[7] Borwein, Peter, Barker Polynomials and Golay Pairs, Computational Excursions in Analysis and Number Theory, 109-119 (2002), New York, NY: Springer New York, New York, NY · Zbl 1020.12001
[8] Botinčan, M.; Parkinson, M.; Schulte, W., Separation logic verification of C programs with an SMT solver, Electron. Notes Theor. Comput. Sci., 254, 5-23 (2009)
[9] Bright, C., ĐokoviĆ, D.Ž., Kotsireas, I., Ganesh, V.: A SAT+CAS approach to finding good matrices: new examples and counterexamples. In: Hentenryck, P.V., Zhou, Z.H. (eds.) Thirty-third AAAI Conference on Artificial Intelligence. AAAI Press (2019) · Zbl 1434.05001
[10] Bright, C., Ganesh, V., Heinle, A., Kotsireas, I., Nejati, S., Czarnecki, K.: Mathcheck2: a SAT+CAS verifier for combinatorial conjectures. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) International Workshop on Computer Algebra in Scientific Computing, pp 117-133. Springer (2016) · Zbl 1453.05001
[11] Bright, C., Kotsireas, I., Ganesh, V.: A SAT+CAS method for enumerating Williamson matrices of even order. In: Mcilraith, S.A., Weinberger, K.Q. (eds.) Thirty-second AAAI Conference on Artificial Intelligence, pp. 6573-6580. AAAI Press (2018)
[12] Bright, C.; Kotsireas, I.; Ganesh, V., The SAT+CAS paradigm and the Williamson conjecture, ACM Commun. Comput. Algebra, 52, 3, 82-84 (2018) · Zbl 07045168
[13] Bright, C., Kotsireas, I., Ganesh, V.: Applying computer algebra systems with SAT solvers to the Williamson conjecture. J. Symbolic Comput. (to appear) · Zbl 07045168
[14] Bright, C., Kotsireas, I., Heinle, A., Ganesh, V.: Enumeration of complex Golay pairs via programmatic SAT. In: Arreche, C. (ed.) Proceedings of the 2018 ACM on International Symposium on Symbolic and Algebraic Computation, ISSAC 2018, New York, NY, USA, July 16-19, 2018, pp. 111-118 (2018) · Zbl 1467.68202
[15] Bright, C., Kotsireas, I., Heinle, A., Ganesh, V.: Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT. J. Symbolic Comput. (to appear) · Zbl 1468.68276
[16] Cadar, C.; Ganesh, V.; Pawlowski, Pm; Dill, Dl; Engler, Dr, EXE: automatically generating inputs of death, ACM Trans. Inform. Sys. Secur. (TISSEC), 12, 2, 1-38 (2008)
[17] Cimatti, A.; Griggio, A.; Irfan, A.; Roveri, M.; Sebastiani, R., Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions, ACM Trans. Comput. Logic (TOCL), 19, 3, 19:1-19:52 (2018) · Zbl 1407.68285
[18] Cimatti, A., Sebastiani, R.: Building efficient decision procedures on top of SAT solvers. In: Bernardo, M., Cimatti, A. (eds.) International School on Formal Methods for the Design of Computer, Communication and Software Systems, pp. 144-175. Springer (2006) · Zbl 1182.68114
[19] Craigen, R.; Holzmann, W.; Kharaghani, H., Complex Golay sequences: structure and applications, Discrete Mathematics, 252, 1-3, 73-89 (2002) · Zbl 0993.05034
[20] Craigen, R., Kharaghani, H.: Hadamard matrices and Hadamard designs. In: Colbourn, C.J., Dinitz, J.H. (eds.) Handbook of Combinatorial Designs, pp 273-280. Chapman & Hall/CRC, Boca Raton (2007)
[21] de Moura, L., Bjørner, N.: The Z3 theorem prover. https://github.com/Z3Prover(2008)
[22] Doković, Dž, Skew-Hadamard matrices of orders 188 and 388 exist, Int. Math. Forum, 3, 22, 1063-1068 (2008) · Zbl 1157.05308
[23] Doković, Dž, Supplementary difference sets with symmetry for Hadamard matrices, Operators and Matrices, 3, 4, 557-569 (2009) · Zbl 1286.05015
[24] Doković, Dž; Kotsireas, Is, Compression of periodic complementary sequences and applications, Des. Codes Crypt., 74, 2, 365-377 (2015) · Zbl 1307.05033
[25] Đoković, Dž; Kotsireas, Is, Goethals-Seidel difference families with symmetric or skew base blocks, Math. Comput. Sci., 12, 4, 373-388 (2018) · Zbl 1444.05028
[26] Dransfield, Michael R.; Marek, Victor W.; Truszczyński, Mirosław, Satisfiability and Computing van der Waerden Numbers, Theory and Applications of Satisfiability Testing, 1-13 (2004), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1204.05097
[27] Dutertre, B., de Moura, L.: The Yices SMT solver. http://yices.csl.sri.com/(2006)
[28] Fiedler, Frank, Small Golay sequences, Advances in Mathematics of Communications, 7, 4, 379-407 (2013) · Zbl 1283.94043
[29] Fink, J., Perfect matchings extend to Hamilton cycles in hypercubes, Journal of Combinatorial Theory, Series B, 97, 6, 1074-1076 (2007) · Zbl 1126.05080
[30] Frigo, M.; Johnson, Sg, The design and implementation of FFTW3, Proc. IEEE, 93, 2, 216-231 (2005)
[31] Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, pp. 519-531 (2007) · Zbl 1135.68472
[32] Ganesh, Vijay; O’Donnell, Charles W.; Soos, Mate; Devadas, Srinivas; Rinard, Martin C.; Solar-Lezama, Armando, Lynx: A Programmatic SAT Solver for the RNA-Folding Problem, Theory and Applications of Satisfiability Testing - SAT 2012, 143-156 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[33] Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) International Conference on Computer Aided Verification, pp. 175-188. Springer (2004) · Zbl 1103.68616
[34] Georgiou, S.; Koukouvinos, C.; Seberry, J., On circulant best matrices and their applications, Linear and Multilinear Algebra, 48, 3, 263-274 (2001) · Zbl 1007.05031
[35] Goethals, Jm; Seidel, Jj, A skew Hadamard matrix of order 36, J. Aust. Math. Soc., 11, 3, 343-344 (1970) · Zbl 0226.05015
[36] Golay, Mje, Multi-slit spectrometry, JOSA, 39, 6, 437-444 (1949)
[37] Golomb, Sw; Baumert, Ld, The search for Hadamard matrices, Am. Math. Mon., 70, 1, 12-17 (1963) · Zbl 0112.01205
[38] Hedayat, A.; Wallis, Wd, Hadamard matrices and their applications, Ann. Stat., 6, 6, 1184-1238 (1978) · Zbl 0401.62061
[39] Heule, M.J.H.: Schur number five. In: Mcilraith, S.A., Weinberger, K.Q. (eds.) Thirty-Second AAAI Conference on Artificial Intelligence, pp. 6598-6606. AAAI Press (2018)
[40] Heule, Mjh; Kullmann, O., The science of brute force, Commun. ACM, 60, 8, 70-79 (2017)
[41] Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W., Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer, Theory and Applications of Satisfiability Testing - SAT 2016, 228-245 (2016), Cham: Springer International Publishing, Cham · Zbl 1403.68226
[42] Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving very hard problems: cube-and-conquer, a hybrid SAT solving method. In: Sierra, C. (ed.) Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, pp. 4864-4868 (2017)
[43] Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and Conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenço, J.S, Shehory, O. (eds.) Haifa Verification Conference, pp 50-65. Springer (2011)
[44] Heule, M.J.H., van Maaren, H.: Look-ahead based SAT Solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chap. 5, pp. 155-184. IOS Press (2009)
[45] Holzmann, Wh; Kharaghani, H.; Tayfeh-Rezaie, B., Williamson matrices up to order 59, Des. Codes Crypt., 46, 3, 343-352 (2008) · Zbl 1179.05023
[46] Horadam, K.J.: Hadamard matrices and their applications. Princeton University Press (2012) · Zbl 1145.05014
[47] Kharaghani, H.; Tayfeh-Rezaie, B., A Hadamard matrix of order 428, J. Comb. Des., 13, 6, 435-440 (2005) · Zbl 1076.05017
[48] Kim, J.; Solé, P., Skew Hadamard designs and their codes, Des. Codes Crypt., 49, 1-3, 135-145 (2008) · Zbl 1179.05024
[49] Konev, Boris; Lisitsa, Alexei, A SAT Attack on the Erdős Discrepancy Conjecture, Lecture Notes in Computer Science, 219-226 (2014), Cham: Springer International Publishing, Cham · Zbl 1343.68217
[50] Kotsireas, Is; Koukouvinos, C., Constructions for Hadamard matrices of Williamson type, J. Comb. Math. Comb. Comput., 59, 17-32 (2006) · Zbl 1122.05020
[51] Kotsireas, Is; Koukouvinos, C., Hadamard matrices of Williamson type: a challenge for computer algebra, J. Symb. Comput., 44, 3, 271-279 (2009) · Zbl 1158.13315
[52] Kotsireas, Is; Koukouvinos, C.; Seberry, J., Weighing matrices and string sorting, Ann. Comb., 13, 3, 305-313 (2009) · Zbl 1229.05055
[53] Koukouvinos, C.; Stylianou, S., On skew-Hadamard matrices, Discret. Math., 308, 13, 2723-2731 (2008) · Zbl 1159.05011
[54] Kouril, Michal; Franco, John, Resolution Tunnels for Improved SAT Solver Performance, Theory and Applications of Satisfiability Testing, 143-157 (2005), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1128.68468
[55] Kouril, M.; Paul, Jl, The van der Waerden number W(2, 6) is 1132, Exp. Math., 17, 1, 53-61 (2008) · Zbl 1151.05048
[56] Kullmann, Oliver, Green-Tao Numbers and SAT, Theory and Applications of Satisfiability Testing - SAT 2010, 352-362 (2010), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1259.68182
[57] Liang, Jia Hui; V. K., Hari Govind; Poupart, Pascal; Czarnecki, Krzysztof; Ganesh, Vijay, An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate, Theory and Applications of Satisfiability Testing - SAT 2017, 119-135 (2017), Cham: Springer International Publishing, Cham · Zbl 1496.68304
[58] Lynce, I., Ouaknine, J.: Sudoku as a SAT problem. In: 9th International Symposium on Artificial Intelligence and Mathematics (2006)
[59] MacWilliams, F.J., Sloane, N.J.A.: The theory of error-correcting codes, vol. 16 Elsevier (1977) · Zbl 0369.94008
[60] Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of satisfiability, chap. 4, pp. 131-153. IOS Press (2009)
[61] McCune, W.: A Davis-Putnam Program and Its Application to Finite First-Order Model Search: Quasigroup Existence Problems. Tech. rep., Argonne National Laboratory (1994)
[62] Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), Journal of the ACM, 53, 6, 937-977 (2006) · Zbl 1326.68164
[63] Pratt, Wk; Kane, J.; Andrews, Hc, Hadamard transform image coding, Proc. IEEE, 57, 1, 58-68 (1969)
[64] Rao, Jnk; Shao, J., On balanced half-sample variance estimation in stratified random sampling, J. Am. Stat. Assoc., 91, 433, 343-348 (1996) · Zbl 0871.62013
[65] Ruskey, F.; Savage, C., Hamilton cycles that extend transposition matchings in Cayley graphs of sn, SIAM J. Discret. Math., 6, 1, 152-166 (1993) · Zbl 0771.05050
[66] Seberry, J., On skew Hadamard matrices, Ars Combinatoria, 6, 255-275 (1978) · Zbl 0414.05008
[67] Seberry, J., Yamada, M.: Hadamard matrices, sequences, and block designs. Contemporary design theory: a collection of surveys, pp. 431-560 (1992) · Zbl 0776.05028
[68] Stickel, M.E., Zhang, H.: First results of studying quasigroup identities by rewriting techniques. In: Proceedings of Workshop on Automated Theorem Proving in conjunction with FGCS, pp. 16-23 (1994)
[69] Sylvester, Jj, Thoughts on inverse orthogonal matrices, simultaneous signsuccessions, and tessellated pavements in two or more colours, with applications to Newton’s rule, ornamental tile-work, and the theory of numbers, The London, Edinburgh, and Dublin Philosophical Magazine and Journal of Science, 34, 232, 461-475 (1867)
[70] Taghavi, M.; Zahraei, M., On the autocorrelations of ± 1 polynomials, Journal of Mathematical Extension, 1, 2, 139-147 (2007) · Zbl 1285.94035
[71] The Sage Development Team: Sage tutorial, release 8.6. https://www.sagemath.org(2019)
[72] Van Der Waerden, Blbl, Beweis einer Baudetschen vermutung, Nieuw Archief voor Wiskunde, 15, 212-216 (1927) · JFM 53.0073.12
[73] Vardi, Moshe Y., Symbolic Techniques in Propositional Satisfiability Solving, Lecture Notes in Computer Science, 2-3 (2009), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[74] Vizel, Y.; Weissenbacher, G.; Malik, S., Boolean satisfiability solvers and their applications in model checking, Proc. IEEE, 103, 11, 2021-2035 (2015)
[75] Williamson, J., Hadamard’s determinant theorem and the sum of four squares, Duke Mathematical Journal, 11, 1, 65-81 (1944) · Zbl 0060.03202
[76] Wolfram, S.: The Mathematica Book, fifth edition (2003)
[77] Zhang, H.: Specifying latin square problems in propositional logic. In: Veroff, R. (ed.) Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, pp. 115-146. MIT Press (1997) · Zbl 0928.68101
[78] Zhang, H.: Combinatorial designs by SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chap. 17, pp. 533-568. IOS Press (2009)
[79] Zulkoski, E.; Bright, C.; Heinle, A.; Kotsireas, I.; 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
[80] Zulkoski, Edward; Ganesh, Vijay; Czarnecki, Krzysztof, MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers, Automated Deduction - CADE-25, 607-622 (2015), Cham: Springer International Publishing, Cham · Zbl 1465.68300
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.