Back to the email M Mark Webster June 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. 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 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.