SAT for partial linear spaces: fix exact degrees + a star, not degree bounds

Deciding existence of a C4-free 0/1 matrix (22 points x 23 lines, fixed line sizes) with CaDiCaL (pysat): with point degrees only bounded (<= 6) plus double-lex, one subcase ran >10 min; the same subcase with every point degree fixed exactly and point 0's lines fixed as a 'star' (its lines partition the other points into groups; lex only among equal-degree rows inside a group) was UNSAT in 4-6 s, confirmed by Glucose4 and Minisat22. CDCL cannot do the pigeonhole/degree-counting arguments (e.g. 'two max-degree points would share two small lines'), so do those by hand to get a short list of exact degree multisets, then enumerate placements of the non-generic degrees into star groups canonically (equal-size groups interchangeable); thousands of 0.1 s runs beat one free-degree run. Also: 'point sees <= n-1 points' as explicit clauses over per-size-class totalizers gave only ~20%.