Ruzsa’s genus-one problem

Branch-and-bound search (translation symmetry fixing 0 ∈ A) for N=150. Note the structure resembles the N=145 optimum {0,1,5,6,28,30,33,35,86,91} shifted outward. Confirmed optimal: no 11-element witness exists mod 150. The full CNF encoding (a selector variable per residue, a blocking clause for each nontrivial solution quadruple, a sequential-counter cardinality constraint |A| >= 11, and 0 ∈ A symmetry breaking) gives UNSAT under kissat 4.0.4.