I can confirm Pontus's answers for $3 \times 3$ and $4 \times 4$. I used Python for enumerating possible boards and Z3 for checking if each board has a unique solution:
def puzz126600():
class DisjointSet(object):
def __init__(self, n):
self.parent = [*range(n)]
self.rank = [0] * n
def find(self, n):
while self.parent[n] != n:
self.parent[n] = self.parent[self.parent[n]]
n = self.parent[n]
return n
def union(self, n1, n2):
n1 = self.find(n1)
n2 = self.find(n2)
if n1 == n2: return False
if self.rank[n1] < self.rank[n2]:
n1, n2 = n2, n1
self.parent[n2] = n1
if self.rank[n1] == self.rank[n2]:
self.rank[n1] += 1
return True
import z3
from itertools import product
from collections import defaultdict
def partitions(n):
dp = [[[]]]
for l in range(1, n+1):
cur = []
for first in range(1, l+1):
rest = l - first
for r in dp[rest]:
cur.append([first] + r)
dp.append(cur)
return dp[-1]
def grid_printer(n, horizontal, vertical):
canvas_row1 = '+-' * n + '+'
canvas_row2 = '| ' * n + '|'
canvas = [list(row) for row in [canvas_row1, canvas_row2] * n + [canvas_row1]]
for r in range(n):
start_idx = 0
for width in horizontal[r]:
canvas_r = r * 2 + 1
for c in range(start_idx, start_idx + width - 1):
canvas_c = c * 2 + 1
canvas[canvas_r][canvas_c + 1] = ' '
start_idx += width
for c in range(n):
start_idx = 0
for width in vertical[c]:
canvas_c = c * 2 + 1
for r in range(start_idx, start_idx + width - 1):
canvas_r = r * 2 + 1
canvas[canvas_r + 1][canvas_c] = ' '
start_idx += width
for row in canvas:
print(''.join(row))
def solve(n, connected_only=False):
parts = partitions(n)
frag_sets = defaultdict(list)
for grid in product(parts, repeat=n):
counts = [0] * n
for row in grid:
for part in row:
counts[part-1] += 1
frag_sets[tuple(counts)].append(grid)
# print(sum(len(grids) ** 2 for grids in frag_sets.values()))
answer = 0
cases_checked = 0
for grids in frag_sets.values():
for horizontal in grids:
for vertical in grids:
dset = DisjointSet(n * n)
components = n * n
solver = z3.SolverFor('QF_FD')
grid = [[z3.Int(f'a{r}{c}') for c in range(n)] for r in range(n)]
for r in range(n):
start_idx = 0
for width in horizontal[r]:
for c in range(start_idx, start_idx + width - 1):
components -= dset.union(r * n + c, r * n + c + 1)
space = [grid[r][c] for c in range(start_idx, start_idx + width)]
for v in space:
solver += 1 <= v
solver += v <= width
solver += z3.Distinct(*space)
start_idx += width
for c in range(n):
start_idx = 0
for width in vertical[c]:
for r in range(start_idx, start_idx + width - 1):
components -= dset.union(r * n + c, (r + 1) * n + c)
space = [grid[r][c] for r in range(start_idx, start_idx + width)]
for v in space:
solver += 1 <= v
solver += v <= width
solver += z3.Distinct(*space)
start_idx += width
if connected_only and components != 1: continue
if solver.check() == z3.sat:
model = solver.model()
solution = [[model.eval(v) for v in row] for row in grid]
solver += z3.Or(*[v != sol for vrow, solrow in zip(grid, solution) for v, sol in zip(vrow, solrow)])
if solver.check() == z3.unsat:
#print('unique', horizontal, vertical)
#grid_printer(n, horizontal, vertical)
answer += 1
cases_checked += len(grids) ** 2
print(f'{cases_checked} cases checked')
print(answer)
solve(3, False)
solve(4, False)
For an additional challenge by Carmeister (the ones where all cells are connected), I found
exactly 2 different grids up to symmetry:
Analysis:
If one of the rows has a (1,1,1) partition, one of the columns must be too. (In order to have three chunks of ones without a (1,1,1), all three columns must be either (1,2) or (2,1), but the two remaining rows cannot be divided into three chunks of 2.) Then the cell at the intersection of such row and column is isolated.
On the other hand, if all rows are (3) i.e. no dividers at all, all columns are also (3) and there are 6 solutions in this board. Therefore, at least one row and one column are either (1,2) or (2,1), and the rest are (3).
If two rows are (1,2), i.e. a divider on the same side, there are two 1s forced on the first column, so there must be a divider on it. Then one or two cells are isolated in all cases. Therefore, a valid solution has at most one (1,2) and one (2,1) for its rows, and the same goes for columns.
The rest was mental case bashing on the remaining cases. The answer was cross-checked by running solve(3, True) in the code above.
