Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Constraint Satisfaction Programming for the No-three-in-line Problem

Thomas Prellberg

TL;DR

This work solves the classical no-three-in-line problem on $n\times n$ grids for all $n\le 60$ by formulating it as a constraint-satisfaction problem and employing a symmetry-reduced CP-SAT model. The authors exploit $90^\circ$ rotational symmetry to reduce the search space, enabling construction of $2n$-point configurations and proving $D(n)=2n$ for all $2\le n\le60$, thereby shifting the unknown boundary to $n=61$. They analyze solve-time behavior under a run-until-first-success parallel protocol and introduce a shifted-exponential model to describe early-time performance, providing practical extrapolations for planning large-scale runs. The work also documents data availability and suggests directions for further speedups and deeper structural insights to guide exact search in combinatorial geometry.

Abstract

Using a constraint satisfaction approach, we exhibit configurations of $2n$ points on the $n\times n$ grid for all $n\le60$ with no three collinear. Consequently, the smallest $n$ for which it is unknown whether $D(n)=2n$ increases from $47$ to $61$.

Constraint Satisfaction Programming for the No-three-in-line Problem

TL;DR

This work solves the classical no-three-in-line problem on grids for all by formulating it as a constraint-satisfaction problem and employing a symmetry-reduced CP-SAT model. The authors exploit rotational symmetry to reduce the search space, enabling construction of -point configurations and proving for all , thereby shifting the unknown boundary to . They analyze solve-time behavior under a run-until-first-success parallel protocol and introduce a shifted-exponential model to describe early-time performance, providing practical extrapolations for planning large-scale runs. The work also documents data availability and suggests directions for further speedups and deeper structural insights to guide exact search in combinatorial geometry.

Abstract

Using a constraint satisfaction approach, we exhibit configurations of points on the grid for all with no three collinear. Consequently, the smallest for which it is unknown whether increases from to .
Paper Structure (18 sections, 1 theorem, 23 equations, 6 figures, 3 tables)

This paper contains 18 sections, 1 theorem, 23 equations, 6 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Results and formulations
  3. Satisfiability formulation
  4. Existence up to $n=60$
  5. Symmetry reduction
  6. Implementation and computational setup
  7. Hardware and software
  8. Constraint generation and deduplication
  9. Model sizes
  10. Parallel protocol and termination
  11. Solve times and scaling
  12. Baseline timings
  13. Empirical solve-time distributions and parallelism
  14. Data collection protocol.
  15. A shifted-exponential model
  16. ...and 3 more sections

Key Result

Theorem 1

For $2\le n\le60$ there exists a configuration in $\mathcal{F}_n$. In particular, $D(n)=2n$ for $2\le n\le60$.

Figures (6)

  • Figure 1: $2n$ lattice points with no three in line for $n=60$. The $120$ occupied sites (red) are shown together with the $\binom{120}{2}=7140$ straight-line segments joining each pair of occupied sites (blue), illustrating the $90^\circ$ rotational symmetry.
  • Figure 2: Wall-clock time (log scale) to the first solution in a single experiment consisting of $384$ independent CP-SAT runs executed in parallel on an AMD EPYC 9965 CPU. Red squares: direct model \ref{['CPSAT']} (no symmetry restriction). Blue circles: symmetry-reduced model \ref{['CPSATred']} enforcing rotational symmetry.
  • Figure 3: Empirical cumulative distribution function $F(t)$ of the time to success for a single CP-SAT run (blue), obtained from $10{,}436$ independent runs of \ref{['CPSATred']} at $n=34$. Also shown is the derived CDF $F_{384}(t)$ for the first success among $M=384$ parallel runs (orange), computed via \ref{['FM']}, and a shifted-exponential fit \ref{['expmodel']} to $F_{384}(t)$ near the origin (green). The inset magnifies the small-time region relevant for $F_{384}$.
  • Figure 4: For $n=44$: derived CDF $F_{384}(t)$ for the first success among $384$ parallel runs (orange) together with a shifted-exponential fit \ref{['expmodel']} (green). On this time window the empirical single-run CDF $F(t)$ is extremely small and is therefore not visually prominent.
  • Figure 5: Even sizes: semi-log plot of solve-time statistics versus grid size $n$. Blue circles: observed wall-clock times to first solution in single runs. Green triangles and cyan inverted triangles: estimated $50\%$ and $98\%$ completion times for $M=384$ parallel runs, derived from the shifted-exponential fit \ref{['expmodel']} via \ref{['meanquant']}. Solid lines: least-squares fits of $\log t$ versus $n$. The horizontal line indicates a ten-day wall-clock budget. Reported times over 10 days are aggregated from multiple job runs.
  • ...and 1 more figures

Theorems & Definitions (2)

  • Theorem 1
  • proof