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