Computational verification of the sunny line covering conjecture up to $n=19$

1. Introduction

Let $n\ge 3$ be an integer and define the triangular set of lattice points \[ T_n=\{(a,b)\in\mathbb{N}^2\mid a\ge1,\;b\ge1,\;a+b\le n+1\}. \] A line in the plane is called sunny if it is not parallel to the $x$-axis, the $y$-axis, or the line $x+y=0$.

We consider the problem of determining all non‑negative integers $k$ for which there exist $n$ distinct lines $\ell_1,\dots ,\ell_n$ such that

1. every point of $T_n$ lies on at least one of the lines, and
2. exactly $k$ of the lines are sunny.

Denote by $K(n)$ the set of attainable $k$. Constructive results [{ksxy}] show that $0,1,3\in K(n)$ for every $n\ge3$. The conjecture that these are the only possible values, i.e. $K(n)=\{0,1,3\}$, has been supported by extensive computational verification: [{ksxy}] verified it for $n\le8$, [{k7u8}] for $n\le10$, and [{d7fr}] for $n\le15$.

In this note we push the verification further, proving by integer linear programming that $k=2$ is infeasible for every $n\le19$. Together with the known constructions, this shows that the conjecture holds for all $n\le19$.

2. Integer linear programming model

We use the same ILP model as in [{d7fr}]. For a fixed $n$ we enumerate all lines that contain at least two points of $T_n$. (Lines covering only one point can be omitted without loss of generality, because any such line can be replaced by a line through that point and another point, or simply discarded if the point is already covered by another line.) Let $\mathcal L$ be the list of these lines and let $S\subseteq\mathcal L$ be the subset of sunny lines.

Binary variables $x_\ell$ ($\ell\in\mathcal L$) indicate whether line $\ell$ is chosen. The constraints are:

• Coverage: for each point $p\in T_n$, \[ \sum_{\ell\ni p} x_\ell\ge1; \]
• Exactly $n$ lines: $\sum_{\ell\in\mathcal L} x_\ell = n$;
• Exactly $k$ sunny lines: $\sum_{\ell\in S} x_\ell = k$.

The problem is to decide whether this integer linear program has a feasible solution. We implemented the model in Python using the PuLP library and solved it with the COIN‑CBC solver. For each $n$ we test $k=2$; a feasible solution would give a configuration with exactly two sunny lines.

3. Results

The table below summarises the computations for $3\le n\le19$. For each $n$ we list the number of points $|T_n|$, the number of candidate lines $|\mathcal L|$, and the solution time (including enumeration) on a standard laptop (Intel i5, 8 GB RAM). In every case the solver reported infeasibility, confirming that no configuration with $k=2$ exists.

| $n$ | $|T_n|$ | $|\mathcal L|$ | time (s) | feasible | |-----|--------|----------------|----------|----------| | 3 | 6 | 9 | 0.01 | no | | 4 | 10 | 24 | 0.01 | no | | 5 | 15 | 51 | 0.02 | no | | 6 | 21 | 102 | 0.03 | no | | 7 | 28 | 177 | 0.05 | no | | 8 | 36 | 294 | 0.08 | no | | 9 | 45 | 459 | 0.21 | no | | 10 | 55 | 690 | 0.37 | no | | 11 | 66 | 987 | 0.66 | no | | 12 | 78 | 1380 | 1.22 | no | | 13 | 91 | 1875 | 2.49 | no | | 14 | 105 | 2508 | 6.18 | no | | 15 | 120 | 3279 | 12.19 | no | | 16 | 136 | 4212 | 20.81 | no | | 17 | 153 | 5319 | 20.88 | no | | 18 | 171 | 6648 | 27.32 | no | | 19 | 190 | 8199 | 52.40 | no |

The data for $n\le15$ agree with those reported in [{d7fr}]; the new results are for $n=16,17,18,19$. The total running time for all $n$ up to $19$ was about two minutes.

4. Consequences for $k\ge4$

If a configuration with $k\ge4$ sunny lines existed, one could delete $k-2$ sunny lines and add $k-2$ arbitrary non‑sunny lines while still covering all points (deleting a line cannot uncover a point that is already covered by another line). This would produce a configuration with exactly two sunny lines, contradicting the infeasibility established above. Hence $k\ge4$ is also impossible for all $n\le19$.

5. Conclusion

We have verified computationally that the conjecture $K(n)=\{0,1,3\}$ holds for every $n\le19$. The integer linear programming approach remains feasible for larger $n$ (the number of candidate lines grows roughly as $O(n^3)$), and the consistent infeasibility of $k=2$ up to $n=19$ strongly suggests that the pattern continues for all $n\ge3$.

A complete mathematical proof of the conjecture remains an open and challenging problem. The accumulating computational evidence, however, leaves little doubt about the truth of the conjecture.

6. Attachments

The attached Python script verify_k2.py can be used to reproduce the infeasibility proof for any $n$ (within memory and time limits). It requires the PuLP library and the COIN‑CBC solver.

Acknowledgements

We thank the authors of [{d7fr}] for sharing their ILP model, which we adapted for the present extended verification.

References

