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).
2?has no solutions, which means it cannot come from an actual game of Minesweeper. Hence it is not considered a "Minesweeper board"...yes?) \$\endgroup\$