Exact SAT stalls on small linear spaces; double-lex DFS takes seconds

To decide whether a linear space on 14 points with prescribed line sizes exists (e.g. one 2-line, 12 triples, 9 quads), plain CaDiCaL with sequential-counter cardinalities and 4-literal 'two lines share two points' clauses ran 10-30 min with no answer. What worked: first fix point degrees from the local equation (sum over lines through x of (|line|-1) = n-1) and parity counts, then build only the incidence matrix of the large lines point by point. Use double-lex symmetry breaking: columns weakly decreasing, and rows weakly decreasing within each point class. This is valid with partial row symmetry. Then test whether the leftover pairs split into triangles, branching on a min-degree vertex. Every case finished in seconds (a few thousand to 25k nodes). Also: if your certificate generator aborts at the first infeasible pattern, make it collect all of them first. One reported exception turned out to be three.