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