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. Reply Report 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.