{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T20:43:52Z","timestamp":1781901832226,"version":"3.54.5"},"reference-count":70,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,12,1]],"date-time":"2016-12-01T00:00:00Z","timestamp":1480550400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s10817-016-9396-y","type":"journal-article","created":{"date-parts":[[2016,12,1]],"date-time":"2016-12-01T09:40:40Z","timestamp":1480585240000},"page":"313-339","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1816-1614","authenticated-orcid":false,"given":"Edward","family":"Zulkoski","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Curtis","family":"Bright","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Albert","family":"Heinle","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ilias","family":"Kotsireas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Krzysztof","family":"Czarnecki","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,12,1]]},"reference":[{"key":"9396_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F.A. Markov, I.L. Sakallah, K.A.: Shatter: efficient symmetry-breaking for boolean satisfiability. In: Proceedings of the 40th Annual Design Automation Conference, pp. 836\u2013839. ACM, (2003)","DOI":"10.1145\/775832.776042"},{"key":"9396_CR2","unstructured":"Areces, C., D\u00e9harbe, D., Pascal, F., Ezequiel, O.: SyMT: finding symmetries in SMT formulas. In: SMT Workshop 2013 11th International Workshop on Satisfiability Modulo Theories, (2013)"},{"key":"9396_CR3","first-page":"399","volume":"9","author":"G Audemard","year":"2009","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. IJCAI 9, 399\u2013404 (2009)","journal-title":"IJCAI"},{"key":"9396_CR4","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification. Lecture Notes in Computer Science","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A.: CVC4. In: Gopalakrishnan, Ganesh, Qadeer, Shaz (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 6806, pp. 171\u2013177. Springer, Berlin (2011)"},{"key":"9396_CR5","doi-asserted-by":"crossref","unstructured":"Bayless, S., Bayless, N., Hoos, H.H., Hu, A.J.: SAT modulo monotonic theories. In: Twenty-Ninth AAAI Conference on Artificial Intelligence, (2015)","DOI":"10.1609\/aaai.v29i1.9755"},{"key":"9396_CR6","doi-asserted-by":"crossref","unstructured":"Benhamou, B., Nabhani, T., Ostrowski, R., Sa\u00efdi, M.R.: Enhancing clause learning by symmetry in SAT solvers. In: 22nd IEEE International Conference on Tools with Artificial Intelligence (ICTAI), 2010, vol.\u00a01, pp. 329\u2013335. IEEE, (2010)","DOI":"10.1109\/ICTAI.2010.55"},{"key":"9396_CR7","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of satisfiability, volume 185 of frontiers in artificial intelligence and applications. IOS Press, (2009)"},{"issue":"3","key":"9396_CR8","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. Symb. Comput. 24(3), 235\u2013265 (1997)","journal-title":"J. Symb. Comput."},{"key":"9396_CR9","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction: CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., de Oliveira, D.C.B., D\u00e9harbe, D.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) Automated Deduction: CADE-22. LNCS, vol. 5663, pp. 151\u2013156. Springer, Berlin (2009)"},{"key":"9396_CR10","doi-asserted-by":"crossref","unstructured":"Bright, C., Ganesh, V., Heinle, A., Kotsireas, l., Nejati, S., Czarnecki, K.: MathCheck2: A SAT+CAS verifier for combinatorial conjectures. In: Computer Algebra in Scientific Computing (to appear). Springer, Berlin (2016)","DOI":"10.1007\/978-3-319-45641-6_9"},{"issue":"2","key":"9396_CR11","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, Michael B.: A tutorial introduction to Maple. J. Symb. Comput. 2(2), 179\u2013200 (1986)","journal-title":"J. Symb. Comput."},{"key":"9396_CR12","unstructured":"Chen, Y.-C., Li, K.-L.: Matchings extend to perfect matchings on hypercube networks. In: Proceedings of the International Multiconference of Engineers and Computer Scientists, vol.\u00a01. Citeseer, (2010)"},{"key":"9396_CR13","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":"9396_CR14","doi-asserted-by":"crossref","unstructured":"Darga, P.T., Sakallah, K.A., Markov, I.L.: Faster symmetry discovery using sparsity of symmetries. In: Proceedings of the 45th Annual Design Automation Conference, pp. 149\u2013154. ACM, (2008)","DOI":"10.1145\/1391469.1391509"},{"key":"9396_CR15","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9396_CR16","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe, D., Fontaine, P., Merz, S., Paleo, B.W.: Exploiting symmetry in SMT problems. In: Automated deduction\u2013CADE-23, pp. 222\u2013236. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22438-6_18"},{"key":"9396_CR17","unstructured":"Devos, S., Norine, M.: Edge-antipodal colorings of cubes. Open Problems Garden (2008)"},{"key":"9396_CR18","doi-asserted-by":"crossref","unstructured":"Dooms, G., Deville, Y., Dupont, P.: CP(Graph): introducing a graph computation domain in constraint programming. In: Principles and Practice of Constraint Programming-CP 2005, pp. 211\u2013225. Springer, Berlin (2005)","DOI":"10.1007\/11564751_18"},{"key":"9396_CR19","doi-asserted-by":"crossref","unstructured":"Downey, R.G., Fellows, M.R.: Fundamentals of parameterized complexity, vol.\u00a04. Springer, London (2013)","DOI":"10.1007\/978-1-4471-5559-1"},{"key":"9396_CR20","unstructured":"Een, N., S\u00f6rensson, N.: MiniSat: a SAT solver with conflict-clause minimization. Sat, 5:8th, (2005)"},{"issue":"10","key":"9396_CR21","doi-asserted-by":"crossref","first-page":"1421","DOI":"10.1016\/j.dam.2012.12.025","volume":"161","author":"T Feder","year":"2013","unstructured":"Feder, T.: Subi, Carlos: On hypercube labellings and antipodal monochromatic paths. Discrete Appl. Math. 161(10), 1421\u20131426 (2013)","journal-title":"Discrete Appl. Math."},{"issue":"6","key":"9396_CR22","doi-asserted-by":"crossref","first-page":"1074","DOI":"10.1016\/j.jctb.2007.02.007","volume":"97","author":"J Fink","year":"2007","unstructured":"Fink, J.: Perfect matchings extend to Hamilton cycles in hypercubes. J. Comb. Theory Ser. B 97(6), 1074\u20131076 (2007)","journal-title":"J. Comb. Theory Ser. B"},{"issue":"2","key":"9396_CR23","doi-asserted-by":"crossref","first-page":"1100","DOI":"10.1137\/070697288","volume":"23","author":"J Fink","year":"2009","unstructured":"Fink, J.: Connectivity of matching graph of hypercube. SIAM J. Discrete Math. 23(2), 1100\u20131109 (2009)","journal-title":"SIAM J. Discrete Math."},{"key":"9396_CR24","doi-asserted-by":"crossref","unstructured":"Frigo, M., Johnson, S.G.: The design and implementation of FFTW3. In: Proceedings of the IEEE, 93(2):216\u2013231, (2005). Special issue on \u201cProgram Generation, Optimization, and Platform Adaptation\u201d","DOI":"10.1109\/JPROC.2004.840301"},{"key":"9396_CR25","doi-asserted-by":"crossref","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Computer Aided Verification, pp. 519\u2013531. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"9396_CR26","doi-asserted-by":"crossref","unstructured":"Ganesh, V., O\u2019donnell, C.W., Soos, M., Devadas, S., Rinard, M.C., Solar-Lezama, A.: Lynx: A programmatic SAT solver for the RNA-folding problem. In: Theory and Applications of Satisfiability Testing\u2013SAT 2012, pp. 143\u2013156. Springer, (2012)","DOI":"10.1007\/978-3-642-31612-8_12"},{"key":"9396_CR27","doi-asserted-by":"crossref","unstructured":"Gebser, M., Janhunen, T., Rintanen, J.: SAT modulo graphs: Acyclicity. In: Logics in Artificial Intelligence, pp. 137\u2013151. Springer, (2014)","DOI":"10.1007\/978-3-319-11558-0_10"},{"key":"9396_CR28","doi-asserted-by":"crossref","unstructured":"Gent, I.P., Petrie, K.E., Puget, J.F.: Symmetry in constraint programming. Handbook of constraint programming, pp. 329\u2013376, (2006)","DOI":"10.1016\/S1574-6526(06)80014-3"},{"key":"9396_CR29","unstructured":"Gent, I., Smith, P.: Symmetry breaking during search in constraint programming. Citeseer, Barbara (1999)"},{"issue":"6","key":"9396_CR30","doi-asserted-by":"crossref","first-page":"1711","DOI":"10.1016\/j.disc.2008.02.013","volume":"309","author":"P Gregor","year":"2009","unstructured":"Gregor, P.: Perfect matchings extending on subcubes to Hamiltonian cycles of hypercubes. Discrete Math. 309(6), 1711\u20131713 (2009)","journal-title":"Discrete Math."},{"issue":"1","key":"9396_CR31","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."},{"issue":"6","key":"9396_CR32","doi-asserted-by":"crossref","first-page":"1184","DOI":"10.1214\/aos\/1176344370","volume":"6","author":"A Hedayat","year":"1978","unstructured":"Hedayat, A., Wallis, W.D.: Hadamard matrices and their applications. Ann. Stat. 6(6), 1184\u20131238 (1978)","journal-title":"Ann. Stat."},{"key":"9396_CR33","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Formal methods in computer-aided design (FMCAD), 2013, pp. 181\u2013188. IEEE, (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"9396_CR34","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. arXiv preprint arXiv:1605.00723 , (2016)","DOI":"10.1007\/978-3-319-40970-2_15"},{"issue":"4","key":"9396_CR35","doi-asserted-by":"crossref","first-page":"723","DOI":"10.1145\/502090.502095","volume":"48","author":"J Holm","year":"2001","unstructured":"Holm, J., de Lichtenberg, K., Thorup, M.: Poly-logarithmic deterministic fully-dynamic algorithms for connectivity, minimum spanning tree, 2-edge, and biconnectivity. J. ACM 48(4), 723\u2013760 (2001)","journal-title":"J. ACM"},{"key":"9396_CR36","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)"},{"key":"9396_CR37","doi-asserted-by":"crossref","unstructured":"Junttila, T., Kaski, P.: Engineering an efficient canonical labeling tool for large and sparse graphs. In: Applegate, D., Brodal, G.S., Panario, D., Sedgewick, R (eds) Proceedings of the Ninth Workshop on Algorithm Engineering and Experiments and the Fourth Workshop on Analytic Algorithms and Combinatorics, pp. 135\u2013149. SIAM, (2007)","DOI":"10.1137\/1.9781611972870.13"},{"key":"9396_CR38","doi-asserted-by":"crossref","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the Erd\u0151s discrepancy conjecture. In: SAT, (2014)","DOI":"10.1007\/978-3-319-09284-3_17"},{"key":"9396_CR39","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"},{"issue":"5","key":"9396_CR40","doi-asserted-by":"crossref","first-page":"658","DOI":"10.1016\/j.ejc.2005.03.004","volume":"27","author":"IS Kotsireas","year":"2006","unstructured":"Kotsireas, I.S., Koukouvinos, C., Seberry, J.: Hadamard ideals and Hadamard matrices with two circulant core. Eur. J. Comb. 27(5), 658\u2013668 (2006)","journal-title":"Eur. J. Comb."},{"issue":"1","key":"9396_CR41","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0012-365X(88)90040-4","volume":"68","author":"C Koukouvinos","year":"1988","unstructured":"Koukouvinos, C., Kounias, S.: Hadamard matrices of the Williamson type of order $$4\\cdot m$$ 4 \u00b7 m , $$m=p\\cdot q$$ m = p \u00b7 q an exhaustive search for $$m=33$$ m = 33 . Discrete Math 68(1), 45\u201357 (1988)","journal-title":"Discrete Math"},{"key":"9396_CR42","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Exponential recency weighted average branching heuristic for SAT solvers. In: Schuurmans, D., Wellman, M.P. (eds), Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12\u201317, 2016, Phoenix, Arizona, USA., pp. 3434\u20133440. AAAI Press, (2016)"},{"key":"9396_CR43","first-page":"1594","volume":"8","author":"V Lifschitz","year":"2008","unstructured":"Lifschitz, V.: What is answer set programming? AAAI 8, 1594\u20131597 (2008)","journal-title":"AAAI"},{"key":"9396_CR44","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: 37th IEEE\/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, Vol. 1, pp. 609\u2013619, (2015)","DOI":"10.1109\/ICSE.2015.77"},{"key":"9396_CR45","doi-asserted-by":"crossref","unstructured":"Muller, D.E.: Application of Boolean algebra to switching circuit design and to error detection. Electronic Computers, Transactions of the IRE Professional Group on Electronic Computers, EC-3(3):6\u201312, (1954)","DOI":"10.1109\/IREPGELC.1954.6499441"},{"key":"9396_CR46","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader F., Voronkov A. (eds.) LPAR, volume 3452 of Lecture Notes in Computer Science, pp. 36\u201350. Springer, (2004)"},{"key":"9396_CR47","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic, vol. 2283. Springer Science & Business Media, (2002)","DOI":"10.1007\/3-540-45949-9"},{"issue":"1","key":"9396_CR48","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0012-365X(93)90495-F","volume":"115","author":"DZ Dokovi\u0107","year":"1993","unstructured":"Dokovi\u0107, D.Z.: Williamson matrices of order 4n for n = 33, 35, 39. Discrete Math. 115(1), 267\u2013271 (1993)","journal-title":"Discrete Math."},{"issue":"2","key":"9396_CR49","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/s10623-013-9862-z","volume":"74","author":"DZ Dokovi\u0107","year":"2015","unstructured":"Dokovi\u0107, D.Z., Kotsireas, I.S.: Compression of periodic complementary sequences and applications. Des. Codes Cryptogr. 74(2), 365\u2013377 (2015)","journal-title":"Des. Codes Cryptogr."},{"issue":"1","key":"9396_CR50","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1002\/sapm1933121311","volume":"12","author":"REAC Paley","year":"1933","unstructured":"Paley, R.E.A.C.: On orthogonal matrices. J. Math. Phys. 12(1), 311\u2013320 (1933)","journal-title":"J. Math. Phys."},{"issue":"4","key":"9396_CR51","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"},{"issue":"1","key":"9396_CR52","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1137\/0406012","volume":"6","author":"F Ruskey","year":"1993","unstructured":"Ruskey, F., Savage, C.: Hamilton cycles that extend transposition matchings in Cayley graphs of $${S}_n$$ S n . SIAM J. Discrete Math. 6(1), 152\u2013166 (1993)","journal-title":"SIAM J. Discrete Math."},{"key":"9396_CR53","first-page":"289","volume":"185","author":"KA Sakallah","year":"2009","unstructured":"Sakallah, K.A.: Symmetry and satisfiability. Handb. Satisf. 185, 289\u2013338 (2009)","journal-title":"Handb. Satisf."},{"key":"9396_CR54","first-page":"141","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. 3, 141\u2013224 (2007)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"9396_CR55","unstructured":"Seberry, J.: Library of Williamson Matrices. http:\/\/www.uow.edu.au\/~jennie\/WILLIAMSON\/williamson.html"},{"key":"9396_CR56","unstructured":"Sloane, N.: Library of Hadamard Matrices. http:\/\/neilsloane.com\/hadamard\/"},{"key":"9396_CR57","doi-asserted-by":"crossref","unstructured":"Soh, T., Le\u00a0Berre, D., Roussel, S., Banbara, M., Tamura, N.: Incremental SAT-based method with native Boolean cardinality handling for the Hamiltonian cycle problem. In Logics in Artificial Intelligence, pp. 684\u2013693. Springer, (2014)","DOI":"10.1007\/978-3-319-11558-0_52"},{"key":"9396_CR58","unstructured":"Stein, W.A., et\u00a0al.: Sage Mathematics Software (Version 6.3), (2010)"},{"issue":"232","key":"9396_CR59","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. Lond. Edinb. Dublin Philos. Magaz. J. Sci. 34(232), 461\u2013475 (1867)","journal-title":"Lond. Edinb. Dublin Philos. Magaz. J. Sci."},{"key":"9396_CR60","unstructured":"The Coq\u00a0development team. The Coq proof assistant reference manual. LogiCal Project, 2004. Version 8.0"},{"key":"9396_CR61","doi-asserted-by":"crossref","unstructured":"Thurley, M.: sharpSAT\u2013counting models with advanced component caching and implicit BCP. In Theory and Applications of Satisfiability Testing\u2013SAT 2006, pp. 424\u2013429. Springer, (2006)","DOI":"10.1007\/11814948_38"},{"key":"9396_CR62","unstructured":"Torlak, E.: A constraint solver for software engineering: finding models and cores of large relational specifications. PhD thesis, Massachusetts Institute of Technology, (2009)"},{"key":"9396_CR63","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Gao, P.: Efficient SAT techniques for absolute encoding of permutation problems: Application to Hamiltonian cycles. In SARA, (2009)","DOI":"10.1007\/978-3-642-10439-8_52"},{"issue":"1","key":"9396_CR64","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":"2","key":"9396_CR65","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1109\/MCSE.2011.37","volume":"13","author":"S St\u00e9fan van der Walt","year":"2011","unstructured":"St\u00e9fan van der Walt, S., Colbert, C., Varoquaux, G.: The NumPy array: a structure for efficient numerical computation. Comput. Sci. Eng. 13(2), 22\u201330 (2011)","journal-title":"Comput. Sci. Eng."},{"key":"9396_CR66","doi-asserted-by":"crossref","unstructured":"Wetzler, N., Heule, M.J.H., Hunt\u00a0Jr, W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In International Conference on Theory and Applications of Satisfiability Testing, pp. 422\u2013429. Springer, (2014)","DOI":"10.1007\/978-3-319-09284-3_31"},{"issue":"1","key":"9396_CR67","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":"9396_CR68","volume-title":"The Mathematica Book, version 4","author":"S Wolfram","year":"1999","unstructured":"Wolfram, S.: The Mathematica Book, version 4. Cambridge University Press, Cambridge (1999)"},{"key":"9396_CR69","unstructured":"Zulkoski, E., Ganesh, V.: SageSAT, (2015) https:\/\/bitbucket.org\/ezulkosk\/sagesat"},{"key":"9396_CR70","doi-asserted-by":"crossref","unstructured":"Zulkoski, E., Ganesh, V., Czarnecki, K.: MathCheck: A math assistant based on a combination of computer algebra systems and SAT solvers. In International Conference on Automated Deduction, Berlin, Germany, 08\/2015. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-21401-6_41"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9396-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9396-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9396-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T23:46:37Z","timestamp":1749771997000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9396-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,1]]},"references-count":70,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["9396"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9396-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,12,1]]}}}