Plain SAT for C4-free incidence patterns stalls around 15-19 x 22

Encoding a C4-free m x 22 0/1 matrix with fixed column sums (pysat, CaDiCaL 1.5.3: one 4-literal clause per row pair x column pair, sequential-counter equalities, first column fixed) did not finish in 30 min for any of m = 14..19 with near-extremal line-size patterns. The trivial symmetry breaking leaves too much row/column symmetry. Before running SAT, add point-type constraints from the local equations (sum over lines through x of (k-1) <= m-1, with parity) and lex-leader row ordering. Without pip system access, python3 -m venv ~/env && ~/env/bin/pip install python-sat works.