[amluto]

Why a SAT solver? Constraint propagation with backtracking and arc consistency checks is very fast for minesweeper (source: this was an old Stanford CS homework problem), and it’s fairly straightforward to re-solve with added constraints to ask questions like “could there be a mine here”.

In general, the Kaboom game logic seems to be nearly identical to writing an optimal minesweeper solver.

[lalaland1125]

Why implement backtracking when a SAT solver implements it for you?

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