The Expensive Half of a SAT Proof

Here is a number that bothered me for a week. I wanted the exact value of a small combinatorial quantity called z(10,11;3,4). A SAT solver found a good configuration in about two seconds, which told me the answer was at least 72. To finish, I needed the other direction: a proof that nothing does better, that the answer is at most 72. I started that second SAT job and walked away. It ran for more than seven days without an answer.

Then I added one idea, an old and standard one, and the same proof finished in 27 minutes.

The idea is symmetry breaking. This post builds it up from scratch, watches it work on the problem above (the payoff was three new values in the On-Line Encyclopedia of Integer Sequences), and then watches it fail on a different problem, because knowing when a tool stops working is most of the skill of using it.

A problem you can hold in your hand

The quantity z(m,n;s,t) is the largest number of 1s you can put in an m-by-n grid of 0s and 1s without creating an all-ones s-by-t block. By “block” I mean: pick some s rows and some t columns; the s-by-t cells where they cross must not all be 1.

Picture a 4-by-4 grid. If rows 1 and 3 and columns 2 and 4 all carry 1s at their four intersections, that is a forbidden 2-by-2 block. Avoid every such block, pack in as many 1s as you can, and the maximum is the Zarankiewicz number. These numbers grow in a ragged, formula-resistant way, which is exactly why people compute them one at a time.

This is a natural fit for a SAT solver. Put one Boolean variable on each cell, true when the cell is 1. For every choice of s rows and t columns, add one clause saying “at least one of these s times t cells is 0.” Add a counting constraint, “at least k cells are 1,” and ask the solver:

• If it answers satisfiable, it hands back a grid with k ones and no forbidden block. So z is at least k.
• If it answers unsatisfiable, no such grid exists, so z is less than k.

To pin the exact value you need both: a witness at k, and an impossibility proof at k+1. The witness side is usually easy. The impossibility side, the UNSAT side, is the expensive half.

Why proving impossibility is hard

The asymmetry is intuitive once you say it out loud. To find a witness, the solver needs one lucky arrangement. To prove impossibility, it must rule out every arrangement. That is already a harder job. But there is a second, sneakier cost, and it is the one that matters here.

The solver keeps rediscovering the same grid wearing different clothes.

Take any valid grid. Swap two of its rows. You get a different assignment of the Boolean variables, but it is plainly the same object: same number of 1s, same blocks present or absent. Swap two columns: same story. The solver does not know this. To the solver, the original and the swapped version are two different points in the search space, each to be explored and refuted from scratch.

Counting the copies

Name the thing that is hurting us. The row permutations and the column permutations form a group that acts on every grid while preserving both what we are maximizing (the count of 1s) and what we are forbidding (the blocks). So the grids come in families, called orbits, and every grid in an orbit is the same object relabeled.

How big is an orbit? For a 10-by-11 grid, you can reorder the rows in 10! ways and the columns in 11! ways:

10! times 11! is about 1.4 times 10^14.

That is roughly a hundred trillion relabelings of a single grid. When the solver is trying to prove that no good grid exists, it is wading through a hundred trillion copies of each candidate it has already dismissed. No wonder the job ran for a week.

The fix: keep one copy of each

The cure is to refuse all but one member of each orbit. If we can tell the solver “only consider the canonical version of each grid,” the search shrinks by the size of the orbits.

The standard canonical choice is the lexicographically smallest relabeling, and the standard way to enforce it cheaply is called double-lex:

• require the rows to be in non-decreasing lexicographic order, and
• require the columns to be in non-decreasing lexicographic order.

Read each row left to right as a string of 0s and 1s; demand row 1 is no larger than row 2, which is no larger than row 3, and so on. Do the same down the columns.

The reason this is allowed, and it is worth saying carefully, is a soundness fact: every orbit contains at least one grid that is both row-sorted and column-sorted. So when we throw away every non-doubly-lex grid, we never throw away an entire orbit. If a good grid existed before, a good doubly-lex grid still exists. Satisfiability is untouched, and so is unsatisfiability. We have deleted only redundant copies, never an actual solution. That is the whole game.

Saying “this row is not bigger” in clauses

A SAT solver speaks in clauses, so we have to express “this 0/1 vector is lexicographically less than or equal to that one” as a pile of ORs. The construction is a small classic, and building it is the kind of thing this blog likes to do by hand.

Compare two vectors a and b, position by position from the left. Carry one extra Boolean per position, an “equal so far” flag. The rule:

• while the prefixes are still equal, the current bits must satisfy a-bit implies b-bit (you are not allowed to be the one that is larger);
• update the “equal so far” flag to stay true only if the current bits match.

In clause form, at each position, with eq meaning equal-so-far:

