Computer Things

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

Would it be simpler to code the regions as row vectors, so it's similar to the queen positions? I don't know SAT or SMT, so the syntax could be rather 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 each cell is assigned to exactly one region, and the region constraint becomes 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.