[Rule] Satisfiability to Minesweeper

[QingyunQian]

Source: Satisfiability
Target: Minesweeper
Motivation: Re-establishes NP-completeness of Minesweeper Consistency by direct reduction from SAT (rather than CircuitSAT). Uses much more compact templates than Kaye's original proof, and guarantees a predetermined mine count — matching the original Minesweeper game rules where the total number of mines is known.
Reference:

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

Reduction Algorithm

Notation:

• Source: a Boolean formula f in CNF with k variables x₀, ..., x_{k−1}, l literal occurrences, and h gate layers in its binary tree representation.
• Target: a Minesweeper instance on an M × N grid with a predetermined mine count M_f and a designated output square.
• Let l_w = number of normal (non-inverting) wires and l_i = number of inverting wires in the inversion sublayer, with l_w + l_i = l.

Step 1: Formula preprocessing

Convert the CNF formula into a binary tree representation. Apply De Morgan's law to eliminate AND gates: x₀ · x₁ = (x₀' + x₁')'. After this transformation, the tree has only OR gates and negation in the wiring. Remove any resulting double negations.

Step 2: Literal layer construction

Build the leftmost part of the Minesweeper grid, consisting of three sublayers:

1. Mine-count sublayer (width 12 columns): For each of the l horizontal literal wires, create a pair of splits. Each pair consists of one split in this sublayer and one in the variables sublayer. The two splits in a pair always have exactly 5 covered mines total (regardless of variable valuation), ensuring a predetermined mine count. Splits are arranged in alternating stacks connected by simple wires (4×3, 8 predefined + 1 covered mine).

2. Variables sublayer (width 6k columns): One vertical wire per variable, built from crossing templates (6×6, 16 predefined + 3 covered mines) stacked vertically. Each vertical wire has exactly one split template (6×6, 16 predefined + 1 or 4 covered mines) at the position where the corresponding literal branches off horizontally.

3. Inversion sublayer (width 6 columns): For each literal, either a normal wire (6 wide, 18 predefined + 2 covered mines) or an inverting wire (6 wide, 16 predefined + 2 covered mines), depending on whether the literal is positive or negated.

Total literal layer dimensions: (18 + 6k) × (3 + 6l).

Step 3: Gate and wiring layers

Build the circuit from left to right, following the tree structure:

1. Gate layer (width 7 columns each): For each position in the gate layer, place either:

   • OR gate template: 3×3 kernel with uncovered "3" center, inputs 5 squares apart. 29 predefined + 3 covered mines.
   • Wire-gate template: for tree positions without a gate. 18 predefined + 2 covered mines.

2. Wiring layer (width 10 columns each): Connects consecutive gate layers. Consists of:

   • Inversion sublayer (6 columns): optional negation via wire/inverting-wire templates.
   • Displacement sublayer (4 columns): vertical displacement templates for 3+6n rows (n ∈ ℕ₀). For even n: 14+14n predefined + 1+3(n/2) covered mines. For odd n: 14+12n predefined + 3+3⌊n/2⌋ covered mines.

3. Final inverter (width 3 columns): A NOT gate at the output ensures the mine count is independent of the Boolean valuation. 4 predefined + 1 covered mine. The output is taken from either the input or output of this inverter, depending on whether the formula's root is negated.

Step 4: Border and fill

• Bottom border: 2 rows, 3 mines per variable column (3k mines total).
• Top border: 1 row, no mines (but top splits/crossings have 1 extra mine each, contributing k additional mines).
• All grid cells not covered by any template are revealed safe squares with counts derived from neighboring mines.

Step 5: Output constraint

The designated output square (i, j)_f is constrained to contain a mine. The formula f is satisfiable if and only if the generated partial Minesweeper solution is consistent with a mine at (i, j)_f.

Key template properties (from Thieme & Basten, Table in Section 6):

Template	Size	Predefined mines	Covered mines
NOT gate	3×3	4	1
OR gate (synthesis)	7 wide	29	3
Wire gate (synthesis)	7 wide	18	2
Wire (synthesis)	6 wide	18	2
Inverting wire (synthesis)	6 wide	16	2
Split	6×6	16	1 or 4 (paired: always 5)
Crossing	6×6	16	3
Simple wire (mine-count)	4×3	8	1
Displacement (even n)	4+5n wide	14+14n	1+3(n/2)
Displacement (odd n)	4+4n wide	14+12n	3+3⌊n/2⌋

Correctness (Proposition 1 + Theorem 1 from the paper):

