We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.DM

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Discrete Mathematics

Title: A Nonexistence Certificate for Projective Planes of Order Ten with Weight 15 Codewords

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.
Subjects: Discrete Mathematics (cs.DM); Logic in Computer Science (cs.LO); Symbolic Computation (cs.SC); Combinatorics (math.CO)
Cite as: arXiv:1911.04032 [cs.DM]
  (or arXiv:1911.04032v1 [cs.DM] for this version)

Submission history

From: Curtis Bright [view email]
[v1] Mon, 11 Nov 2019 01:48:58 GMT (22kb,D)

Link back to: arXiv, form interface, contact.