2
$\begingroup$

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?

Improve this question
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – RobPratt
    Commented Jun 6, 2022 at 13:58
  • $\begingroup$ @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. $\endgroup$
    – user1502040
    Commented Jun 6, 2022 at 14:25

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.