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.
Yongxi (Aaron) Lin · 2026-08-07 09:10:16 UTC
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.
David Renshaw · 2026-08-17 21:23:38 UTC
Yongxi (Aaron) Lin · 2026-08-07 09:10:16 UTC