# if equal so far, then a <= b at this position
(not eq) OR (not a) OR b

# eq_next is true exactly when eq held and the bits matched
# (a handful of clauses define eq_next = eq AND (a == b))

It is linear in the length of the vector, and you can check it against a truth table to be sure (I did, for all vectors up to length four, before trusting it on anything larger). Apply it to each adjacent pair of rows and each adjacent pair of columns, and you have double-lex.

One honest caveat. Double-lex is not a complete symmetry break. Some orbits still keep more than one doubly-lex member, and we only constrained adjacent pairs rather than all permutations directly. It is sound and cheap, not perfect. That is fine. Removing most of the symmetry is enough to turn intractable into tractable, and chasing a unique representative would cost more than it returns.

The payoff, in real seconds

First, sanity. A known value: z(9,9;3,4) is 56. The proof that it is not 57 is a small UNSAT instance. With the plain encoding, the solver did not finish it inside a 90-second budget. With double-lex, it finished in about ten seconds. The symmetry break is the difference between “no answer” and “ten seconds” on a problem whose answer we already knew, which is exactly the kind of validation you want before trusting it on a problem whose answer you do not.

Then the one that started this post:

That 27-minute proof, paired with the two-second witness, settled z(10,11;3,4) = 72 exactly. Two siblings fell the same way. All three went to the OEIS as new values of classic Zarankiewicz sequences (A006615, A006622, A006625), and they sit alongside the rest of my OEIS contributions, which is where this kind of computed-then-verified result tends to land.

Now watch it fail

If the story stopped there, you might think symmetry-broken SAT is a frontier machine. It is not, and the failure is more instructive than the success.

Try a different problem: the most edges you can put on n points without ever forming a 4-cycle (a square). This is also a 0/1 matrix question, an adjacency matrix this time, and it has the same flavor of symmetry, so the same tool should apply. I built it and validated it: it reproduces the known values (OEIS A006855) exactly up to n = 15.

Then it dies. The runtime grows by roughly a factor of five for every extra vertex. By n = 15 a single value already takes about a minute, and the known frontier sits at n = 41. Five to the twenty-sixth power times a minute is not a number of minutes anyone will wait. The tool that cracked Zarankiewicz in 27 minutes cannot get near this frontier at all.

Why the split? It comes down to the shape of the symmetry.

• In the Zarankiewicz grid, rows and columns are separate axes. You can sort them independently, and the dimensions are modest (10 by 11). Adjacent lexicographic order removes enough of the redundancy to win.
• In a graph, there is one symmetry, the relabeling of vertices, and it permutes the rows and the columns of the adjacency matrix together. Adjacent-pair lexicographic order barely dents that single large group, and the leftover symmetry still explodes the search.

The people who actually reach the C4-free frontier do not use plain SAT at all. They use orderly generation, building graphs in a canonical form so that no two relabelings are ever produced (the lineage of nauty and its relatives). That is a different and heavier instrument.

The lesson generalizes. Symmetry-broken SAT scales when the symmetry group is a product of modest factors you can sort independently, and it stalls when it is one big group. Before you reach for it, look at the symmetry you are facing and ask which of those two worlds you are in.

Credit where it is due

None of the machinery here is mine, and that is worth stating plainly rather than burying. Double-lex symmetry breaking for matrix models is from Flener, Frisch, Hnich, Kiziltan, Miguel, Pearson, and Walsh, “Breaking row and column symmetries in matrix models” (CP 2002). Attacking Zarankiewicz numbers with symmetry-aware SAT was done by Jeremy Tan in “An attack on Zarankiewicz’s problem through SAT solving” (2022). The lexicographic clause encoding is textbook (Knuth, TAOCP 7.2.2.2; and Codish and collaborators). The only new things in my version are the particular values that came out the other end.

That is, in a way, the point of the post. This is a standard technique that lives mostly inside the constraint-programming community and is underused everywhere else. If you find yourself staring at a SAT job that will not prove the impossibility you are sure is true, count the symmetries first. There may be a hundred trillion copies of your problem hiding in plain sight, and a few lexicographic clauses to make them go away.

Takeaways

• The UNSAT side of an exact-value SAT proof is the expensive half, and symmetry is usually why.
• Canonical-representative constraints (double-lex) are cheap, sound, and often decisive: they keep one grid per orbit instead of all m! times n! of them.
• They are standard in constraint programming and underused elsewhere.
• They scale on product-of-modest-groups symmetry (the Zarankiewicz grid) and stall on one large group (graph vertex relabeling), where canonical generation is the right tool instead. Match the method to the symmetry.

The code (a lexicographic-CNF builder, the Zarankiewicz attack, and the C4-free contrast case, all with tests) lives in my open-problems repository.