[Rule] Minesweeper to ILP

[QingyunQian]

Source: Minesweeper
Target: ILP (binary)
Motivation: Minesweeper constraints are naturally linear equalities over binary variables, making ILP the most direct formulation. This enables solving Minesweeper via standard ILP solvers (branch-and-bound, cutting planes).
Reference:

• Kaye, R. (2000). "Minesweeper is NP-complete." Mathematical Intelligencer, 22(2), 9–15.

Reduction Algorithm

Notation:

• Source: a Minesweeper instance with an m × n grid, a set R of revealed cells, and a set U of unrevealed cells with |U| = k.
  • Each revealed cell r ∈ R has position (rᵣ, cᵣ) and mine count cntᵣ ∈ {0, ..., 8}.
  • N(r) = {u ∈ U : u is 8-connected neighbor of r} denotes the unrevealed neighbors of r.
• Target: an ILP instance with k binary variables, |R| equality constraints, and a trivial objective.

Variable mapping:

Each unrevealed cell uᵢ ∈ U (for i = 0, ..., k−1) maps to a binary ILP variable xᵢ ∈ {0, 1}, where xᵢ = 1 means cell uᵢ contains a mine and xᵢ = 0 means it is safe.

Constraint transformation:

For each revealed cell r ∈ R with mine count cntᵣ and unrevealed neighbor set N(r):

$$\sum_{u_i \in N(r)} x_i = \text{cnt}_r$$

This is a single linear equality constraint per revealed cell.

Objective:

Trivial: minimize 0 (empty objective vector). Any feasible solution to the ILP is a valid mine assignment. Since Minesweeper is a satisfaction problem, we only need feasibility.

Correctness:

A mine assignment satisfies all Minesweeper constraints if and only if the corresponding binary vector satisfies all ILP equality constraints. The mapping is bijective — no auxiliary variables are introduced.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_vars	k = |U| (one per unrevealed cell)
num_constraints	|R| (one equality per revealed cell)

The reduction is linear in the input size. No auxiliary variables or constraints are needed.

Validation Method

• Closed-loop testing: for small instances, brute-force solve both the Minesweeper instance and the ILP, verify solution sets match.
• Cross-check with SAT encoding: reduce the same Minesweeper instance to both ILP and SAT, verify they agree on satisfiability.
• Hand-verify on the example instances from the Minesweeper model issue.

Example

Source Minesweeper instance (3×3 grid, Instance 3 from model issue):

Grid:
  1 ? ?
  1 2 ?
  0 1 ?

rows = 3, cols = 3
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)]

Variables: x₀ = (0,1), x₁ = (0,2), x₂ = (1,2), x₃ = (2,2)

Target ILP instance:

4 binary variables, 5 equality constraints:

Constraint from (0,0)=1:  neighbors in U = {(0,1)} → x₀ = 1
Constraint from (1,0)=1:  neighbors in U = {(0,1)} → x₀ = 1
Constraint from (1,1)=2:  neighbors in U = {(0,1),(0,2),(1,2),(2,2)} → x₀ + x₁ + x₂ + x₃ = 2
Constraint from (2,0)=0:  neighbors in U = {} → (trivially satisfied, 0 = 0)
Constraint from (2,1)=1:  neighbors in U = {(1,2),(2,2)} → x₂ + x₃ = 1

Solution:

From x₀ = 1 and x₀ + x₁ + x₂ + x₃ = 2: x₁ + x₂ + x₃ = 1.
Combined with x₂ + x₃ = 1: x₁ = 0.
Two feasible solutions: (1, 0, 1, 0) and (1, 0, 0, 1).

Verification for (1, 0, 1, 0) → mines at (0,1) and (1,2):

• (0,0)=1: neighbor (0,1) is mine → count = 1 ✓
• (1,0)=1: neighbor (0,1) is mine → count = 1 ✓
• (1,1)=2: neighbors (0,1) and (1,2) are mines → count = 2 ✓
• (2,0)=0: no mine neighbors → count = 0 ✓
• (2,1)=1: neighbor (1,2) is mine → count = 1 ✓