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

Aaron Barnoff; Curtis Bright

arxiv: 2511.23226 · v2 · pith:SC7OWC3Mnew · submitted 2025-11-28 · 🧮 math.CO · cs.DM· cs.LO

North-East Lattice Paths Avoiding k Collinear Points via Satisfiability

Aaron Barnoff , Curtis Bright This is my paper

Pith reviewed 2026-05-17 03:53 UTC · model grok-4.3

classification 🧮 math.CO cs.DMcs.LO

keywords north-east lattice pathsavoiding collinear pointssatisfiability solversenumerationGerver-Ramsey problemlattice path constructions

0 comments

The pith

Satisfiability solvers classify all north-east lattice paths avoiding up to six collinear points and find a 327-step example for seven.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper applies satisfiability techniques to the Gerver-Ramsey problem of building the longest possible north-east lattice path without k collinear points. It enumerates every such path up to isomorphism when k is six or smaller. It also exhibits a path of 327 steps that avoids seven collinear points, longer than the earlier record of 260 steps. A reader might care because the complete lists for small k provide a foundation for understanding all possible avoiding configurations, while the new example shows how far computational search can extend known constructions.

Core claim

Using a satisfiability solver, up to isomorphism we enumerate all north-east lattice paths avoiding k collinear points for k ≤ 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.

What carries the argument

SAT encoding of the condition that a north-east lattice path has no k collinear points, used to drive exhaustive search up to isomorphism.

If this is right

All isomorphism classes of avoiding paths are known for k ≤ 6.
There exists a north-east lattice path of 327 steps avoiding 7 collinear points.
The prior record length of 260 steps for k=7 has been surpassed by computational means.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The enumerated paths for small k could be extended step by step to seek even longer avoiding paths for k=7.
The SAT method may apply to similar avoidance problems on other types of paths or grids.
Independent verification of the 327-step path would confirm the improvement over Shallit's construction.

Load-bearing premise

The SAT encoding correctly captures the collinearity-avoidance condition and the solver finds all solutions up to isomorphism for k≤6 while producing a genuine 327-step avoiding path for k=7.

What would settle it

An exhaustive manual or alternative computational enumeration of north-east lattice paths for k=6 that identifies an avoiding path not present in the SAT results, or a check that reveals seven collinear points in the reported 327-step path.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

SAT solver gives complete enumeration for k≤6 and pushes the k=7 lower bound from 260 to 327 steps, but the abstract supplies no encoding details.

read the letter

The key takeaway is that this paper applies SAT solving to enumerate north-east lattice paths avoiding k collinear points for k up to 6, and finds a 327-step example for k=7 that improves on Shallit's 260-step construction. What stands out is the use of computational search to get complete lists for the smaller values and a better lower bound for k=7. That's concrete progress on the Gerver-Ramsey problem, and the abstract positions it as going beyond prior work. The soft spot is obvious from the abstract alone: there's zero detail on the encoding. How do they turn the no-k-collinear condition into CNF clauses? Are all possible slopes and lines covered? Without that, or without the actual paths or verification steps, the claims rest on trust in the solver output. The stress-test note is right to flag this as unverifiable right now. No issues with circularity or invented parameters here; it's a straight computational result. This paper is for people who care about lattice paths and combinatorial geometry, especially those open to computational approaches. A reader in that area gets new numbers to work with. It deserves a serious referee. The results look like they could be checked if the full paper includes the encoding and perhaps some sample paths. I'd say send it to review.

Referee Report

2 major / 0 minor

Summary. The manuscript investigates the Gerver-Ramsey problem of finding the longest north-east lattice paths without k collinear points. It claims to have used a satisfiability solver to enumerate all such paths up to isomorphism for k ≤ 6 and to have discovered a 327-step path avoiding 7 collinear points, improving on Shallit's previous record of 260 steps.

Significance. If the results are correct, the enumerations for small k and the improved lower bound for k=7 advance knowledge of the maximum lengths in this combinatorial geometry problem. The SAT-based computational approach is a positive aspect, as it allows systematic search for avoidance conditions that may be difficult to handle by hand.

major comments (2)

[Abstract] Abstract: The manuscript reports computational enumerations and a new 327-step example but supplies no description of the SAT encoding, including variable definitions for east/north steps, clause generation for the no-k-collinear-points condition, or handling of slopes and boundary cases. This encoding is load-bearing for all claimed results.
[Abstract] Abstract: No details are given on the solver used, the method for enumerating up to isomorphism, run times, or any post-processing verification that the satisfying assignments correspond to valid paths satisfying the geometric condition. Without these, the soundness of the k≤6 enumerations and the k=7 example cannot be evaluated.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and for identifying the need for greater methodological transparency. We agree that the current manuscript lacks sufficient detail on the computational approach and will make major revisions to address both comments.

read point-by-point responses

Referee: [Abstract] Abstract: The manuscript reports computational enumerations and a new 327-step example but supplies no description of the SAT encoding, including variable definitions for east/north steps, clause generation for the no-k-collinear-points condition, or handling of slopes and boundary cases. This encoding is load-bearing for all claimed results.

Authors: We agree that a description of the SAT encoding is essential. The abstract is intentionally brief, but the full manuscript will be revised to include a dedicated section detailing the variable definitions (boolean variables indicating east or north steps at successive positions), the clause construction for forbidding any k points from being collinear (via exhaustive enumeration over candidate slopes and point sets), and the handling of slopes together with boundary conditions that keep the path within the north-east quadrant. revision: yes
Referee: [Abstract] Abstract: No details are given on the solver used, the method for enumerating up to isomorphism, run times, or any post-processing verification that the satisfying assignments correspond to valid paths satisfying the geometric condition. Without these, the soundness of the k≤6 enumerations and the k=7 example cannot be evaluated.

Authors: We accept this criticism. The revised manuscript will specify the SAT solver and configuration employed, describe the technique used to enumerate solutions up to isomorphism (via symmetry-breaking constraints or canonical reduction), report the observed run times, and outline the post-processing verification that converts each satisfying assignment into an explicit path and confirms it satisfies the geometric no-k-collinear condition by direct coordinate checks. revision: yes

Circularity Check

0 steps flagged

No circularity; result is direct computational output

full rationale

The paper uses a SAT solver to enumerate north-east lattice paths avoiding k collinear points up to isomorphism for k≤6 and reports a 327-step example for k=7. The provided abstract contains no equations, parameter fits, self-citations, or derivations. The central claim is an exhaustive search result from an external solver applied to a geometric condition; no step reduces by construction to its own inputs or relies on a load-bearing self-citation chain. This is a self-contained computational discovery against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Abstract-only review yields no explicit free parameters, invented entities, or non-standard axioms; the work rests on the standard definition of north-east lattice paths and the Gerver-Ramsey collinearity condition.

axioms (2)

standard math North-east lattice paths consist of east and north unit steps on the integer grid.
Standard combinatorial definition invoked by the problem statement.
domain assumption k collinear points means k distinct points of the path lie on a single straight line in the Euclidean plane.
Core condition of the Gerver-Ramsey problem referenced in the abstract.

pith-pipeline@v0.9.0 · 5348 in / 1333 out tokens · 39307 ms · 2026-05-17T03:53:49.565526+00:00 · methodology