[Rule] Minesweeper to Satisfiability

[QingyunQian]

Source: Minesweeper
Target: Satisfiability
Motivation: Encodes Minesweeper constraints as CNF cardinality constraints, enabling the use of highly optimized SAT solvers (CDCL, DPLL) for Minesweeper consistency checking. Since each cell has at most 8 neighbors, the combinatorial encoding produces a manageable number of clauses without auxiliary variables.
Reference:

• Kaye, R. (2000). "Minesweeper is NP-complete." Mathematical Intelligencer, 22(2), 9–15.
• The cardinality-to-CNF encoding is standard; see e.g. Bailleux & Boufkhad (2003). "Efficient CNF Encoding of Boolean Cardinality Constraints." CP 2003, LNCS 2833, 108–122.

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}, with |N(r)| = dᵣ.
• Target: a SAT instance in CNF with k Boolean variables and a set of clauses.

Variable mapping:

Each unrevealed cell uᵢ ∈ U (for i = 0, ..., k−1) maps to a SAT variable xᵢ₊₁ (1-indexed). xᵢ₊₁ = true means cell uᵢ contains a mine.

Constraint transformation:

For each revealed cell r with mine count c = cntᵣ and neighbor variables {y₁, ..., y_d} (where d = dᵣ), encode "exactly c of {y₁, ..., y_d} are true" as CNF using the combinatorial (binomial) encoding:

1. At-most-c constraint: For every (c+1)-element subset S ⊆ {y₁, ..., y_d}, add the clause (¬y_{s₁} ∨ ¬y_{s₂} ∨ ... ∨ ¬y_{s_{c+1}}). This produces C(d, c+1) clauses. Intuition: if c+1 variables were all true, that would exceed the count.

2. At-least-c constraint: For every (d−c+1)-element subset S ⊆ {y₁, ..., y_d}, add the clause (y_{s₁} ∨ y_{s₂} ∨ ... ∨ y_{s_{d−c+1}}). This produces C(d, d−c+1) = C(d, c−1) clauses. Intuition: if d−c+1 variables were all false, fewer than c would be true.

Special cases:

• c = 0: only at-most-0 clauses → d unit clauses (¬yⱼ) for each neighbor. No at-least clauses needed.
• c = d: only at-least-d clauses → d unit clauses (yⱼ) for each neighbor. No at-most clauses needed.
• N(r) = ∅: no clauses generated (constraint is trivially satisfied if c = 0, or the instance is infeasible if c > 0, but this is caught by the model's validation).

Clause count per constraint:

Since d ≤ 8 in Minesweeper, the worst case is d = 8, c = 4: C(8,5) + C(8,5) = 56 + 56 = 112 clauses. Total clauses ≤ 112 × |R|.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_vars	k = |U| (one per unrevealed cell, no auxiliary variables)
num_clauses	≤ 112 × |R| (worst case: 8 neighbors, count 4)

No auxiliary variables are introduced. The clause count is polynomial (in fact bounded by a constant times |R| since d ≤ 8).

Validation Method

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

Example

Source Minesweeper instance (3×3 grid):

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 (1-indexed for SAT): x₁ = (0,1), x₂ = (0,2), x₃ = (1,2), x₄ = (2,2)

Target SAT instance (CNF clauses):

From (0,0)=1, neighbors in U = {x₁}, d=1, c=1:

• at-most-1: no (c+1=2)-subsets of size > d=1 → no clauses
• at-least-1: C(1,1) = 1 clause → (x₁)

From (1,0)=1, neighbors in U = {x₁}, d=1, c=1:

• at-least-1: (x₁)

From (1,1)=2, neighbors in U = {x₁, x₂, x₃, x₄}, d=4, c=2:

• at-most-2: C(4,3) = 4 clauses:
  (¬x₁ ∨ ¬x₂ ∨ ¬x₃), (¬x₁ ∨ ¬x₂ ∨ ¬x₄), (¬x₁ ∨ ¬x₃ ∨ ¬x₄), (¬x₂ ∨ ¬x₃ ∨ ¬x₄)
• at-least-2: C(4,3) = 4 clauses:
  (x₁ ∨ x₂ ∨ x₃), (x₁ ∨ x₂ ∨ x₄), (x₁ ∨ x₃ ∨ x₄), (x₂ ∨ x₃ ∨ x₄)

From (2,0)=0, neighbors in U = {} → no clauses (trivially satisfied)

From (2,1)=1, neighbors in U = {x₃, x₄}, d=2, c=1:

• at-most-1: C(2,2) = 1 clause: (¬x₃ ∨ ¬x₄)
• at-least-1: C(2,2) = 1 clause: (x₃ ∨ x₄)

Total: 12 clauses over 4 variables.

Solution:

x₁ = true (forced by unit clause). From at-most-2 and at-least-2 on (1,1): exactly one of {x₂, x₃, x₄} is true. Combined with (x₃ ∨ x₄) and (¬x₃ ∨ ¬x₄): exactly one of {x₃, x₄} is true, so x₂ = false.

Satisfying assignments: {x₁=T, x₂=F, x₃=T, x₄=F} and {x₁=T, x₂=F, x₃=F, x₄=T}.

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

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