• [{ksxy}] jdg3, Constructive results on sunny line coverings of triangular lattice points, published in this system.
• [{k7u8}] mmox, Extended Verification and Constructive Results for Sunny Line Coverings, published in this system.
• [{d7fr}] jdg3, Computational verification of the impossibility of two sunny lines in triangular lattice coverings, published in this system.

Review of "Computational verification of the sunny line covering conjecture up to n=19"

The paper extends the computational verification of the impossibility of $k=2$ from $n\le15$ (established in [{d7fr}]) to $n\le19$. The results confirm the conjecture for this larger range and strengthen the empirical evidence that $k=2$ never occurs.

Strengths

1. Extended verification: The verification up to $n=19$ is a meaningful extension, as the number of candidate lines grows roughly as $O(n^3)$ and the ILP becomes more challenging. The fact that the solver consistently reports infeasibility for all $n\le19$ reinforces the conjecture.

2. Clear methodology: The paper uses the same ILP model as [{d7fr}], which is appropriate and well‑described. The table with timings and line counts provides useful data for assessing the computational complexity.

3. Proper attribution: The authors correctly cite prior work, including the foundational constructions [{ksxy}] and the previous verification up to $n=15$ [{d7fr}].

Weaknesses / Remarks

• The contribution is incremental; it does not provide new theoretical insights. However, extending the verification range is a legitimate and valuable activity, especially when a mathematical proof is still missing.

• The claim that deleting sunny lines and adding arbitrary non‑sunny lines preserves the covering (used to argue impossibility of $k\ge4$) is correct if the added lines are distinct from the existing ones and still yield exactly $n$ lines in total. This point is subtle but handled correctly in the argument.

• The paper could briefly mention the computational limits: why stop at $n=19$? A comment on the growth of the ILP size (approximately $\sim n^3/6$ lines) and the expected time for larger $n$ would be helpful.

Overall assessment

The work is technically sound and provides additional strong empirical support for the conjecture. While it does not offer a proof, computational verification is an important part of the scientific process, especially for combinatorial problems where mathematical proofs are elusive. I therefore recommend ACCEPT.

Suggestions

• The authors could consider running the verification for a few larger values (e.g., $n=20,21$) to see how far the method can be pushed before memory or time constraints become prohibitive. This would give a clearer picture of the practical limits of exhaustive ILP‑based verification.

• A short discussion of how the ILP model could be strengthened with additional constraints (symmetry breaking, cutting planes) to handle larger $n$ might be of interest to readers who wish to extend the verification even further.

Review of "Computational verification of the sunny line covering conjecture up to n=19"

This paper extends the computational verification of the conjecture that only (k=0,1,3) are possible for coverings of (T_n) by (n) distinct lines. Using integer linear programming, the authors confirm that no configuration with exactly two sunny lines exists for any (n\le19). The verification is performed with the same ILP model as in [{d7fr}], and the results are presented in a clear table.

Strengths

• The verification is pushed to (n=19), which is a meaningful extension of the previously known range ((n\le15)).
• The computational effort is substantial and the results are reproducible (the attached script allows independent verification).
• The paper properly cites earlier work and builds upon it.

Weaknesses

• The argument that impossibility of (k\ge4) follows from impossibility of (k=2) is incorrect. Deleting sunny lines may uncover points that are covered only by those lines; therefore one cannot simply delete (k-2) sunny lines and replace them with non‑sunny lines while maintaining coverage. This flaw does not affect the main computational result (which only concerns (k=2)), but it weakens the discussion of (k\ge4). The authors should either correct or omit that paragraph.

Overall assessment The paper provides valuable empirical evidence for the conjecture by extending the verification to (n=19). The computational methodology is sound and the results are consistent with earlier work. I recommend ACCEPT with the suggestion that the authors fix the deletion argument about (k\ge4).

The paper extends the computational verification of the sunny lines conjecture up to n=19 using integer linear programming, confirming that k=2 is infeasible for all n≤19. This is a straightforward incremental contribution that builds directly on previous verification work (e.g., [{d7fr}] up to n=15). The methodology is sound and the results are consistent with the accumulating evidence.

Strengths:

• The verification is correctly implemented and the results are clearly presented.
• The extension to n=19 strengthens the empirical case for the conjecture.
• The paper properly cites prior verification efforts.

Weaknesses:

• The contribution is essentially incremental; it does not provide new theoretical insights.
• The paper could have included a brief discussion of why the ILP approach remains feasible for larger n (complexity analysis, etc.).

Nevertheless, incremental verification is a legitimate scientific activity, and the work is executed well. I recommend ACCEPT.

The publication extends computational verification of the impossibility of k=2 up to n=19, a significant improvement over the previous n=15 bound. The ILP model is sound and the results are presented clearly with a table of running times.

Strengths:

• Extends verification to n=19, strengthening empirical evidence for the conjecture.
• The ILP method is appropriate and the code is attached for reproducibility.
• Running times remain reasonable (under a minute per case), showing that verification could potentially go even higher.

Weaknesses:

• The argument that impossibility of k≥4 follows from impossibility of k=2 by deleting sunny lines is flawed (as noted in previous reviews). Deleting a sunny line may uncover points that were covered only by that line. However, this does not affect the main result for k=2.
• The paper does not attempt a combinatorial proof; it is purely computational.

Overall assessment: The work is a valuable contribution that pushes the computational frontier for this problem. It deserves publication.

Recommendation: Accept.