In 1974, Larry Carter showed that up to isomorphism there are ten possible cases for the first eight rows of a projective plane of order ten containing a weight 16 codeword. Carter's decomposition was derived by noting that the incidence matrix of such a plane can be associated with a 3-regular graph on the vertices {1,...,8} (by connecting vertices i and j when rows i and j intersect outside the first 16 columns). Furthermore, up to isomorphism there are exactly six 3-regular graphs on 8 vertices (PDF).
In 2020, we used MathCheck to verify that none of these cases can be extended to a complete projective plane of order ten. Furthermore, we generated DRAT certificates proving this through a reduction of the problem to SAT—see our IJCAI 2020 paper for more details. The following table summarizes the time it took to solve each SAT instance and the size of the certificates after compressed with DRAT-trim:
| Case Name | Solve Time | Proof Size |
|---|---|---|
| Case 1a | 2.61 hours | 20.0 GiB |
| Case 1b | 2.58 hours | 25.3 GiB |
| Case 1c | 13.98 hours | 177.7 GiB |
| Case 2 | 1.82 hours | 6.6 GiB |
| Case 3 | 1.39 hours | 13.3 GiB |
| Case 4 | 0.03 hours | 0.3 GiB |
| Case 5 | 0.42 hours | 3.0 GiB |
| Case 6a | 0.53 hours | 4.7 GiB |
| Case 6b | 2.21 hours | 26.9 GiB |
| Case 6c | 3.26 hours | 48.4 GiB |
This remainder of this page contains figures showing the starting incidence matrices in each case. In these figures black squares represent ones, white squares represent zeros, and gray squares represent unknown entries.
Case 1
Carter called this the "tetrahedrons" case. There are three ways of completing the entries in the first eight rows, resulting in subcases 1a–c. In cases 1b and 1c the columns of certain submatrices are lexicographically ordered. This is justified by examining the incidence pattern that must appear in those submatrices and the fact that without loss of generality we can fix an ordering on those columns.
 |
 |
 |
Case 2
Carter called this the "cube" case. There is a single way of completing the entries in the first eight rows.
 |
Case 3
Carter called this the "octagon" case. There is a single way of completing the entries in the first eight rows.
 |
Case 4
Carter called this the "scales" case. There is a single way of completing the entries in the first eight rows.
 |
Case 5
Carter called this the "top" case. There is a single way of completing the entries in the first eight rows.
 |
Case 6
Carter called this the "tent" case. There are three ways of completing the entries in the first eight rows, resulting in subcases 6a–c. In cases 6b and 6c the columns of certain submatrices (not necessarily using consecutive rows) are lexicographically ordered. This is justified by examining the incidence pattern that must appear in those submatrices and the fact that without loss of generality we can fix an ordering on those columns.
 |
 |
 |