[Rule] CircuitSAT to Minesweeper

[QingyunQian]

Source: CircuitSAT
Target: Minesweeper
Motivation: This is the canonical NP-completeness proof for Minesweeper. By reducing CircuitSAT to Minesweeper via logic-gate gadgets embedded in the grid, it establishes that Minesweeper Consistency is NP-complete. The improved templates from Thieme & Basten (2022) yield much more compact constructions than Kaye's originals.
Reference:

• Kaye, R. (2000). "Minesweeper is NP-complete." Mathematical Intelligencer, 22(2), 9–15.
• Thieme, A. & Basten, T. (2022). "Minesweeper is Difficult Indeed!" LNCS 13560, 472–490.

Reduction Algorithm

Notation:

• Source: a Boolean circuit C with n input variables x₀, ..., x_{n−1}, g gates (AND, OR, NOT), w wires, and a single output constrained to true.
• Target: a Minesweeper instance on an M × N grid.
• Convention: mine = logic 1, safe square = logic 0.

Step 1: Convert circuit to OR-only form

Apply De Morgan's law to eliminate AND gates: x₀ · x₁ = (x₀' + x₁')'. After transformation, the circuit contains only OR gates; negation is absorbed into the wiring (inverting wires). This halves the gate types needed.

Step 2: Build NOT gate gadget (3×3)

The NOT gate is the fundamental building block. Layout (⚑ = predefined mine, # = covered/unrevealed, number = revealed safe cell showing that count):

  col0  col1  col2
row0:  ⚑     3     ⚑
row1:  #in   5     #out
row2:  ⚑     3     ⚑

• 4 predefined mines at corners: (0,0), (0,2), (2,0), (2,2).
• 2 covered cells: #in at (1,0) and #out at (1,2).
• 3 revealed safe cells at (0,1), (1,1), (2,1) showing counts 3, 5, 3.
• Exactly 1 of the 2 covered cells is a mine (total covered mines = 1).
• Constraint: #in + #out = 1, i.e., #out = NOT(#in).

Step 3: Build OR gate gadget (from Thieme & Basten, 4×5 core)

The OR gate uses a 3×3 kernel with an uncovered "3" at center, 2 predefined mines and 2 safe squares in the corners, and 4 covered cells. The kernel ensures exactly 1 of the 4 covered cells is a mine. Inputs and output are connected via NOT-pattern triplets. The full OR gate template (for synthesis) is 7 columns wide with 29 predefined mines and 3 covered mines.

Step 4: Build wiring gadgets

• Wire: Even number of concatenated NOT gates → signal preserved. Each NOT segment is 3×3 with 4 predefined + 1 covered mine.
• Inverting wire: Odd number of NOT gates → signal negated.
• Split (6×6): Duplicates a signal for fan-out. 16 predefined mines, 1 or 4 covered mines (paired splits always total 5 covered mines).
• Crossing (6×6): Two wires cross without interference. 16 predefined mines, 3 covered mines.

Step 5: Assemble the circuit

1. Represent the circuit as a binary tree (each OR gate has 2 inputs).
2. Build a literal layer from left: one vertical wire per variable using crossings (6×6 each), with splits to produce literals. Width = 6n + 12 + 6 = 18 + 6n.
3. Build gate layers from left to right: each OR gate or wire-gate template is 7 columns wide.
4. Connect gate layers with wiring layers (10 columns wide): inversion sublayer + displacement sublayer.
5. Add a final inverter (3 columns) to ensure predetermined mine count.
6. Fill all remaining grid cells as revealed safe squares with counts derived from neighboring mines.
7. Constrain the output cell to be a mine (circuit output = true).

Step 6: Correctness

A Boolean valuation satisfies the circuit if and only if the corresponding mine assignment (mine = 1, safe = 0) on covered cells satisfies all revealed cell count constraints. The mapping is bijective on the input variables; internal gate outputs are determined by the gadget constraints.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
rows	3 + 6 * l, where l = number of literal occurrences in the circuit
cols	11 + 6 * num_variables + 17 * h, where h = number of gate layers in the tree representation
num_unrevealed	2 * l + 3 * g_or + 2 * g_wire + 2 * w_norm + 2 * w_inv + 3 * c + s_covered, where g_or = OR gates, g_wire = wire gates, w_norm/w_inv = normal/inverting wires, c = crossings, s_covered = covered cells in splits
num_revealed	rows × cols − num_unrevealed − num_predefined_mines

The total grid area is (3 + 6 * l) × (11 + 6 * num_variables + 17 * h), polynomial in the circuit size.

Validation Method

• For single-gate circuits (NOT, OR), construct the Minesweeper gadget and enumerate all valid mine assignments; verify they match the gate's truth table.
• For the NOT gate: verify the 3×3 gadget has exactly 2 consistent mine assignments corresponding to (in=1, out=0) and (in=0, out=1).
• Cross-reference gadget layouts with Thieme & Basten (2022) Figures 1–2 and Kaye (2000).

Example

Source CircuitSAT instance:

Circuit: out = NOT(x)
  - 1 input variable: x
  - 1 NOT gate
  - Output "out" constrained to true
Satisfying assignment: x = 0 (so NOT(x) = 1 = true)

Target Minesweeper instance (NOT gate gadget, 3×3):

Legend:  ⚑ = predefined mine (flagged)
        # = covered (unrevealed) cell
        n = revealed safe cell showing count n

Grid (3 rows × 3 cols):

        col0   col1   col2
  row0:  ⚑      3      ⚑
  row1:  #x     5      #out
  row2:  ⚑      3      ⚑

Revealed: [(0,1, 3), (1,1, 5), (2,1, 3)]
  plus 4 flagged mines: (0,0), (0,2), (2,0), (2,2)
Unrevealed: [(1,0), (1,2)]

Constraint verification:

Cell (0,1) shows 3: its 8-neighbors are (0,0)=⚑, (0,2)=⚑, (1,0)=#x, (1,1)=safe, (1,2)=#out.
→ Constraint: 2 + x + out = 3, i.e., x + out = 1.

Cell (1,1) shows 5: its 8-neighbors are all other cells = ⚑(0,0), 3(0,1), ⚑(0,2), #x(1,0), #out(1,2), ⚑(2,0), 3(2,1), ⚑(2,2).
→ Constraint: 4 + x + out = 5, i.e., x + out = 1.

Cell (2,1) shows 3: its 8-neighbors are (1,0)=#x, (1,1)=safe, (1,2)=#out, (2,0)=⚑, (2,2)=⚑.
→ Constraint: 2 + x + out = 3, i.e., x + out = 1.

All three constraints give x + out = 1, enforcing out = NOT(x).

Solution enumeration:

x (mine?)	out (mine?)	x + out	Consistent?	Circuit satisfied?
0 (safe)	1 (mine)	1	✓	NOT(0) = 1 = true ✓
1 (mine)	0 (safe)	1	✓	NOT(1) = 0 = false ✗
0 (safe)	0 (safe)	0 ≠ 1	✗	—
1 (mine)	1 (mine)	2 ≠ 1	✗	—

The Minesweeper instance has 2 consistent assignments. Adding the output constraint (out must be a mine), only (x=0, out=1) remains — matching the unique satisfying assignment x = 0.