In this paper we describe a method of enumerating projective planes of order nine. The enumeration was previously completed by Lam, Kolesova, and Thiel using highly optimized and customized search code. Despite the importance of this result in the classification of projective geometries, the previous search relied on unverified code and has never been independently verified. Our enumeration procedure-which is still a work in progress-uses a hybrid satisfiability (SAT) solving and symbolic computation approach. SAT solving performs an enumerative search, while symbolic computation removes symmetries from the search space. Certificates are produced which demonstrate the enumeration completed successfully.
verification [
Crucially, our work does not rely on trusting the output of either the SAT solver or the
computer algebra system (CAS). Both tools produce certificates that can be used to verify
the output without taking their claims on faith. Although this is a work in progress, we are
confident that our approach will successfully complete a classification of projective planes of
order nine without requiring the trust of any search code. This is particularly important in
computational classification which requires the generation of a complete list of all instances of
a given object—it is in general quite dificult to prove that the list is complete. Moreover, it is not
feasible to prove that a complicated algorithm (like a search procedure) generates correct results
in all cases [
The objects we will be interested in this paper are primarily finite projective planes, which we introduce here. These projective planes have a few diferent representations, the first of which is perhaps the easiest to understand. After giving this as the definition, we discuss another representation which will be more useful for the purpose of doing an exhaustive computer search for these objects. Also playing a role in this work is the notion of a latin square which we define here. Lastly, we describe the notion of a Boolean satisfiability problem or SAT problem.
To start, we define a projective plane of a given order : Definition 1. A projective plane of order is a collection of 2 + + 1 lines and 2 + + 1 points such that: (1) every line contains + 1 points, (2) every point is on + 1 lines, (3) any two distinct lines intersect at exactly one point, and (4) any two distinct points lie on exactly one line.
From this definition, we can see that projective planes are objects which have a natural
interpretation as an incidence structure—that is, two disjoint sets equipped with a relation
between them which we call the incidence relation [
Then we may represent the associated bipartite graph as an (2 + + 1) × (2 + + 1) binary incidence matrix, in which each row represents a point and each column represents a line. The (, )th entry of this matrix will be 1 if the point lies on the line ℓ , and it will be 0 otherwise. This definition is more workable for the purpose of using a SAT solver as we can encode the incidence matrix as (2 + + 1)2 Boolean variables. To be able to utilize this representation, we must also translate the axioms of the projective plane (1)–(4) given above in terms of the incidence matrix. Two binary vectors are said to intersect if they both contain 1s in the same entry of the vector (or rather, their inner product is greater than 0). One can check that an (2 + + 1) × (2 + + 1) incidence matrix is one which arises from a projective plane of order if the following properties are satisfied: (1) each column sum of the matrix is + 1, (2) each row sum of the matrix is + 1, (3) two distinct columns of the matrix intersect exactly once, and (4) two distinct rows of the matrix intersect exactly once.
Definition 2. that: 1. each row contains each of the numbers 1, 2, . . . , exactly once, and 2. each column contains each of the numbers 1, 2, . . . , exactly once.
A × latin square is a × array consisting of the integers 1, 2, . . . , such ⎡ 1 2 3 4 ⎤ ⎢ 2 3 4 1 ⎥ ⎢⎣ 3 4 1 2 ⎦⎥
4 1 2 3 The role that latin squares play in our search for projective planes will become more clear after our discussion in section 2.2.
Lastly, we describe SAT problems—which are useful because heuristic algorithms exist that
often solve SAT instances extremely eficiently. A literal is a Boolean variable or a negated
Boolean variable, and a clause is a disjunction of literals. Given a list of clauses, we say the
list is satisfiable if we can assign true and false values to its variables such that every clause
evaluates to be true. A SAT problem is the problem of determining if a given list of clauses is
satisfiable or not. This problem is known to be NP-complete and there is no known polynomial
time algorithm solving it. However, there are good heuristic SAT solvers like MapleSAT [
With this background established, we now give more details about the problem we’re interested in. As we discussed, we can represent a hypothetical projective plane of order as an (2 + + 1) × (2 + + 1) incidence matrix satisfying certain properties. For the order 9 case, we’re interested in enumerating the 91 × 91 incidence matrices (note: 91 = 92 + 9 + 1) satisfying certain properties up to a certain symmetry. We now comment on what this symmetry is.
Notice that given a fixed projective plane of order 9, one can obtain a distinct, but similar, projective plane by relabelling some of the points, and relabelling some of the lines. Realistically however, these “new” planes are the same as the original one, thus we wish to ignore these extra planes in our search if possible. These relabellings correspond to column and row permutations of the incidence matrix. Consequently, we can give a group theoretic interpretation of this: Let be the group 91 × 91. We may view the first component of this group as the row permutations, and the second as the column permutations. In this way, we have a group action of on the set of incidence matrices corresponding to projective planes. Then we can say that two planes are equivalent if they are in the same orbit under this action. Two planes are in the same orbit, if one can be obtained from the other via action of the group , or rather, by applying column and row permutations.
Searching for only a representative of each orbit makes our search drastically more feasible.
This computational search was first done by Lam, Kolesova, and Thiel [
Here we detail the structure we impose on the incidence matrix of our hypothetical projective plane for the purpose of reducing the search space of our problem. The first important thing to note is that a hypothetical projective plane must contain a triangle—that is, a set of three non-collinear points. We may suppose that the first three points 1, 2, and 3 form this triangle, and furthermore that ℓ1 is the unique line joining 2 and 3, ℓ2 is the unique line joining 1 and 2, and lastly that ℓ3 is the unique line joining 1 and 3. We may impose this order simply by applying the needed row and column permutations to the incidence matrix. With this ordering 1 2 3 4 5 6 7 8 of the points and lines, the upper left 3 × 3 sub-matrix of the incidence matrix will look like:
Once this is done, we know by the first two axioms of a projective plane, that there should be 8 more 1’s in each of the first three rows and columns. By applying further row and column permutations, we may impose a staircase like structure on these entries. For example, we can make the first three rows in columns 4 to 27 will look like: with the entries in columns 28 and above being 0 in those rows.
Then, using further column and row permutations, we may fix many of the entries in the ifrst 27 columns of the incidence matrix shown in Figure 2. The entries in the submatrix formed by columns 20–27 and rows 28–91 will not be fixed but they do have a nice structure.
One can check that the 8 × 8 blocks 1, 2, . . . , 8 given in Figure 2 will be 8 × 8 permutation matrices. Consequently, these blocks correspond to permutations 1, 2, . . . , 8 ∈ 8. Furthermore, we know that we can’t have () = () where ̸= since otherwise we would have two distinct rows intersecting twice. This property ensures that we may encode this set of 8 permutations as an 8 × 8 latin square. A more detailed explanation of this normalized form for the partial plane can be found in Kolesova’s thesis [11, Prop. 4.1].
Thus, for a given 8 × 8 latin square, we may obtain the 27 columns of a partial projective plane, and in this way, all such partial planes may be obtained if all 8 × 8 latin squares can be enumerated. Thus, our approach for generating the projective planes of order 9 will begin by generating the latin squares of order 8. However, two distinct latin squares can give equivalent partial planes. Thus we will be interested in equivalence classes of latin squares as detailed in the next section.
Our enumeration method proceeds in two steps. First, all 8 × 8 latin squares are enumerated up to isomorphism using a SAT+CAS method. Second, for every 8 × 8 latin square generated in the first step the initial 27 columns of a projective plane of order nine are defined in terms of the structure revealed in Section 2.2. For each possible way of completing the first 27 columns a SAT instance is created which is satisfiable exactly when the 27 columns can be extended to 40 columns of a projective plane.
As the structure we identified in the last section suggests, a good first step to generate the projective planes of order 9 will be to first generate all 8 × 8 latin squares up to a certain equivalence. More specifically, we will generate a representative of each main class of latin squares. Two 8 × 8 latin squares are said to belong to the same main class if they difer only by a permutation of the rows, columns, or symbols, or also possibly an exchange of the roles of these three things. Thus we can view the main class of a latin square as its orbit under the natural action of the group (8 × 8 × 8) ⋊ 3 [12, Sec 5.5]1 on the set of latin squares. To generate all such representatives, we reduce the problem to SAT, and then utilize a SAT solver to find all solutions of the instance. The exhaustive search is performed by adjoining a “solution blocking clause” to the instance whenever a solution is found. To reduce the computation, we also provide a mechanism for doing isomorphism checking along the way; if two partial squares belong to the same main class, we throw away the duplicates to reduce the computation time.
The reduction of the latin square problem into SAT is well known, and can be found in a
variety of sources [
Isomorphism removal is done by translating our latin squares to graphs and then checking
if the corresponding graphs are isomorphic to each other using pynauty [
Before performing the final isomorphism removal after generating all 8 rows of the latin
squares, there were 43,791,204 solutions found by MapleSAT. Once the isomorphism removal is
applied, there were 283,657 representatives of the main classes of latin squares which remained,
which serve as the starting point for the next step in our computation. The main classes of
latin squares of order 8 have been enumerated by others including Lam et al. [
The next major step in our enumeration of the projective planes to extend each of the 283,657 partial planes (each with 27 columns to start) to partial planes of 40 columns. We accomplish this by once again using a SAT solver. However, we take a slightly diferent approach than we did with the latin squares since the axioms of a projective plane don’t translate as nicely into SAT. A partial plane (, ) has a natural encoding as a set of Boolean variables by defining a variable , for each entry. We encode in SAT only axioms (3) and (4)—namely, that two distinct rows or columns intersect exactly once. First, the requirement that they intersect at most once is given by the quadfree clauses:
¬, ∨ ¬′, ∨ ¬,′ ∨ ¬′,′ for < ′ and < ′. If one of these clauses is false this means there is a rectangle in the incidence matrix whose corners are 1s—which is exactly what happens if two rows or columns intersect more than once.
Then, we check that a given column intersects the first 27 columns of the partial plane each at least once. Note that because the first 19 columns are the only ones which are fixed among all partial planes, we will need a diferent list of clauses for each starting point of the extension. If column ≤ 27 has 1s in the entries (1, ), (2, ), . . . , (10, ), then for ′ > 27, we include the clause 1,′ ∨ 2,′ ∨ · · · ∨ 10,′ which ensures that column ′ intersects column at least once. In addition to these clauses, we also use unit clauses to impose some structure on the first 19 rows (an exact transpose of the ifrst 19 columns in fact) in order to remove symmetry.
This is currently work in progress but in practice the extension takes about 45 seconds for
the entire pipeline (MapleSAT, GRATgen, isomorphism removal, and isomorphism removal
verification) to run for each 27-column partial plane. This still needs to be done for each of
the 283,657 latin squares which will require Compute Canada’s servers. The few 40-column
partial planes that result from this can typically be extended to a full 91 columns (or shown not
to complete at all) almost instantly [
The SAT solver MapleSAT returns DRAT proofs which can be checked using a proof verifier such as DRAT-trim [18] or GRATgen [19]. This way only the proof verifier—which is much simpler than the SAT solver—needs to be trusted.
In step 1, we do several row extensions with MapleSAT to produce the final list of latin squares. For each of these, we generate and verify the proofs for these steps. This involves adding a blocking clause for each solution of the SAT instance and then showing a conflict can be derived from the original list of clauses in conjunction with the blocking clauses. In step 2, we have a separate list of clauses for each of the 27 column partial planes, thus we end up with a separate proof for each one, all of which need to be verified independently just as in step 1. Lastly, we must also do this for the final extension from column 40 to the full 91 columns.
In addition to verifying the proofs above, we will verify the correctness of the isomorphism removal which is done at several stages. After generating solutions, we create a new file with one representative of the isomorphism class of each of the solutions in the first file. When doing so, we store the relabelling of the corresponding graph which turns it into the graph of its representative in the new file. This can then be verified easily by checking that each relabelling turns the associated solution into the one at the specified index in the new file. Representatives are chosen by determining the canonical form of the associated graph with pynauty and then using the adjacency lists of these new graphs as keys in a Python dictionary in order to only keep one of each.
The DRAT proof from step 1 can be verified by DRAT-trim in about an hour, and the isomorphism removal can be verified in about 25 hours.
This method of enumerating of the projective planes of order nine relies on two main
components: the generation of solutions with our SAT solver (MapleSAT), and the isomorphism
removal of partial solutions with our CAS (pynauty). Both components are crucial—if either
component were removed this work would not be feasible to complete in a reasonable amount
of time. To the best of our knowledge, the resulting enumeration will be the first independent
verification of the search of Lam, Kolesova, and Thiel [