{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:02:02Z","timestamp":1760061722429},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319456409"},{"type":"electronic","value":"9783319456416"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-45641-6_9","type":"book-chapter","created":{"date-parts":[[2016,9,8]],"date-time":"2016-09-08T06:30:29Z","timestamp":1473316229000},"page":"117-133","source":"Crossref","is-referenced-by-count":7,"title":["MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures"],"prefix":"10.1007","author":[{"given":"Curtis","family":"Bright","sequence":"first","affiliation":[]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[]},{"given":"Albert","family":"Heinle","sequence":"additional","affiliation":[]},{"given":"Ilias","family":"Kotsireas","sequence":"additional","affiliation":[]},{"given":"Saeed","family":"Nejati","sequence":"additional","affiliation":[]},{"given":"Krzysztof","family":"Czarnecki","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,9]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m, E.: Building bridges between symbolic computation and satisfiability checking. In: Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation, pp. 1\u20136. ACM, New York (2015)","DOI":"10.1145\/2755996.2756636"},{"key":"9_CR2","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Wener, B.: Verifying SAT and SMT in CoQ for a fully automated decision procedure. In: PSATTT 2011: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, pp. 11\u201325 (2011)"},{"key":"9_CR3","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)"},{"issue":"3","key":"9_CR4","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1006\/jsco.1996.0125","volume":"24","author":"W Bosma","year":"1997","unstructured":"Bosma, W., Cannon, J., Playoust, C.: The Magma algebra system I: the user language. J. Symbolic Comput. 24(3), 235\u2013265 (1997)","journal-title":"J. Symbolic Comput."},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-Solver. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009)"},{"issue":"2","key":"9_CR6","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/S0747-7171(86)80021-9","volume":"2","author":"BW Char","year":"1986","unstructured":"Char, B.W., Fee, G.J., Geddes, K.O., Gonnet, G.H., Monagan, M.B.: A tutorial introduction to Maple. J. Symbolic Comput. 2(2), 179\u2013200 (1986)","journal-title":"J. Symbolic Comput."},{"key":"9_CR7","unstructured":"Colbourn, C.J., Dinitz, J.H. (eds.): Handbook of Combinatorial Designs. Discrete Mathematics and its Applications (Boca Raton), 2nd edn. Chapman & Hall\/CRC, Boca Raton (2007)"},{"key":"9_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2181-2","volume-title":"Ideals, Varieties, and Algorithms","author":"D Cox","year":"1992","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms, 2nd edn. Springer, New York (1992)","edition":"2"},{"key":"9_CR9","unstructured":"Decker, W., Greuel, G.M., Pfister, G., Sch\u00f6nemann, H.: Singular 4-0-2 \u2013 A computer algebra system for polynomial computations (2015). http:\/\/www.singular.uni-kl.de"},{"issue":"1","key":"9_CR10","first-page":"240","volume":"17","author":"J Hadamard","year":"1893","unstructured":"Hadamard, J.: R\u00e9solution d\u2019une question relative aux d\u00e9terminants. Bull. Sci. Math. 17(1), 240\u2013246 (1893)","journal-title":"Bull. Sci. Math."},{"key":"9_CR11","unstructured":"Hearn, A.: Reduce user\u2019s manual, version 3.8 (2004)"},{"issue":"6","key":"9_CR12","doi-asserted-by":"crossref","first-page":"1184","DOI":"10.1214\/aos\/1176344370","volume":"6","author":"A Hedayat","year":"1978","unstructured":"Hedayat, A., Wallis, W.: Hadamard matrices and their applications. Ann. Stat. 6(6), 1184\u20131238 (1978)","journal-title":"Ann. Stat."},{"issue":"2","key":"9_CR13","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/s10601-006-7094-9","volume":"11","author":"B Hnich","year":"2006","unstructured":"Hnich, B., Prestwich, S.D., Selensky, E., Smith, B.M.: Constraint models for the covering test problem. Constraints 11(2), 199\u2013219 (2006)","journal-title":"Constraints"},{"issue":"3","key":"9_CR14","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/s10623-007-9163-5","volume":"46","author":"WH Holzmann","year":"2008","unstructured":"Holzmann, W.H., Kharaghani, H., Tayfeh-Rezaie, B.: Williamson matrices up to order 59. Des. Codes Crypt. 46(3), 343\u2013352 (2008)","journal-title":"Des. Codes Crypt."},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/978-3-642-40663-8_18","volume-title":"Algebraic Informatics","author":"S Junges","year":"2013","unstructured":"Junges, S., Loup, U., Corzilius, F., \u00c1brah\u00e1m, E.: On Gr\u00f6bner bases in the context of satisfiability-modulo-theories solving over the real numbers. In: Muntean, T., Poulakis, D., Rolland, R. (eds.) CAI 2013. LNCS, vol. 8080, pp. 186\u2013198. Springer, Heidelberg (2013)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/978-3-319-09284-3_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"B Konev","year":"2014","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the Erd\u0151s discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 219\u2013226. Springer, Heidelberg (2014)"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Kotsireas, I.S.: Algorithms and metaheuristics for combinatorial matrices. In: Handbook of Combinatorial Optimization, pp. 283\u2013309. Springer, New York (2013)","DOI":"10.1007\/978-1-4419-7997-1_13"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-40970-2_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"JH Liang","year":"2016","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D., Le Berre, D., Le Berre, D., Le Berre, D., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123\u2013140. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-40970-2_9"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Exponential recency weighted average branching heuristic for SAT solvers. In: Proceedings of AAAI 2016 (2016)","DOI":"10.1007\/978-3-319-40970-2_9"},{"issue":"5","key":"9_CR20","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K., et al.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530\u2013535. ACM, New York (2001)","DOI":"10.1145\/378239.379017"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction -Cade-25","author":"L Moura de","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, P.A., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 378\u2013388. Springer, Switzerland (2015)"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Muller, D.E.: Application of Boolean Algebra to Switching Circuit Design and to Error Detection. Electron. Comput. Trans. IRE Prof. Group Electron. Comput. EC-3(3), 6\u201312 (1954)","DOI":"10.1109\/IREPGELC.1954.6499441"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/978-3-642-31612-8_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 242\u2013255. Springer, Heidelberg (2012)"},{"issue":"1","key":"9_CR25","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0012-365X(93)90495-F","volume":"115","author":"D\u017d \u0110okovi\u0107","year":"1993","unstructured":"\u0110okovi\u0107, D.\u017d.: Williamson matrices of order $$4n$$ for $$n = 33$$ , $$35$$ , $$39$$ . Discrete Math. 115(1), 267\u2013271 (1993)","journal-title":"Discrete Math."},{"issue":"2","key":"9_CR26","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/s10623-013-9862-z","volume":"74","author":"D\u017d \u0110okovi\u0107","year":"2015","unstructured":"\u0110okovi\u0107, D.\u017d., Kotsireas, I.S.: Compression of periodic complementary sequences and applications. Des. Codes Crypt. 74(2), 365\u2013377 (2015)","journal-title":"Des. Codes Crypt."},{"issue":"1","key":"9_CR27","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1002\/sapm1933121311","volume":"12","author":"RE Paley","year":"1933","unstructured":"Paley, R.E.: On orthogonal matrices. J. Math. Phys. 12(1), 311\u2013320 (1933)","journal-title":"J. Math. Phys."},{"issue":"2","key":"9_CR28","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/s10601-012-9117-z","volume":"17","author":"SD Prestwich","year":"2012","unstructured":"Prestwich, S.D., Hnich, B., Simonis, H., Rossi, R., Tarim, S.A.: Partial symmetry breaking by local search in the group. Constraints 17(2), 148\u2013171 (2012)","journal-title":"Constraints"},{"issue":"4","key":"9_CR29","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/TIT.1954.1057465","volume":"4","author":"I Reed","year":"1954","unstructured":"Reed, I.: A class of multiple-error-correcting codes and the decoding scheme. Trans. IRE Prof. Group Inf. Theory 4(4), 38\u201349 (1954)","journal-title":"Trans. IRE Prof. Group Inf. Theory"},{"key":"9_CR30","unstructured":"Riel, J.: nsoks: A Maple script for writing $$n$$ as a sum of $$k$$ squares"},{"key":"9_CR31","unstructured":"Seberry, J.: Library of Williamson Matrices. http:\/\/www.uow.edu.au\/~jennie\/WILLIAMSON\/williamson.html"},{"key":"9_CR32","unstructured":"Sloane, N.: Library of Hadamard Matrices. http:\/\/neilsloane.com\/hadamard\/"},{"issue":"232","key":"9_CR33","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1080\/14786446708639914","volume":"34","author":"JJ Sylvester","year":"1867","unstructured":"Sylvester, J.J.: Thoughts on inverse orthogonal matrices, simultaneous sign successions, and tessellated pavements in two or more colours, with applications to Newton\u2019s rule, ornamental tile-work, and the theory of numbers. London Edinb. Dublin Philos. Mag. J. Sci. 34(232), 461\u2013475 (1867)","journal-title":"London Edinb. Dublin Philos. Mag. J. Sci."},{"key":"9_CR34","unstructured":"SC $${{}^{2}}$$ : Satisfiability checking and symbolic computation. http:\/\/www.sc-square.org\/"},{"key":"9_CR35","unstructured":"The Sage Developers: Sage Mathematics Software (Version 7.0) (2016). http:\/\/www.sagemath.org"},{"issue":"1","key":"9_CR36","doi-asserted-by":"crossref","first-page":"5","DOI":"10.2307\/2387224","volume":"45","author":"JL Walsh","year":"1923","unstructured":"Walsh, J.L.: A closed set of normal orthogonal functions. Am. J. Math. 45(1), 5\u201324 (1923)","journal-title":"Am. J. Math."},{"issue":"1","key":"9_CR37","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1215\/S0012-7094-44-01108-7","volume":"11","author":"J Williamson","year":"1944","unstructured":"Williamson, J.: Hadamard\u2019s determinant theorem and the sum of four squares. Duke Math. J 11(1), 65\u201381 (1944)","journal-title":"Duke Math. J"},{"key":"9_CR38","unstructured":"Wolfram, S.: The Mathematica Book, version 4. Cambridge University Press (1999)"},{"key":"9_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/978-3-319-21401-6_41","volume-title":"Automated Deduction - CADE-25","author":"E Zulkoski","year":"2015","unstructured":"Zulkoski, E., Ganesh, V., Czarnecki, K.: MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers. In: Felty, P.A., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 607\u2013622. Springer, Switzerland (2015)"}],"container-title":["Lecture Notes in Computer Science","Computer Algebra in Scientific Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-45641-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T04:12:05Z","timestamp":1568347925000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-45641-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319456409","9783319456416"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-45641-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}