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

Technical Summary: North–East Lattice Paths Avoiding $k$ Collinear Points via Satisfiability

Problem Definition
This paper investigates the Gerver–Ramsey collinearity problem, which seeks to determine the maximum length of a north–east lattice path (steps in $\{(1,0), (0,1)\}$) that avoids containing $k$ collinear points. Let $a(k)$ denote the smallest integer such that every north–east lattice path of length $a(k)$ contains $k$ collinear points; consequently, $a(k)-1$ is the length of the longest such path avoiding $k$ collinear points. While Montgomery (1972) proved that such a bound exists for all $k$, and Gerver and Ramsey (1979) provided an explicit but extremely loose upper bound, the exact values of $a(k)$ for small $k$ remained largely unknown or computationally difficult to verify. Prior to this work, J. Shallit (2013) had computationally determined $a(4)=9$, $a(5)=29$, and $a(6)=97$, and established a lower bound of $a(7) \ge 261$ by finding a path of length 260.

Methodology
The authors employ Boolean Satisfiability (SAT) solving to enumerate and verify these lattice paths. The core approach involves encoding the existence of a path of length $m$ avoiding $k$ collinear points as a Conjunctive Normal Form (CNF) formula.

1. SAT Encoding:

   • Variables: Boolean variables $v_{x,y}$ represent whether point $(x,y)$ is on the path.
   • Path Constraints: Clauses ensure the path starts at $(0,0)$, moves only North or East, and does not split (i.e., from any point, the path proceeds to exactly one of the two possible next points).
   • Non-Collinearity Constraints: The authors use cardinality constraints (at-most-$k$) to ensure no line contains $k$ points. These are encoded into CNF using sequential counter encodings or handled natively via "at-least-$k$ conjunctive normal form" (KNF) using klauses.
   • Optimizations:
     • Symmetry Breaking: The search space is reduced by enforcing the first step to be North, eliminating complementation symmetry. Reversal symmetries were largely ignored during search to avoid encoding overhead, with isomorphism checks performed post-enumeration.
     • Reachability Bounds: Points proven unreachable (e.g., those requiring $k-1$ consecutive steps in one direction) are blocked via unit clauses.
     • Constraint Removal Heuristic: To improve solver efficiency, non-collinearity constraints corresponding to lines with very few points in the relevant region are removed. If a solution is found, it is explicitly verified to ensure no $k$ collinear points exist.
     • Parallelization: For large instances, the "cube-and-conquer" technique is used. A lookahead solver (march) partitions the search space into disjoint subproblems (cubes), which are then solved in parallel.

2. Solver Selection:

   • The authors benchmarked standard CNF encodings (solved by CaDiCaL) against KNF encodings (solved by Cardinality-CaDiCaL).
   • Results indicated that KNF performs significantly better on satisfiable instances (finding long paths), while CNF is superior for unsatisfiable instances (proving non-existence of longer paths). The methodology adapts the encoding type based on whether the goal is to find a path or prove its non-existence.

Key Results
The paper presents the following computational results:

• Enumeration for $k \le 6$: The authors exhaustively enumerated all maximal GR($k$) walks (paths of length $a(k)-1$) up to isomorphism for $k \le 6$.

  • Confirmed previous results: $a(4)=9$, $a(5)=29$, and $a(6)=97$.
  • Found that there are two distinct maximal GR(4) walks, one unique maximal GR(5) walk, and two distinct maximal GR(6) walks.
  • Generated DRAT proof certificates for the non-existence of longer paths, allowing independent verification of the results without trusting the SAT solver itself.

• Advances for $k = 7$:

  • Lower Bound Improvement: The authors discovered a GR(7) walk of length 327 steps, significantly improving the previous best known length of 260 steps found by Shallit.
  • Reachability Analysis: They determined upper and lower reachability bounds for GR(7) walks up to 267 steps and identified the first unreachable point on the line $y=x+1$ at $(146, 147)$.
  • Search Strategy: The longest walks were found using a hybrid approach involving random seed parallelization and cube-and-conquer. Notably, the longest walks found were concentrated near the line $y=x+1$.

Significance and Claims
The paper claims that SAT solvers are not only effective for solving discrete geometry problems with enormous search spaces but can also provide higher levels of trustworthiness than custom-written search code due to the ability to generate and verify proof certificates (DRAT format).

The primary contributions are:

1. A SAT-based method for finding long GR($k$) walks and proving their maximality.
2. The complete enumeration of maximal GR($k$) walks for $k \le 6$, confirming and extending previous computational results.
3. A new lower bound for $a(7)$, extending the known longest path from 260 to 327 steps.
4. An experimental study demonstrating that while the exact value of $a(7)$ remains unknown, SAT solving can effectively navigate the search space to find significantly longer paths than previously discovered, and that proof certificates can be generated for non-existence claims.

The authors remain modest regarding the determination of $a(7)$, noting that the exact value is still unknown, but they hope their introduction of SAT solving to this problem will facilitate further progress.