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
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.