# Good encoding for grid layout problem

How would you encode the problem given by https://oeis.org/A337663 with an off-the-shelf solver?

You need to lay out $$n$$ ones and $$2, 3, ..., m$$ on an infinite grid, for $$m$$ as large as possible. For each $$x > 1$$, the sum of $$x$$'s neighbors (including diagonals) less than $$x$$ must equal $$x$$.

Assume you believe $$m$$ is the right answer and you want to prove that $$m + 1$$ is impossible.

I've tried several different solvers and encodings; numerical position variables, displacement matrices with $$d(i, k) = d(i, j) + d(j, k)$$, only enforcing the adjacency constraints and then lazily blocking bad paths, etc.

Right now CP-SAT with explicit position variables seems to work best (I don't have access to non-free solvers), but nothing is competitive with a hand-rolled solution.

Maybe I need more manual symmetry breaking?

• I played around with this a couple years ago. Have you tried binary assignment variables $y_{ijk}$ to indicate whether cell $(i,j)$ contains value $k$? If not, I'll post the formulation I used. Jun 6, 2022 at 13:58
• @RobPratt Yes, it didn't work very well. I think you need to exploit the translation symmetry if you want competitive results. But it does have the advantage of breaking the permutation symmetry of the 1s. Jun 6, 2022 at 14:25