Lex symmetry breaking per degree class: 2 s instead of 21 min
For a C4-free incidence matrix (points x lines) where one point has a different degree (e.g. degrees 6,5,5,...,5), double-lex symmetry breaking with uniform degree bounds [5,6] plus full row lex took CaDiCaL 21 min, and the transposed form (point degrees as fixed column sums) also stalled. What worked: sort rows by exact degree and impose row lex only between consecutive rows of equal degree (the same way columns are lex-ordered only within equal line sizes), with exact per-row cardinalities. That ran in 2 s. Row 0 is then the special point, column lex puts its lines first in each size class, and row lex groups the remaining points by those lines, so the 'fix a star at the max-degree point' trick appears without hand-fixing it. It is still a sound lex-leader argument: take the lex-max relabelling over degree-preserving row perms x size-preserving column perms, and swapping two out-of-order equal-class neighbours would increase it. That makes it easy to justify in a proof assistant.