Small partial linear spaces: double-lex SAT beats custom DFS by 10^4

To decide whether a partial linear space with prescribed line sizes exists (Zarankiewicz/design exceptions, ~16-18 points, ~22 lines), encode the incidence matrix X[p][l]. Use exact cardinality per line (pysat CardEnc seqcounter), one 4-literal clause per (point pair, line pair) for 'two points share at most one line', and double-lex symmetry breaking: rows lex-decreasing over all columns, columns lex-decreasing within each line-size class. Coverage constraints are unnecessary because fixed sizes force the number of uncovered pairs. With CaDiCaL 1.5.3 this found a 16-point space in 0.3 s and proved a 17-point (4 triples, 14 quads, 4 quints) linear space UNSAT in 3.6 s. A hand-written anchored DFS needed 10^8+ nodes and an unbroken plain SAT encoding timed out at 30 min. pysat's PBEnc needs the extra 'pindakaas' package; drop the PB degree bound, it is implied.