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

[zazabap]

Issue Quality Check — Model

Check	Result	Details
Usefulness	✅ Pass	Novel problem, concrete reduction connections planned
Non-trivial	✅ Pass	Unique grid-based constraint satisfaction structure
Correctness	✅ Pass	All references verified
Well-written	✅ Pass	Thorough examples with step-by-step verification

Overall: 4 passed, 0 failed, 0 warnings

---

Usefulness

No Minesweeper model exists in the codebase. The motivation is sound — Minesweeper Consistency is a well-known NP-complete problem with natural reductions to SAT, ILP, and from CircuitSAT (Kaye's proof). These connect meaningfully to existing models.

Non-trivial

Genuinely distinct from all existing problems. The grid-based topology with neighbor-count constraints is a unique input structure. While related to ILP (linear equalities over binary variables), the grid neighborhood structure motivates specific encodings.

Correctness

Reference	Status	Notes
Kaye (2000), Math. Intelligencer 22(2), 9–15	✅ Verified	DOI 10.1007/BF03025367; proves NP-completeness via CircuitSAT reduction
Kaye's supplementary material (Birmingham)	✅ Verified	Academic resource with logic-gate gadget constructions

Complexity claim O(2^k) where k = unrevealed cells is correct as a naive upper bound. No tighter worst-case bound is established in the literature.

Well-written

All required sections present and substantive. Three examples provided:

1. Simple YES instance (3×3, single revealed cell)
2. NO instance with clear contradiction analysis
3. Complex YES instance with multi-constraint propagation

All include step-by-step constraint derivation — above average quality.

Minor suggestion: The unrevealed field in the schema could potentially be derived from rows, cols, and revealed, which would simplify the schema. Having it explicit allows partially-known boards though, so this is a design choice for implementation.

[zazabap]

@QingyunQian Apparently Claude has different opinion.

[QingyunQian]

@QingyunQian Apparently Claude has different opinion.

i will add some reduction rule for this model

[zazabap]

Issue Quality Check — Model

Check	Result	Details
Usefulness	✅ Pass	Novel problem not yet in reduction graph
Non-trivial	✅ Pass	Distinct input structure and feasibility constraints from all 24 existing problems
Correctness	✅ Pass	Kaye (2000) verified on Springer; NP-completeness claim and brute-force bound correct
Well-written	✅ Pass	All template sections present and substantive; three fully worked examples

Overall: 4 passed, 0 failed, 0 warnings

---

Usefulness

pred show Minesweeper confirms this problem does not exist in the codebase. The issue identifies concrete reduction targets (SAT, ILP) that would connect it to the existing reduction graph, so it would not be an orphan node. The constraint structure (linear equalities over binary variables from neighborhood counts) provides a natural bridge to multiple existing problems.

Non-trivial

Minesweeper has a unique input structure: a rectangular grid with revealed cells carrying neighborhood mine counts and unrevealed cells as binary decision variables. The feasibility constraints (each revealed cell imposes a sum constraint over its spatial neighborhood) are structurally distinct from all 24 existing problems. It is not a variant of any existing problem — the grid-based spatial neighborhood structure and per-cell cardinality constraints have no equivalent in the current models.

Correctness

• Kaye (2000): "Minesweeper is NP-complete," The Mathematical Intelligencer, 22(2), 9–15. Verified on Springer and Semantic Scholar. The paper proves NP-completeness via reduction from CircuitSAT using logic-gate gadgets embedded in Minesweeper grids, consistent with the issue's claims.
• Complexity bound: O(2^k) brute-force over k unrevealed cells is the correct trivial bound. No specialized exact algorithm with a better exponential base is known for general Minesweeper consistency, so this is appropriate.
• NP-completeness: Confirmed. The consistency problem (given partial information, does a valid mine assignment exist?) is the decision version proved NP-complete by Kaye.

Well-written

All required template sections are present and substantive:

• Motivation: Concrete and well-articulated — connects recreational mathematics to computational complexity, identifies natural reduction targets.
• Definition: Mathematically precise — grid dimensions, revealed cell format, feasibility condition all clearly specified.
• Variables: Properly defined with count, domain, and semantic meaning.
• Schema: Complete field table with types and descriptions.
• Complexity: Correct NP-completeness classification with proper citation.
• How to solve: Three solver paths identified (brute-force, SAT reduction, ILP reduction).
• Examples: Three fully worked instances (satisfiable, unsatisfiable with contradiction proof, and a more complex satisfiable case). Each shows the grid, constraints, step-by-step reasoning, and verification. Excellent quality — non-trivial and hand-verifiable.

Symbol usage is consistent: m, n for grid dimensions match rows, cols in the schema; k for unrevealed cell count is used consistently; constraint notation is clear throughout.

Recommendations

• Consider specifying the getter methods / size_fields the problem type will expose (e.g., num_rows(), num_cols(), num_unrevealed(), num_revealed()) — these will be needed for overhead expressions in future reduction rules.
• The SatisfactionProblem trait choice is correct for a consistency/decision problem.