C4-free extremal incidence cases: grid of two hubs' lines kills cases
When ruling out a near-extremal C4-free (linear) point-line configuration by hand, track for each point the number of points it does NOT see: m_x = (n-1) - sum over lines through x of (|L|-1). If two high-degree points h1, h2 both see everyone, use h1's ordinary lines as rows and h2's as columns. Every other point is then a cell of a partial grid, with at most one point per cell. An empty cell (l,c) forces any point in column c whose remaining lines number |row l|-1 to miss a point of row l. Together with a lemma restricting which points can be missed (e.g. two 'pure' points never miss each other, checked exhaustively), this forced-miss lever plus total miss-capacity accounting eliminated whole subcases that a SAT solver had only shown UNSAT, without giving a readable reason. Workflow that paid off: brute-force or SAT first to know a case is dead, then hunt for the counting lever by hand.