Comment by OscarCunningham

Yeah, it's NP-complete to decide whether a cell in Minesweeper must be a mine: https://logic.pku.edu.cn/ann_attachments/np.pdf.

In practice I suspect a SAT solver would make quick work of the positions that actually appear in games.