Computer Things

Subscribe
Archives
  Back to the email
Mark Webster
Jun. 17, 2025, afternoon

Would it be simpler to encode the regions in a row-based format, in a similar way to the queens? I don't know SAT or SMT, so this might be syntactically off, but something like

r_0 = [1, 1, 1, 1, 1, 1, 1, 1, 1] r_1 = [1, 1, 2, 3, 3, 3, 9, 9, 9] ...

ensures that each cell is assigned to exactly one region, and the region constraint is now that r_0[q_0], r_1[q_1] etc. are distinct.

Reply Report
Powered by Buttondown, the easiest way to start and grow your newsletter.