A nonexistence certificate for projective planes of order ten with weight 15 codewords

DOI10.1007/S00200-020-00426-YzbMATH Open1460.68098arXiv1911.04032OpenAlexW3017080342MaRDI QIDQ780361FDOQ780361

Authors: Curtis Bright, Brett Stevens, Dominique Roy, Ilias S. Kotsireas, Vijay Ganesh, Kevin K. H. Cheung 

Publication date: 15 July 2020

Published in: Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1911.04032

Recommendations

• scientific article; zbMATH DE number 4096245
• On a computational approach to the existence problem of a projective plane of order 10
• The Non-Existence of Finite Projective Planes of Order 10
• Publication:3029691
• The Search for a Finite Projective Plane of Order 10

zbMATH Keywords

projective planessymbolic computationsatisfiability checkingcombinatorial searchSAT+CAS

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Symbolic computation and algebraic computation (68W30) Combinatorial aspects of finite geometries (05B25) Combinatorial structures in finite projective spaces (51E20)

Cites Work

• Practical graph isomorphism. II.
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
• Computing the Ramsey number \(R(4,3,3)\) using abstraction and symmetry breaking
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Computer-aided proof of Erdős discrepancy properties
• The van der Waerden NumberW(2, 6) Is 1132
• On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
• Green-Tao Numbers and SAT
• The Nonexistence of Certain Finite Projective Planes
• Formalizing projective plane geometry in Coq
• The Non-Existence of Finite Projective Planes of Order 10
• The Search for a Finite Projective Plane of Order 10
• On a computational approach to the existence problem of a projective plane of order 10
• The nonexistence of code words of weight 16 in a projective plane of order 10
• Editorial: Symbolic computation and satisfiability checking
• Formally verifying the solution to the Boolean Pythagorean triples problem
• Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
• Unbalanced Hadamard matrices and finite projective planes of even order
• On the existence of a projective plane of order 10
• Blocking sets, k-arcs and nets of order ten
• Learning rate based branching heuristic for SAT solvers
• Building bridges between symbolic computation and satisfiability checking
• Efficient SAT solving under assumptions
• Configurations in a Plane of Order Ten
• Enumeration of complex Golay pairs via programmatic SAT
• Non-existence of a certain projective plane
• The nonexistence of ovals in a projective plane of order 10
• Formalizing Some “Small” Finite Models of Projective Geometry in Coq

Cited In (2)

• Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
• The nonexistence of code words of weight 16 in a projective plane of order 10

Uses Software

• GAP
• Maple
• Mathematica
• nauty
• Traces
• tawSolver
• DRAT-trim
• MathCheck
• Lynx
• SMTCoq
• CnC
• GitHub

This page was built for publication: A nonexistence certificate for projective planes of order ten with weight 15 codewords

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q780361)