[Model] Minesweeper

[QingyunQian]

Motivation

Add the Minesweeper Consistency problem, a classic NP-complete problem from recreational mathematics. This problem demonstrates that even simple puzzle games can encode hard computational problems, and each revealed cell is a linear constraint over binary variables — making it a natural source for reductions to SAT and ILP.

Definition

Name: Minesweeper
Reference:

• Kaye, R. (2000). "Minesweeper is NP-complete." The Mathematical Intelligencer, 22(2), 9–15.
• Kaye, R. — Minesweeper pages (proofs and gadgets)

Given a rectangular m × n grid of cells where:

• Some cells are revealed, each showing a number c ∈ {0, 1, ..., 8} indicating how many of its (up to 8) adjacent cells contain mines.
• The remaining cells are unrevealed and may or may not contain mines.

Determine whether there exists an assignment of mines to the unrevealed cells such that every revealed cell's count is satisfied.

Note: This is the consistency problem (decision version), distinct from the inference problem (determine whether a specific cell must be a mine in all valid assignments).

Variables

• Count: k (number of unrevealed cells)
• Per-variable domain: {0, 1} (0 = safe, 1 = mine)
• Meaning: xᵢ = 1 if unrevealed cell i contains a mine, 0 otherwise

Schema (data type)

Type name: Minesweeper
Variants: grid dimensions (rectangular grids of various sizes)

Field	Type	Description
rows	usize	Number of rows m
cols	usize	Number of columns n
revealed	Vec<(usize, usize, u8)>	Revealed cells: (row, col, mine_count)
unrevealed	Vec<(usize, usize)>	Unrevealed cell positions

Complexity

• Best known exact algorithm: O(2^k) by exhaustive search, where k is the number of unrevealed cells
• Complexity class: NP-complete
• References:
  • Kaye (2000) proves NP-completeness by constructing logic-gate gadgets (AND, OR, NOT, wire) as Minesweeper sub-grids, reducing from CircuitSAT.

Extra Remark

Relationship to other problems:

• SAT/CircuitSAT: Kaye's proof reduces CircuitSAT → Minesweeper (via gadget construction)
• ILP: Each revealed cell yields a linear equality over binary variables — Minesweeper is a special case of 0-1 ILP feasibility
• Constraint Satisfaction: Can be viewed as a CSP with sum constraints on overlapping neighborhoods

Implementation notes:

• Should implement SatisfactionProblem trait
• Each revealed cell generates a constraint: Σ(adjacent unrevealed cells) = count
• Revealed cells are never mines

How to solve

• It can be solved by bruteforce (enumerate all 2^k mine placements)
• It can be reduced to SAT (encode sum constraints as boolean cardinality constraints)
• It can be reduced to ILP (linear equality constraints over binary variables)

Example Instance

Instance 1: Simple 3×3 grid - YES

Grid (row, col from top-left):
  ? ? ?
  ? 1 ?
  ? ? ?

Revealed: [(1, 1, 1)]
Unrevealed: (0,0), (0,1), (0,2), (1,0), (1,2), (2,0), (2,1), (2,2)

Constraint: (1,1) has 8 unrevealed neighbors, exactly 1 must be a mine.

Answer: YES
Solution: Mine at (0,0), all others safe.
Verification:
  - (1,1): neighbors include (0,0)=mine, 7 others safe → count = 1 ✓

Instance 2: Contradictory constraints - NO

Grid:
  1 ? 1
  ? 0 ?
  1 ? 1

Revealed: (0,0,1), (0,2,1), (1,1,0), (2,0,1), (2,2,1)
Unrevealed: (0,1), (1,0), (1,2), (2,1)

Constraints:
  (1,1)=0: all unrevealed neighbors must be safe
    neighbors of (1,1): (0,0)r, (0,1)u, (0,2)r, (1,0)u, (1,2)u, (2,0)r, (2,1)u, (2,2)r
    → x₀₁ + x₁₀ + x₁₂ + x₂₁ = 0
    → x₀₁ = x₁₀ = x₁₂ = x₂₁ = 0

  (0,0)=1: needs 1 mine among unrevealed neighbors
    neighbors of (0,0): (0,1)u, (1,0)u, (1,1)r
    → x₀₁ + x₁₀ = 1

  But from (1,1)=0: x₀₁ = 0 and x₁₀ = 0, so x₀₁ + x₁₀ = 0 ≠ 1.

Answer: NO (contradiction between (1,1)=0 and (0,0)=1)

Instance 3: Classic Minesweeper pattern - YES

Grid:
  1 ? ?
  1 2 ?
  0 1 ?

Revealed: (0,0,1), (1,0,1), (1,1,2), (2,0,0), (2,1,1)
Unrevealed: (0,1), (0,2), (1,2), (2,2)

Constraints:
  (0,0)=1: unrevealed neighbors (0,1), (1,0)r → x₀₁ = 1
  (1,0)=1: unrevealed neighbors (0,1) → x₀₁ = 1
  (1,1)=2: unrevealed neighbors (0,1), (0,2), (1,2), (2,2) → x₀₁ + x₀₂ + x₁₂ + x₂₂ = 2
  (2,0)=0: no unrevealed neighbors → trivially satisfied
  (2,1)=1: unrevealed neighbors (1,2), (2,2) → x₁₂ + x₂₂ = 1

  From x₀₁=1 and (1,1): x₀₂ + x₁₂ + x₂₂ = 1
  Combined with x₁₂ + x₂₂ = 1: x₀₂ = 0

Answer: YES
Solution: Mines at (0,1) and (1,2), others safe.
Verification:
  - (0,0): (0,1)=mine → count = 1 ✓
  - (1,0): (0,1)=mine → count = 1 ✓
  - (1,1): (0,1)=mine, (1,2)=mine → count = 2 ✓
  - (2,0): no mine neighbors → count = 0 ✓
  - (2,1): (1,2)=mine → count = 1 ✓

Validation Method

• Cross-check with Minesweeper solvers (e.g., Simon Tatham's Mines solver)
• Verify on hand-crafted instances with known solutions
• Compare with SAT/ILP encodings of the same problem

Potential reductions:

• Minesweeper → SAT: Encode sum constraints as boolean cardinality constraints (CNF)
• Minesweeper → ILP: Each revealed cell becomes a linear equality over binary variables

[QingyunQian]

Low priority, I think, as I have other interesting models and rules.