My students claim that this disconnect four puzzle (fill the grid with crosses and zeros, such that no four equal symbols appear in a row. Rows can be horizontal, vertical, or diagonal) does not have a unique solution, as it should.

What is the fewest crosses and/or zeros must I add so that it does have a unique solution?

• Is it intended that the image is transparent in three particular locations?
– Deusovi
Sep 29, 2021 at 20:29
• @Deusovi No, I will try and fix it! Ignore it for the time being. Sep 29, 2021 at 20:33
• @Deusovi Fixed, I hope. Sep 29, 2021 at 20:39
• I casebashed at this for a while and couldn't get anywhere - is there an intended 'nice' path to the solution?
– Deusovi
Sep 30, 2021 at 0:01
• @Deusovi Bubbler seems to have found something nice (at least to my standard) Sep 30, 2021 at 9:41

at most 4, likely exact.

Trying to solve the puzzle from scratch doesn't give us much:

However, case analysis on

R6C3

gives very interesting results.

(Edit: I now see that R10C4 is X and R10C1 is O on the first board, but it doesn't change the general conclusion.)

Note that

The 2nd board has exactly three cells empty which can be filled independently. The 1st has more freedom: R8C3 is clearly independent from the other cells, and the same applies to R8C9; at least one more cell needs to be constrained in order to have a unique solution.

Since we already forced a cell by case analysis, the total number of cells we need to force to get a unique solution is

1 + 3 = 4.

• I have proved the minimum - see my answer. Sep 30, 2021 at 10:23

Converting a Disconnect Four puzzle to a SAT instance is very easy.

Set X as 1 and O as 0 and label the unknown cells like this:

The CNF has 197 clauses representing each possible line of four not already containing an X and an O; the "no 4 Xs (Os) in a row" condition is represented by negative (positive) literals. The CNF-generating code is in findsols.py here.

Based on this

I found exactly 8408 solutions, and manual inspection showed that all but eight set slot 1 to O. Those eight solutions differ only in slots 6, 20 and 40, so there is a four-clue uniquisation. To show that there is no uniquisation with fewer clues is as easy as looping over all possible assignments of three extra clues and showing that none of them give a unique solution – after proving this I considered all assignments yielding eight solutions and showed that they all leave the same three free squares 6, 20 and 40, and that the eight solutions are the same in every case. The latter analysis is analyse.py in the gist above.

The assignments appearing in all 8408 solutions are$$3X, 10X, 16X, 17O, 18X, 19O, 22X, 24O, 28O, 30X, 33X, 35O, 37O$$The assignments leaving eight solutions are$$1O, 2X, 7O, 8O, 9X, 14O, 15X, 21X, 23X, 25O, 27O, 29X, 31X, 34O, 36X, 38O, 39X, 41X, 42X, 43O, 44O, 45O, 46X, 48X, 49O, 51O, 52X, 53O, 54X, 57X, 58O$$In the diagram below the first set of assignments (forced) is fuchsia, the second set (leaving eight solutions) is lime and the assignments forced by any one of the lime assignments are light grey.

This concludes the proof that four is the minimum of extra clues needed to get a unique solution.