[amluto]

You can turn this around; why implement complicated cardinality constraints to reduce a problem to SAT when a different solver can handle them directly.

I think it’s a shame that there is a general lack of high-quality open source IP/MIP solvers. Formulating Minesweeper as an integer program is trivial. SMT solvers might work well, too.

There’s another twist. The right thing to do here is probably to divide the board into connected components (where two squares have an edge if they have a common neighbor), then solve each component with no constraints on the number of mines, and then to match up the solutions. This would improve the game, since the concept of “a guess is needed” could take into account that revealing more numbers might not help solve a given component.