Back to the email M Mark Webster June 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. You're not signed in. Posting this comment will subscribe you to this newsletter with the email address you enter below. Reply and Subscribe
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.