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?