[IEEE Trans. on Information Theory, vol. 68, no. 1, pp. 153-177, January 2022 ]

Hexagonal Run-Length Zero Capacity Region — Part II: Automated Proofs

Spencer Congero and Kenneth Zeger

Abstract

The zero capacity region for hexagonal (d,k) run-length constraints is known for many, but not all, d and k. The pairs (d,k) for which it has been unproven whether the capacity is zero or positive consist of:

(i) k=d+2 when d ≥ 2;
(ii) k=d+3 when d ≥ 1;
(iii) k=d+4 when either d=4 or d is odd and d ≥ 3;
(iv) k=d+5 when d=4.

Here, we prove the capacity is zero in case (i) when 2 ≤ d ≤ 9, in case (ii) when 3 ≤ d ≤ 11, and in case (iii) when d ∈ {4,5,7,9}. We also prove the capacity is positive in case (ii) when d ∈ {1,2}, in case (iii) when d = 3, and in case (iv). The zero capacities for k=d+4 are the first and only known cases equal to zero when k-d > 3. All of our results are obtained by developing three algorithms that automatically and rigorously assist in proving either the zero or positive capacity results by efficiently searching large numbers of configurations. The proofs involve either upper bounding the number of paths through certain large directed graphs, finding forbidden strings, or building distinct tileable square labelings. Some of the proofs examine over 20 billion cases using a supercomputer. In Part I of this two-part series, it is proven that the capacity is zero for all of case (i), and for case (ii) whenever d ≥ 7. Thus, the only remaining unknown cases are now when k=d+4, for any odd d ≥ 11.