Can I sweep the mines? Minesweeper is a popular puzzle game where you must discover which tiles are &quot;mines&quot; without clicking on those tiles. Instead, you click on nearby tiles to reveal the number of adjacent mines. One downside about the game is that it is possible to end up in a scenario where there are multiple valid answers and you may only guess. For example, take the following board:
1110
2*31
3*??
2*4?
112?

In this format, a number represents the number of adjacent mines, an * represents a known mine, and a &quot;?&quot; represents a potential mine. The unfortunate thing about this particular puzzle is that there are four distinct and valid potential solutions:
1110    1110    1110    1110    
2*31    2*31    2*31    2*31
3*4*    3*5*    3**2    3**1
2*42    2*4*    2*4*    2*42
112*    1121    1121    112*

This means the board is unsolvable. Here is an example of a solvable board:
1121
1??*
12?*
0122

This board is solvable because there is only one possible valid solution:
1121
1*4*
12**
0122

Your task is to write either a program or function that takes a valid minesweeper board and determines if it is solvable or not. By &quot;valid minesweeper board&quot;, I mean that the input will always be rectangular, have at least one solution, and not contain any invalid characters.
Your input may be an array of characters, an array of strings, a string containing newlines, etc. The output must be a truthy value if it is solvable and a falsy value if it is not. I am not extremely worried about performance, but your solution must theoretically work for any size input.
As usual, standard loopholes apply and the shortest solution in bytes wins!
Examples:
The following examples are all solvable:
1121
1??*
12?*
0122

1110
1???
1110
0000

1110
3???
??20
*310

****
****
****
****

0000
0000
0000
0000

1100
*100
2321
??*2
13*2
1221
1*10
1110

1121
2*??
2*31
2220
1*10

The following examples are all unsolvable:
1110
2*31
3*??
2*4?
112?

01??11*211
12??2323*1
1*33*2*210
12?2122321
13?3101**1
1***101221

1***
3*52
2*31
12??
02??
01??

00000111
000012*1
00001*21
22101110
**100111
?31123*1
?311**31
**113*20
GNU Prolog, 493 bytes



z(_,[_,_]).
z(F,[A,B,C|T]):-call(F,A,B,C),z(F,[B,C|T]).
i([],[],[],[]).
i([H|A],[I|B],[J|C],[H-I-J|T]):-i(A,B,C,T).
c(A/_-B/_-C/_,D/_-_/T-E/_,F/_-G/_-H/_):-T#=A+B+C+D+E+F+G+H.
r(A,B,C):-i(A,B,C,L),z(c,L).
q(63,V):-var(V).
q(42,1/_).
q(X,0/Y):-Y#=X-48.
l([],[0/_]).
l([H|T],[E|U]):-q(H,E),l(T,U).
p([],[[0/_,0/_]],0).
p([],[[0/_|T]],N):-M#=N-1,p([],[T],M).
p([H|T],[[0/_|E]|U],N):-p(T,U,N),l(H,E).
m([H|A],B):-length(H,N),p([],[R],N),p([H|A],M,N),z(r,[R|M]),p(B,M,N).
s(A):-setof(B,m(A,B),[_]).


An extra predicate that may be useful for testing (not part of the submission):

d([]).
d([H|T]):-format("~s~n",[H]),d(T).


Prolog's definitely the right language for solving this task from the practical point of view. This program pretty much just states the rules of Minesweeper and lets GNU Prolog's constraint solver solve the problem from there.

z and i are utility functions (z does a sort of fold-like operation but on sets of three adjacent elements rather than 2; i transposes 3 lists of n elements into a list of n 3-tuples). We internally store a cell as x/y, where x is 1 for a mine and 0 for a nonmine, and y is the number of adjacent mines; c expresses this constraint on the board. r applies c to every row of the board; and so z(r,M) checks to see if M is a valid board.

Unfortunately, the input format required to make this work directly is unreasonable, so I also had to include a parser (which probably accounts for more code than the actual rules engine, and most of the time spent debugging; the Minesweeper rules engine pretty much worked first time, but the parser was full of thinkos). q converts a single cell between a character code and our x/y format. l converts one line of the board (leaving one cell that's known to be not a mine, but with an unknown number of neighbouring mines, at each edge of the line as a border); p converts the entire board (including the bottom border, but excluding the top one). All of these functions can be run either forwards or backwards, thus can both parse and pretty-print the board. (There's some annoying wiggling around with the third argument to p, which specifies the width of the board; this is because Prolog doesn't have a matrix type, and if I don't constrain the board to be rectangular, the program will go into an infinite loop trying progressively wider borders around the board.)

m is the main Minesweeper solving function. It parses the input string, generating a board with a correct border (via using the recursive case of p to convert most of the board, then calling the base case directly to generate the top border, which has the same structure as the bottom border). Then it calls z(r,[R|M]) to run the Minesweeper rules engine, which (with this call pattern) becomes a generator generating only valid boards. At this point, the board is still expressed as a set of constraints, which is potentially awkward for us; we could perhaps have a single set of constraints which could represent more than one board. Additionally, we haven't yet specified anywhere that each square contains at most one mine. As such, we need to explicitly "collapse the waveform" of each square, requiring it to be specifically either a (single) mine or a nonmine, and the easiest way to do this is to run it through the parser backwards (the var(V) on the q(63,V) case is designed to prevent the ? case running backwards, and thus deparsing the board forces it to be fully known). Finally, we return the parsed board from m; m thus becomes a generator which takes a partially unknown board and generates all the known boards consistent with it.

That's really enough to solve Minesweeper, but the question explicitly asks to check whether there's exactly one solution, rather than to find all solutions. As such, I wrote an extra predicate s which simply converts the generator m into a set, and then asserts that the set has exactly one element. This means that s will return truthy (yes) if there is indeed exactly one solution, or falsey (no) if there is more than one or less than one.

d is not part of the solution, and not included in the bytecount; it's a function for printing a list of strings as though it were a matrix, which makes it possible to inspect the boards generated by m (by default, GNU Prolog prints strings as a list of ASCII codes, because it treats the two synonymously; this format is fairly hard to read). It's useful during testing, or if you want to use m as a practical Minesweeper solver (because it uses a constraint solver, it's highly efficient).