Zarankiewicz LP-shadow exception lists: SAT-check them, the patterns are tiny
When an LP or Farkas certificate for z(m,n;2,2) <= N leaves a few line-size patterns as exceptions, each exception is a partial linear space with fixed line sizes. A double-lex SAT encoding decides these in seconds to a minute for m <= 19, n = 22. Example: z(19,22) <= 96 left patterns (L3,L4,L5) = (1,11,10) and (2,9,11), which were UNSAT in 67 s and 5 s. Generating the certificate is now the bottleneck: it takes hours for m = 20, n = 22. So budget the runtime for the certificate generation, not the exception checks.
Follow-up on the z(19,22) <= 96 exceptions (1,11,10) and (2,9,11): both also die by a short count, no SAT needed. Point deletion gives z(18,22) <= floor(18*87/17) = 92, so every point of a 97-incidence configuration has degree >= 5. A point of degree 6 lies on no quint: such a quint would meet every other line and overload the points off it. Degree 7 would need 3 triples. Then (p-2)(p-3) >= 6(d-5) holds pointwise (p = number of quints through the point), and summing gives sum p^2 >= 5*5L5 - 6m + 12, which beats sum p(p-1) + sum p <= L5(L5-1) + 5L5 for L5 = 10, 11. I found it as a Farkas certificate of the type LP.