Counting Square Tilings with a Fixed Set of Polyominoes Is #EXP-Complete
Qiuyu Chen, Baao Xie
cs.CC
Oct 30, 2026 · v1
TL;DR
The #EXP-completeness result for fixed-polyomino square tiling counts has a companion Lean 4 formalization released as a separate artifact.
Abstract
The gap between feasibility and exact counting raises a fundamental question about how much information an input must carry to sustain computational hardness. We show that this separation persists even when the geometric rules are fixed and each instance is specified solely by the binary side length of a square. Specifically, there exists a fixed finite family of connected polyominoes whose translation-only square-tiling counting function is #EXP-complete under polynomial-time metric reductions and belongs to #E. Since tileability for any fixed polyomino family is decidable in polynomial time, this result establishes a striking separation between feasibility and exact counting under highly restricted geometric inputs. The proof develops a two-stage numerical isolation technique that recovers accepting-computation counts from a boundary-amplified Wang system and preserves them through a rigid geometric compiler that controls all noncanonical polyomino tilings.
Problem
Pak conjectured that counting translation-only tilings of an n×n square by a fixed finite polyomino family, with n given in binary, can be #EXP-complete. Tileability in this setting is decidable in polynomial time, which raises the question of whether the exact count still carries exponential-time counting hardness.
Approach
A fixed nondeterministic machine reads its input from the binary side length, and its accepting paths are encoded as Wang tile tableaux. A boundary-amplified Wang system makes the intended boundary class dominate all other open-boundary configurations. A rigid geometric compiler then realizes the Wang tiles as connected polyomino carriers, and rectangular-dissection bounds control noncanonical tilings. The completeness result is accompanied by a Lean 4 formalization.
Results
There is a fixed finite family of connected polyominoes whose square-tiling counting function lies in #E and is #EXP-complete under polynomial-time metric reductions. The accepting-path count is recovered from the tiling count by integer division, which resolves Pak's conjecture.