A Boolean formula f is satisfiable if and only if the generated partial Minesweeper solution, with a mine allocated to the designated circuit output, is consistent. The conversion is polynomial in the size of the formula. Minesweeper Consistency is NP-complete.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
rows	3 + 6 * num_literals
cols	11 + 6 * num_vars + 17 * h
num_unrevealed	5 * num_literals + 2 * l_w + 2 * l_i + 3 * (num_vars * num_literals − num_literals) + ⌊num_literals / 2⌋ + 3 * g_or + 2 * g_wire + Σ d_j + 1, where h = gate layers in binary tree, l_w/l_i = normal/inverting wires, g_or/g_wire = OR/wire gates per layer, d_j = covered mines in displacement template j
num_revealed	rows × cols − num_unrevealed − M_predefined

All quantities are polynomial in num_vars, num_literals, h (and hence in the formula size). The total predetermined mine count M_f = 4·num_vars + 19·num_vars·num_literals + 25·num_literals + 9⌊num_literals/2⌋ + 20·l_w + 18·l_i + M_circuit (where M_circuit depends on gate/wiring layer template counts + 7 for the final inverter) is a construction property, not a target size field.

Validation Method

• For small formulas (1–2 variables, 1–2 clauses), manually construct the Minesweeper grid following the synthesis procedure and verify:
  1. All template mine counts match the paper's specifications.
  2. Satisfying assignments of the formula correspond to consistent mine assignments.
  3. Unsatisfiable formulas produce inconsistent Minesweeper instances.
• Cross-reference with Thieme & Basten (2022), specifically Figures 1–13 and Section 7.
• Compare grid sizes against the dimension formulas: rows = 3 + 6l, cols = 11 + 6k + 17h.

Example

Source SAT instance:

Formula: f = NOT(x₀)
  In CNF: single clause (¬x₀), i.e., one unit clause.

Variables: k = 1 (x₀)
Literals: l = 1 (one occurrence of x₀)
Gate layers: h = 0 (no OR gates needed; the formula is a single literal)

After De Morgan preprocessing: no AND gates to eliminate.
The tree is a single leaf: ¬x₀.

Satisfying assignment: x₀ = 0 (false), so ¬x₀ = true.

Target Minesweeper instance construction:

Grid dimensions: rows = 3 + 6×1 = 9, cols = 11 + 6×1 + 17×0 = 17

Literal layer only (no gate layers needed):
  - Mine-count sublayer (12 cols): 1 pair of splits
  - Variables sublayer (6 cols): 1 vertical wire with 1 split for x₀
  - Inversion sublayer (6 cols): 1 inverting wire (since literal is ¬x₀)

The core of the construction is the NOT gate gadget at the inversion sublayer.

NOT gate gadget within the grid (the inversion sublayer):

The inverting wire contains a NOT gate core (3×3):

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

  - #x₀ at (1,0): covered cell representing x₀ (mine = x₀ is true)
  - #x₀' at (1,2): covered cell representing ¬x₀ (mine = ¬x₀ is true)
  - 4 predefined mines at corners
  - 3 revealed safe cells showing counts 3, 5, 3

Constraint verification for the NOT gate core:

Cell (0,1) = 3: neighbors include ⚑(0,0), ⚑(0,2), #x₀(1,0), safe(1,1), #x₀'(1,2).
→ 2 + x₀ + x₀' = 3 → x₀ + x₀' = 1.

Cell (1,1) = 5: all 8 neighbors = 4 corner mines + #x₀ + #x₀' + 2 safe cells.
→ 4 + x₀ + x₀' = 5 → x₀ + x₀' = 1.

Cell (2,1) = 3: neighbors include #x₀(1,0), safe(1,1), #x₀'(1,2), ⚑(2,0), ⚑(2,2).
→ 2 + x₀ + x₀' = 3 → x₀ + x₀' = 1.

All constraints enforce x₀' = NOT(x₀). The output x₀' is constrained to be a mine (true).

Solution:

x₀	x₀' = NOT(x₀)	x₀ + x₀' = 1?	Output = mine?	Formula satisfied?
0	1	✓	✓ (x₀' = mine)	¬0 = true ✓
1	0	✓	✗ (x₀' = safe)	¬1 = false ✗

Only x₀ = 0 produces a consistent Minesweeper instance with the output constrained to be a mine, matching the unique satisfying assignment.

Mine count verification:

Total mines in the NOT gate core: 4 predefined + 1 covered = 5.
This count is independent of the valuation (always exactly 1 covered mine), confirming the predetermined mine count property.