North-East Lattice Paths Avoiding $k$ Collinear Points via Satisfiability

TL;DR

This paper tackles the Gerver-Ramsey collinearity problem for north-east lattice paths by encoding the search for GR(k) walks as SAT problems. It develops CNF/KNF encodings with path constraints, non-collinearity constraints via cardinalities, symmetry breaking, and reachability handling, and applies cube-and-conquer parallelization to solve large instances. The authors fully enumerate GR(k) walks for k ≤ 6, verifying Shallit’s results (a(4)=9, a(5)=29, a(6)=97), and push the GR(7) boundary from 260 to 327 steps, with extensive reachability bounds and subpath-extension techniques. This SAT-based approach provides verifiable certificates and scalable exploration of discrete geometric problems, offering a blueprint for related combinatorial search problems.

Abstract

We investigate the Gerver-Ramsey collinearity problem of determining the maximum number of points in a north-east lattice path without $k$ collinear points. Using a satisfiability solver, up to isomorphism we enumerate all north-east lattice paths avoiding $k$ collinear points for $k \leq 6$. We also find a north-east lattice path avoiding $k = 7$ collinear points with 327 steps, improving on the previous best length of 260 steps found by Shallit.

Figures (7)

• Figure 1: A visual representation of the longest north--east walk avoiding $k=3$ collinear points. Walking two steps in the same direction introduces three collinear points, so the longest walk avoiding three collinear points alternates directions.
• Figure 2: The unique longest GR(5) walk up to isomorphism; any additional step (black) creates five collinear points.
• Figure 3: Exhaustive enumeration of GR($k$) walks for $k=4$ to $k=6$ in normal form. Color intensity indicates number of distinct walks reaching each point, with red indicating the most number of paths (the deepest red for $k=6$ corresponding to $324{,}571$ walks), blue indicating the least number of paths, and white indicating the point is unreachable using a GR($k$) walk in normal form. The red antidiagonal line corresponds to $y=(a(k)-1)-x$.
• Figure 4: A partial reachability diagram for $k=7$. Blue squares are GR(7)-reachable points, and red crosses are GR(7)-unreachable points. The black triangles show the reflected upper unreachability bound, and gray circles show the extremal bounds from Section \ref{['sec:extremalpoints']}.
• Figure 5: Heatmap of points visited by 125 distinct 305-point walks found using parallelization. Also included in the plot is the midline $y=x+1$ as well as the lines $y=x+1\pm50$.

Theorems & Definitions (2)

• Proposition 1
• proof