{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T09:15:32Z","timestamp":1766049332385},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T00:00:00Z","timestamp":1586908800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T00:00:00Z","timestamp":1586908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["AAECC"],"published-print":{"date-parts":[[2020,6]]},"DOI":"10.1007\/s00200-020-00426-y","type":"journal-article","created":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T20:02:54Z","timestamp":1586980974000},"page":"195-213","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A nonexistence certificate for projective planes of order ten with weight 15 codewords"],"prefix":"10.1007","volume":"31","author":[{"given":"Curtis","family":"Bright","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kevin","family":"Cheung","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brett","family":"Stevens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"Roy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilias","family":"Kotsireas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,15]]},"reference":[{"key":"426_CR1","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m, 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\u20136. ACM,\u00a0New York, NY, USA (2015)","DOI":"10.1145\/2755996.2756636"},{"key":"426_CR2","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.dam.2014.05.007","volume":"174","author":"T Ahmed","year":"2014","unstructured":"Ahmed, T., Kullmann, O., Snevily, H.: On the van der Waerden numbers $$w(2;3, t)$$. Discret. Appl. Math. 174, 27\u201351 (2014)","journal-title":"Discret. Appl. Math."},{"key":"426_CR3","doi-asserted-by":"crossref","unstructured":"Assmus Jr., E.F., Mattson Jr., H.F.: On the possibility of a projective plane of order 10. Algebraic Theory of Codes II, Air Force Cambridge Research Laboratories Report AFCRL-71-0013, Sylvania Electronic Systems, Needham Heights, Mass (1970)","DOI":"10.21236\/AD0718114"},{"key":"426_CR4","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C., (ed.) IJCAI-09: Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence, pp. 399\u2013404 (2009)"},{"key":"426_CR5","unstructured":"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. Maplesoft, Waterloo, ON, Canada (2019)"},{"key":"426_CR6","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-319-99957-9_4","volume-title":"International Conference on Artificial Intelligence and Symbolic Computation","author":"D Braun","year":"2018","unstructured":"Braun, D., Magaud, N., Schreck, P.: Formalizing some small\u201d finite models of projective geometry in Coq. In: Fleuriot, J., Wang, D., Calmet, J. (eds.) International Conference on Artificial Intelligence and Symbolic Computation, pp. 54\u201369. Springer, Berlin (2018)"},{"key":"426_CR7","doi-asserted-by":"crossref","unstructured":"Bright, C., \u0110okovi\u0107, D., Kotsireas, I., Ganesh, V.: A SAT+CAS approach to finding good matrices: New examples and counterexamples. In: Van Hentenryck, P., Zhou, Z.H., (eds.) Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-19), pp. 1435\u20131442. AAAI Press, Cambridge (2019)","DOI":"10.1609\/aaai.v33i01.33011435"},{"key":"426_CR8","doi-asserted-by":"crossref","unstructured":"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.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18), pp. 6573\u20136580. AAAI Press, Cambridge (2018)","DOI":"10.1609\/aaai.v32i1.12203"},{"key":"426_CR9","unstructured":"Bright, C., Kotsireas, I., Ganesh, V.: SAT solvers and computer algebra systems: A powerful combination for mathematics. In: Pakfetrat, T., Jourdan, G., Kontogiannis, K., Enenkel, R., (eds.) Proceedings of the 29th International Conference on Computer Science and Software Engineering, pp. 323\u2013328. IBM Corp.,\u00a0Riverton, NJ, USA (2019)"},{"key":"426_CR10","doi-asserted-by":"crossref","unstructured":"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 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201918, pp. 111\u2013118. New York, NY, USA (2018)","DOI":"10.1145\/3208976.3209006"},{"issue":"191","key":"426_CR11","first-page":"9","volume":"1","author":"RH Bruck","year":"1949","unstructured":"Bruck, R.H., Ryser, H.J.: The nonexistence of certain finite projective planes. Can. J. Math 1(191), 9 (1949)","journal-title":"Can. J. Math"},{"issue":"2","key":"426_CR12","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0001-8708(73)90114-X","volume":"10","author":"A Bruen","year":"1973","unstructured":"Bruen, A., Fisher, J.C.: Blocking sets, $$k$$-arcs and nets of order ten. Adv. Math. 10(2), 317\u2013320 (1973)","journal-title":"Adv. Math."},{"issue":"1","key":"426_CR13","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/0097-3165(71)90005-7","volume":"11","author":"KA Bush","year":"1971","unstructured":"Bush, K.A.: Unbalanced Hadamard matrices and finite projective planes of even order. J. Combin. Theory Ser. A 11(1), 38\u201344 (1971)","journal-title":"J. Combin. Theory Ser. A"},{"key":"426_CR14","volume-title":"On the existence of a projective plane of order ten","author":"JL Carter","year":"1974","unstructured":"Carter, J.L.: On the existence of a projective plane of order ten. University of California, Berkeley (1974)"},{"key":"426_CR15","first-page":"69","volume":"57","author":"D Casiello","year":"2010","unstructured":"Casiello, D., Indaco, L., Nagy, G.P.: Sull\u2019approccio computazionale al problema dell\u2019esistenza di un piano proiettivo d\u2019ordine 10. Atti del Seminario matematico e fisico dell\u2019Universit\u00e0 di Modena e Reggio Emilia 57, 69\u201388 (2010)","journal-title":"Atti del Seminario matematico e fisico dell\u2019Universit\u00e0 di Modena e Reggio Emilia"},{"key":"426_CR16","unstructured":"Clarkson, K., Whitesides, S.: On the non-existence of maximal 6-arcs in projective planes of order 10. In: Poster session at IWOCA 2014, the 25th International Workshop on Combinatorial Algorithms (2014)"},{"issue":"3","key":"426_CR17","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/s10601-016-9240-3","volume":"21","author":"M Codish","year":"2016","unstructured":"Codish, M., Frank, M., Itzhakov, A., Miller, A.: Computing the Ramsey number $$R(4,3,3)$$ using abstraction and symmetry breaking. Constraints 21(3), 375\u2013393 (2016)","journal-title":"Constraints"},{"key":"426_CR18","unstructured":"Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: Aiello, L.C., Doyle, J., Shapiro, S.C., (eds.) Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning, KR\u201996, pp. 148\u2013159. Morgan Kaufmann Publishers Inc., San Francisco (1996)"},{"key":"426_CR19","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/s10817-018-9490-4","volume":"63","author":"L Cruz-Filipe","year":"2018","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Formally verifying the solution to the Boolean Pythagorean triples problem. J. Autom. Reason. 63, 695\u2013792 (2018)","journal-title":"J. Autom. Reason."},{"key":"426_CR20","doi-asserted-by":"crossref","unstructured":"Davenport, J.H., England, M., Griggio, A., Sturm, T., Tinelli, C.: Symbolic computation and satisfiability checking. J. Symb. Comput. 100, 1\u201310\u00a0(2020)","DOI":"10.1016\/j.jsc.2019.07.017"},{"issue":"1\u20132","key":"426_CR21","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1017\/S1446788700007096","volume":"10","author":"RHF Denniston","year":"1969","unstructured":"Denniston, R.H.F.: Non-existence of a certain projective plane. J. Austral. Math. Soc. 10(1\u20132), 214\u2013218 (1969)","journal-title":"J. Austral. Math. Soc."},{"key":"426_CR22","first-page":"143","volume-title":"International Conference on Theory and Applications of Satisfiability Testing","author":"V Ganesh","year":"2012","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: Cimatti, A., Sebastiani, R. (eds.) International Conference on Theory and Applications of Satisfiability Testing, pp. 143\u2013156. Springer, Berlin (2012)"},{"key":"426_CR23","unstructured":"The GAP Group: GAP \u2013 Groups, Algorithms, and Programming, Version 4.10.2 (2019). https:\/\/www.gap-system.org"},{"key":"426_CR24","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/S0167-5060(08)70701-5","volume":"6","author":"M Hall Jr","year":"1980","unstructured":"Hall Jr., M.: Configurations in a plane of order ten. Ann. Discret. Math. 6, 157\u2013174 (1980)","journal-title":"Ann. Discret. Math."},{"key":"426_CR25","unstructured":"Heule, M.J.H.: Cube-and-conquer tutorial (2018). https:\/\/github.com\/marijnheule\/CnC"},{"key":"426_CR26","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H.: Schur number five. In: McIlraith, S.A., Weinberger, K.Q., (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18), pp. 6598\u20136606. AAAI Press, Cambridge (2018)","DOI":"10.1609\/aaai.v32i1.12209"},{"key":"426_CR27","unstructured":"Heule, M.J.H., Kauers, M., Seidl, M.: New ways to multiply $$3\\times 3$$-matrices. (2019) arXiv:1905.10192"},{"key":"426_CR28","first-page":"228","volume-title":"International Conference on Theory and Applications of Satisfiability Testing","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) International Conference on Theory and Applications of Satisfiability Testing, pp. 228\u2013245. Springer, Berlin (2016)"},{"key":"426_CR29","doi-asserted-by":"crossref","unstructured":"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\u20134868 (2017)","DOI":"10.24963\/ijcai.2017\/683"},{"key":"426_CR30","first-page":"50","volume-title":"Haifa Verification Conference","author":"MJH Heule","year":"2011","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) Haifa Verification Conference, pp. 50\u201365. Springer, Berlin (2011)"},{"key":"426_CR31","unstructured":"K\u00e5hrstr\u00f6m, J.: On projective planes. Techn. Rep. (2002).\u00a0http:\/\/kahrstrom.com\/mathematics\/documents\/OnProjectivePlanes.pdf"},{"key":"426_CR32","doi-asserted-by":"crossref","unstructured":"Kaufmann, D., Biere, A., Kauers, M.: Verifying large multipliers by combining SAT and computer algebra. In: Proceedings of Formal Methods in Computer-Aided Design (2020)","DOI":"10.23919\/FMCAD.2019.8894250"},{"key":"426_CR33","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-030-28483-1_4","volume-title":"Proof Technology in Mathematics Research and Teaching","author":"C Keller","year":"2019","unstructured":"Keller, C.: SMTCoq: mixing automatic and interactive proof technologies. In: Hanna, G., Reid, D.A., de Villiers, M. (eds.) Proof Technology in Mathematics Research and Teaching, pp. 73\u201390. Springer International Publishing, Cham (2019)"},{"key":"426_CR34","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.artint.2015.03.004","volume":"224","author":"B Konev","year":"2015","unstructured":"Konev, B., Lisitsa, A.: Computer-aided proof of Erd\u0151s discrepancy properties. Artif. Intell. 224, 103\u2013118 (2015)","journal-title":"Artif. Intell."},{"issue":"1","key":"426_CR35","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1080\/10586458.2008.10129025","volume":"17","author":"M Kouril","year":"2008","unstructured":"Kouril, M., Paul, J.L.: The van der Waerden number $$W(2,6)$$ is 1132. Exp. Math. 17(1), 53\u201361 (2008)","journal-title":"Exp. Math."},{"key":"426_CR36","first-page":"352","volume-title":"International Conference on Theory and Applications of Satisfiability Testing","author":"O Kullmann","year":"2010","unstructured":"Kullmann, O.: Green-Tao numbers and SAT. In: Strichman, O., Szeider, S. (eds.) International Conference on Theory and Applications of Satisfiability Testing, pp. 352\u2013362. Springer, Berlin (2010)"},{"issue":"4","key":"426_CR37","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1080\/00029890.1991.12000759","volume":"98","author":"CWH Lam","year":"1991","unstructured":"Lam, C.W.H.: The search for a finite projective plane of order $$10$$. Am. Math. Month. 98(4), 305\u2013318 (1991)","journal-title":"Am. Math. Month."},{"issue":"2","key":"426_CR38","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/0097-3165(86)90091-9","volume":"42","author":"CWH Lam","year":"1986","unstructured":"Lam, C.W.H., Thiel, L., Swiercz, S.: The nonexistence of code words of weight 16 in a projective plane of order 10. J. Combin. Theory Ser. A 42(2), 207\u2013214 (1986)","journal-title":"J. Combin. Theory Ser. A"},{"issue":"6","key":"426_CR39","doi-asserted-by":"publisher","first-page":"1117","DOI":"10.4153\/CJM-1989-049-4","volume":"41","author":"CWH Lam","year":"1989","unstructured":"Lam, C.W.H., Thiel, L., Swiercz, S.: The non-existence of finite projective planes of order 10. Canad. J. Math 41(6), 1117\u20131123 (1989)","journal-title":"Canad. J. Math"},{"issue":"2\u20133","key":"426_CR40","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0012-365X(83)90049-3","volume":"45","author":"CWH Lam","year":"1983","unstructured":"Lam, C.W.H., Thiel, L., Swiercz, S., McKay, J.: The nonexistence of ovals in a projective plane of order 10. Discret. Math. 45(2\u20133), 319\u2013321 (1983)","journal-title":"Discret. Math."},{"key":"426_CR41","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D., (eds.) Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5\u20138, 2016, Proceedings, pp. 123\u2013140 (2016). https:\/\/ece.uwaterloo.ca\/maplesat\/"},{"issue":"1","key":"426_CR42","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1016\/0097-3165(73)90064-2","volume":"14","author":"FJ MacWilliams","year":"1973","unstructured":"MacWilliams, F.J., Sloane, N.J.A., Thompson, J.G.: On the existence of a projective plane of order 10. J. Combin. Theory Ser. A 14(1), 66\u201378 (1973)","journal-title":"J. Combin. Theory Ser. A"},{"key":"426_CR43","first-page":"141","volume-title":"International Workshop on Automated Deduction in Geometry","author":"N Magaud","year":"2008","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing projective plane geometry in Coq. In: Sturm, T., Zengler, C. (eds.) International Workshop on Automated Deduction in Geometry, pp. 141\u2013162. Springer, Berlin (2008)"},{"key":"426_CR44","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1016\/j.jsc.2013.09.003","volume":"60","author":"BD McKay","year":"2014","unstructured":"McKay, B.D., Piperno, A.: Practical graph isomorphism, II. J. Symb. Comput. 60, 94\u2013112 (2014)","journal-title":"J. Symb. Comput."},{"key":"426_CR45","first-page":"242","volume-title":"International Conference on Theory and Applications of Satisfiability Testing","author":"A Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) International Conference on Theory and Applications of Satisfiability Testing, pp. 242\u2013255. Springer, Berlin (2012)"},{"key":"426_CR46","unstructured":"Perrott, X.: Existence of projective planes. arXiv:1603.05333 (2016)"},{"key":"426_CR47","unstructured":"Roy, D.J.: Proving $$w_{15}=0$$ in a hypothetical projective plane of order 10. Course Project for CSI 5165, University of Ottawa (2005)"},{"key":"426_CR48","unstructured":"Roy, D.J.: Confirmation of the non-existence of a projective plane of order 10. Master\u2019s thesis, Carleton University (2011)"},{"key":"426_CR49","first-page":"827","volume-title":"International Conference on Principles and Practice of Constraint Programming","author":"C Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) International Conference on Principles and Practice of Constraint Programming, pp. 827\u2013831. Springer, Berlin (2005)"},{"key":"426_CR50","first-page":"422","volume-title":"International Conference on Theory and Applications of Satisfiability Testing","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) International Conference on Theory and Applications of Satisfiability Testing, pp. 422\u2013429. Springer, Berlin (2014)"},{"key":"426_CR51","unstructured":"Wolfram Research, Inc.: Mathematica, Version 12.0. Wolfram Research, Inc., Champaign, IL (2019)"},{"issue":"3","key":"426_CR52","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s10817-016-9396-y","volume":"58","author":"E Zulkoski","year":"2017","unstructured":"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\u2013339 (2017)","journal-title":"J. Autom. Reason."},{"key":"426_CR53","first-page":"607","volume-title":"International Conference on Automated Deduction","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, A.P., Middeldorp, A. (eds.) International Conference on Automated Deduction, pp. 607\u2013622. Springer, Cham (2015)"}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00200-020-00426-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00200-020-00426-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00200-020-00426-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,21]],"date-time":"2022-10-21T11:40:38Z","timestamp":1666352438000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00200-020-00426-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4,15]]},"references-count":53,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["426"],"URL":"https:\/\/doi.org\/10.1007\/s00200-020-00426-y","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,4,15]]},"assertion":[{"value":"30 October 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 March 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 April 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}