# zbMATH — the first resource for mathematics

A nonexistence certificate for projective planes of order ten with weight 15 codewords. (English) Zbl 1460.68098
Summary: Using techniques from the fields of symbolic computation and satisfiability checking we verify one of the cases used in the landmark result that projective planes of order ten do not exist. In particular, we show that there exist no projective planes of order ten that generate codewords of weight fifteen, a result first shown in 1973 via an exhaustive computer search. We provide a simple satisfiability (SAT) instance and a certificate of unsatisfiability that can be used to automatically verify this result for the first time. All previous demonstrations of this result have relied on search programs that are difficult or impossible to verify – in fact, our search found partial projective planes that were missed by previous searches due to previously undiscovered bugs. Furthermore, we show how the performance of the SAT solver can be dramatically increased by employing functionality from a computer algebra system (CAS). Our SAT+CAS search runs significantly faster than all other published searches verifying this result.
##### MSC:
 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) 05B25 Combinatorial aspects of finite geometries 51E20 Combinatorial structures in finite projective spaces 68W30 Symbolic computation and algebraic computation
##### Software:
GAP; SMTCoq; Maple; Lynx; nauty; Traces; Mathematica; MathCheck; CnC; tawSolver; GitHub; DRAT-trim
Full Text:
##### 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, New York, NY, USA (2015) · Zbl 1345.68279 [2] 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 [3] 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) [4] 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-404 (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. Maplesoft, Waterloo, ON, Canada (2019) [6] Braun, D.; Magaud, N.; Schreck, P.; Fleuriot, J.; Wang, D.; Calmet, J., Formalizing some small” finite models of projective geometry in Coq, International Conference on Artificial Intelligence and Symbolic Computation, 54-69 (2018), Berlin: Springer, Berlin [7] Bright, C., Đoković, 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-1442. AAAI Press, Cambridge (2019) [8] 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-6580. AAAI Press, Cambridge (2018) [9] 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-328. IBM Corp., Riverton, NJ, USA (2019) [10] 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 ’18, pp. 111-118. New York, NY, USA (2018) [11] Bruck, RH; Ryser, HJ, The nonexistence of certain finite projective planes, Can. J. Math, 1, 191, 9 (1949) [12] Bruen, A.; Fisher, JC, Blocking sets, $$k$$-arcs and nets of order ten, Adv. Math., 10, 2, 317-320 (1973) · Zbl 0258.50021 [13] Bush, KA, Unbalanced Hadamard matrices and finite projective planes of even order, J. Combin. Theory Ser. A, 11, 1, 38-44 (1971) · Zbl 0172.01503 [14] Carter, JL, On the existence of a projective plane of order ten (1974), Berkeley: University of California, Berkeley [15] Casiello, D.; Indaco, L.; Nagy, GP, Sull’approccio computazionale al problema dell’esistenza di un piano proiettivo d’ordine 10, Atti del Seminario matematico e fisico dell’Università di Modena e Reggio Emilia, 57, 69-88 (2010) [16] 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) [17] 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-393 (2016) · Zbl 1368.05046 [18] 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’96, pp. 148-159. Morgan Kaufmann Publishers Inc., San Francisco (1996) [19] Cruz-Filipe, L.; Marques-Silva, J.; Schneider-Kamp, P., Formally verifying the solution to the Boolean Pythagorean triples problem, J. Autom. Reason., 63, 695-792 (2018) · Zbl 07100460 [20] Davenport, J.H., England, M., Griggio, A., Sturm, T., Tinelli, C.: Symbolic computation and satisfiability checking. J. Symb. Comput. 100, 1-10 (2020) · Zbl 1444.68006 [21] Denniston, RHF, Non-existence of a certain projective plane, J. Austral. Math. Soc., 10, 1-2, 214-218 (1969) · Zbl 0175.47701 [22] Ganesh, V.; O’Donnell, CW; Soos, M.; Devadas, S.; Rinard, MC; Solar-Lezama, A.; Cimatti, A.; Sebastiani, R., Lynx: a programmatic SAT solver for the RNA-folding problem, International Conference on Theory and Applications of Satisfiability Testing, 143-156 (2012), Berlin: Springer, Berlin [23] The GAP Group: GAP - Groups, Algorithms, and Programming, Version 4.10.2 (2019). https://www.gap-system.org [24] Hall, M. Jr, Configurations in a plane of order ten, Ann. Discret. Math., 6, 157-174 (1980) · Zbl 0463.05021 [25] Heule, M.J.H.: Cube-and-conquer tutorial (2018). https://github.com/marijnheule/CnC [26] 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-6606. AAAI Press, Cambridge (2018) [27] Heule, M.J.H., Kauers, M., Seidl, M.: New ways to multiply $$3\times 3$$-matrices. (2019) arXiv:1905.10192 [28] Heule, MJH; Kullmann, O.; Marek, VW; Creignou, N.; Le Berre, D., Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer, International Conference on Theory and Applications of Satisfiability Testing, 228-245 (2016), Berlin: Springer, Berlin · Zbl 1403.68226 [29] 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) [30] Heule, MJH; Kullmann, O.; Wieringa, S.; Biere, A.; Eder, K.; Lourenço, J.; Shehory, O., Cube and conquer: guiding CDCL SAT solvers by lookaheads, Haifa Verification Conference, 50-65 (2011), Berlin: Springer, Berlin [31] Kåhrström, J.: On projective planes. Techn. Rep. (2002). http://kahrstrom.com/mathematics/documents/OnProjectivePlanes.pdf [32] 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) [33] Keller, C.; Hanna, G.; Reid, DA; de Villiers, M., SMTCoq: mixing automatic and interactive proof technologies, Proof Technology in Mathematics Research and Teaching, 73-90 (2019), Cham: Springer International Publishing, Cham [34] Konev, B.; Lisitsa, A., Computer-aided proof of Erdős discrepancy properties, Artif. Intell., 224, 103-118 (2015) · Zbl 1344.68205 [35] Kouril, M.; Paul, JL, The van der Waerden number $$W(2,6)$$ is 1132, Exp. Math., 17, 1, 53-61 (2008) · Zbl 1151.05048 [36] Kullmann, O.; Strichman, O.; Szeider, S., Green-Tao numbers and SAT, International Conference on Theory and Applications of Satisfiability Testing, 352-362 (2010), Berlin: Springer, Berlin · Zbl 1259.68182 [37] Lam, CWH, The search for a finite projective plane of order $$10$$, Am. Math. Month., 98, 4, 305-318 (1991) · Zbl 0744.51011 [38] Lam, CWH; 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-214 (1986) · Zbl 0591.51015 [39] Lam, CWH; Thiel, L.; Swiercz, S., The non-existence of finite projective planes of order 10, Canad. J. Math, 41, 6, 1117-1123 (1989) · Zbl 0691.51003 [40] Lam, CWH; Thiel, L.; Swiercz, S.; McKay, J., The nonexistence of ovals in a projective plane of order 10, Discret. Math., 45, 2-3, 319-321 (1983) · Zbl 0511.05020 [41] 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-8, 2016, Proceedings, pp. 123-140 (2016). https://ece.uwaterloo.ca/maplesat/ · Zbl 06623509 [42] MacWilliams, FJ; Sloane, NJA; Thompson, JG, On the existence of a projective plane of order 10, J. Combin. Theory Ser. A, 14, 1, 66-78 (1973) · Zbl 0251.05020 [43] Magaud, N.; Narboux, J.; Schreck, P.; Sturm, T.; Zengler, C., Formalizing projective plane geometry in Coq, International Workshop on Automated Deduction in Geometry, 141-162 (2008), Berlin: Springer, Berlin · Zbl 1302.68246 [44] McKay, BD; Piperno, A., Practical graph isomorphism, II, J. Symb. Comput., 60, 94-112 (2014) · Zbl 1394.05079 [45] Nadel, A.; Ryvchin, V.; Cimatti, A.; Sebastiani, R., Efficient SAT solving under assumptions, International Conference on Theory and Applications of Satisfiability Testing, 242-255 (2012), Berlin: Springer, Berlin · Zbl 1273.68358 [46] Perrott, X.: Existence of projective planes. arXiv:1603.05333 (2016) [47] Roy, D.J.: Proving $$w_{15}=0$$ in a hypothetical projective plane of order 10. Course Project for CSI 5165, University of Ottawa (2005) [48] Roy, D.J.: Confirmation of the non-existence of a projective plane of order 10. Master’s thesis, Carleton University (2011) [49] Sinz, C.; van Beek, P., Towards an optimal CNF encoding of boolean cardinality constraints, International Conference on Principles and Practice of Constraint Programming, 827-831 (2005), Berlin: Springer, Berlin · Zbl 1153.68488 [50] Wetzler, N.; Heule, MJH; Hunt, WA; Sinz, C.; Egly, U., DRAT-trim: efficient checking and trimming using expressive clausal proofs, International Conference on Theory and Applications of Satisfiability Testing, 422-429 (2014), Berlin: Springer, Berlin · Zbl 1423.68475 [51] Wolfram Research, Inc.: Mathematica, Version 12.0. Wolfram Research, Inc., Champaign, IL (2019) [52] 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 [53] Zulkoski, E.; Ganesh, V.; Czarnecki, K.; Felty, AP; Middeldorp, A., MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers, International Conference on Automated Deduction, 607-622 (2015), Cham: Springer, 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. 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.