There are exactly 56 simple symmetric 7-Venn diagrams

Up to isomorphism there are exactly 56 simple symmetric Venn diagrams with seven curves: 23 monotone ones and 33 non-monotone ones. The 23 were proved complete in 2010. The 33 were found by a randomized search in 1998, and the list was believed complete but never proved. Claude wrote a SAT encoding that every such diagram satisfies. The solver found 636 labelled solutions, which fall into 56 diagrams, and its final "no more solutions" answer comes with a proof file that the checkers drat-trim and lrat-trim accept. Claude has written it up as a paper draft under my direction. The draft is not published, so this post is the public account.

It follows up on the 17, 19 and 23 curve diagrams in arXiv:2609.26546, which I described in another post. That post mentions a blind search on October 8 that found 56 distinct seven-curve diagrams, matching the known counts, without showing that there are no others. Claude wrote the generator and ran the searches and the proof certification. Codex reviewed the result and wrote its own checks. I picked the problem and directed the work.

A Venn diagram of n curves is n closed curves in the plane in which each of the 2^n combinations of inside and outside is exactly one connected region. It is simple if no three curves meet at a point, and symmetric if rotating it by 1/n of a turn maps each curve to the next. A symmetric one can only exist for prime n. For seven curves that means 128 regions and 126 crossings. A diagram is monotone if every region inside k curves, for 0 < k < n, touches a region inside k-1 curves and one inside k+1. Those are the diagrams you can draw with convex curves. Two diagrams count as the same if a homeomorphism of the plane takes one to the other or to its mirror image, or if one is the polar flip of the other (the outer region and the innermost region trade places). The curves are unlabelled.

The survey by Ruskey and Weston, "A Survey of Venn Diagrams" (Electronic Journal of Combinatorics, Dynamic Survey DS5, 2005 edition), lists 23 monotone and 33 non-monotone simple symmetric 7-Venn diagrams. In 2010 Cao, Mamakani and Ruskey ("Symmetric monotone Venn diagrams with seven curves", Fun with Algorithms, FUN 2010) proved with a modified algorithm that there are exactly 23 monotone ones. One of their open problems reads: "Find the total number of simple symmetric non-monotone 7-Venn diagrams."

The 33 came from Chow and Ruskey, who started from a pie-slice arrangement and applied "random (or hill-climbing) moves that preserve the number of intersections". The survey says "We believe that these are all". Nobody had shown it.

The encoding

Label each region by the set of curves that contain it. Those labels are the 128 corners of the 7-dimensional cube. At a crossing of curves a and b, the four surrounding regions are u, u+a, u+a+b and u+b, which is one square (a 2-face) of the cube. So a diagram becomes a set of 126 squares, one per crossing.

Rotation shifts every curve index by one, so the set of squares must be unchanged by that shift. The cube has 672 squares, which fall into 96 orbits of seven, and a diagram uses 18 of the orbits. That gives the solver 96 true/false variables.

The conditions are: every edge of the cube lies in 0 or 2 chosen squares; every corner lies in some chosen square; around each corner the chosen squares form a single cycle; the chosen squares are connected; the squares along curve 0 form one cycle; and 18 orbits are chosen. Together these say the squares glue into a sphere whose dual is the diagram. Short lemmas in the paper draft show that every real symmetric diagram satisfies them.

The cycle and connectivity conditions are awkward to write as clauses up front, so the search adds them lazily. The solver proposes an assignment, a checker finds a condition it breaks, and a clause goes in that this assignment violates and every real diagram satisfies. Whenever an assignment is a genuine solution it is written out as a certificate, checked, and blocked.

The run made 998 solver calls in 989 seconds. It added 1,074 such clauses (815 for curve 0's cycle, 193 for connectivity, 66 for the cycles around corners) and 636 blocking clauses, and then the formula (2,904 variables, 8,964 clauses) was unsatisfiable. Relabelling the curves and turning the sphere inside out give a group of 12 symmetries. The 636 solutions are 50 classes of 12 plus 6 classes of 6, so 56 classes, and 23 of them are monotone. The survey describes each diagram by a set of strings that does not change under these symmetries or any relabelling, and the 56 classes match its 56 entries one to one, with no entry hit twice.

Checking it

To back the final "unsatisfiable", Kissat 4.0.4, with bounded variable addition turned off so that every proof step is a simple one, wrote a DRAT proof of about 597 MB. The checker drat-trim verified it and wrote an LRAT version of about 2.98 GB, and lrat-trim 0.2.0 verified that. Kissat took about 914 seconds, drat-trim 1,638 and lrat-trim 28. As a control, both checkers were handed a fake proof, just the empty clause, for a satisfiable formula, and both rejected it. An earlier LRAT checker we had used was retired after it accepted a fake refutation.

There is also a second encoder, written separately and sharing no code with the first. It derives its own base formula (1,920 variables, 8,803 clauses) and checks each of the 1,710 added clauses against its stated justification. Its final formula has 10,513 clauses, with a DRAT proof of about 601 MB and an LRAT proof of about 3.15 GB, verified the same way.

Codex was told to write its own code and not import ours. It wrote a third generator for the base formula, audited all 1,710 added clauses against their witnesses, checked all 636 certificates directly, and refereed the prose lemmas. In a second session it rebuilt the second encoder's formula without using our generator code, ran lrat-trim on that encoder's LRAT proof (7,889,127 clauses checked), and confirmed that a copy with one hint removed is rejected.

What you have to trust

Codex used the same lrat-trim binary we did, and the LRAT file it checked came out of our own drat-trim run. drat-trim and lrat-trim are unverified C programs. The first encoder's LRAT proof was produced after Codex's review and has only been checked by our pipeline. The match with the survey's strings has a single implementation, and Codex did not run a search of its own.

The count needs only one direction: every real symmetric diagram satisfies the base conditions, and every clause added during the search holds for every real diagram. The other direction, that each solution is a real diagram, is checked directly on each of the 636 certificates. The needed direction rests on short prose lemmas. Codex refereed them and found them sound, but its review is, in its own words, "reasoned inferences, not mechanically certified topology", and nobody has formalised them in a proof assistant. A formal proof of those lemmas would make the whole count machine-checked. We have not done that.

Since the list is complete, no simple symmetric non-monotone 7-Venn diagram is polar symmetric, which removes the word "known" from the survey's remark that "there are no known symmetric non-monotone Venn diagrams with polar symmetry". That step still rests on the survey's own check of the 33.

The proof files and the code are not public yet.