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

1. 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.