Counting Square Tilings with a Fixed Set of Polyominoes Is #EXP-Complete

Baao Xie; Qiuyu Chen

REVIEW

Counting Square Tilings with a Fixed Set of Polyominoes Is #EXP-Complete

Qiuyu Chen, Baao Xie

Computational Complexity · Submitted 30 Oct 2026

Pith's verdict: Resolves Pak's fixed-polyomino square-counting conjecture with a long, explicit construction; the complexity-theoretic skeleton is sound and the geometric anchoring lemma is where a referee should dig.

T0 · AI review

How this review was made: An AI referee (deepseek/deepseek-v4-flash) read the paper on November 2, 2026 and answered a fixed list of questions about it. T0 is the starting level every paper gets. The levels describe how deeply Pith has checked the paper, never the authors.

T0 AI review An AI read the paper and answered a fixed list of questions.
T1 Audit Automatic checks that the references and files the paper relies on exist and match.
T2 Compute The paper's code or calculations re-run with the same results.
T3 Formal statement The claims written out in a formal math language a computer can read.
T4 Proof Those claims proved, and the proof checked by computer.

How Pith checks papers →

· 5 minor · Ask about this paper · The compiled record · Read the full review →

Challenge this review Comment (0) Read on arXiv ↗

Cite ▾

arXiv ID2610.42063 (version 2)

Pith IDXYBWHVO7, Pith's permanent record of this paper and its review

CitationBaao Xie, Qiuyu Chen. "Counting Square Tilings with a Fixed Set of Polyominoes Is #EXP-Complete." arXiv:2610.42063 (2026). https://pith.science/paper/XYBWHVO7

Cite this reviewBibTeX for Pith's review of this paper

Claim paper

Why Pith says this

Highlight any text to comment on it.

Editor's note

read the letter

The headline fact: this paper resolves Pak's conjecture (Pak18, Conj. 1.7). There exists a fixed finite family of connected polyominoes whose translation-only square-tiling count, with n given in binary as the sole input, is #EXP-complete under polynomial-time metric reductions, and the count function is in #E. Since tileability for any fixed family is decidable in O(log n) time, the decision/counting separation is sharp in a maximally restricted setting. That is a real result.

What is genuinely new beyond the theorem: two-stage numerical isolation and the rigid geometric compiler. Intended computation histories get a dominant multiplicative factor (Q^{4n-4} from the side-activity amplifier); every junk class is bounded below that (Q^{3n-2}R0^n), so the accepting-path count comes back by integer division. The same trick reappears at the geometric level: canonical one-block tilings contribute samp^{En} * arect(n,n), and nontrivial rectangular dissections are suppressed by a seam-count bound, at least n seams per nontrivial dissection and at most 256^I dissections with I seams. Constants are explicit everywhere, and the postprocessor bit-complexity is actually checked, with an early exit so the reduction never iterates n in unary. The perimeter bound for open Wang tilings of arbitrary rectangles is the cleverest piece: the Case Q identity condition (old centre equals new centre) is what stops zero-head columns from branching exponentially.

Soft spots, in proportion. The load-bearing step is Theorem 7.2(2): every tiling of the Ps*n square has exactly one carrier anchored at each macro-corner. The row-major induction is case-heavy (six origin cases) and leans on the no-three-gap rigidity of Lemma 7.1. I read the cases; the plug-overlap argument and the south-bump case check out. But this is the kind of geometric claim where one surviving noncanonical placement would silently break the Theorem 7.2(5) bijection and the Section 9 floor identity. Referee time should go there, ideally against the companion Lean formalization, which is cited as a GitHub URL with no commit hash and so cannot be machine-checked as cited. Minor: the Mennen-and-Pak attribution points at lecture slides rather than a paper, and the finite exceptional table Hexc is nonconstructive; both are legitimate and the authors are upfront about them.

Bottom line: the proof is long but internally coherent, the reduction is fully explicit, and the citation pattern is appropriate. The readers who get value here are complexity theorists and enumerative combinatorics people, and I would bring it to a reading group. Send it to a serious referee; the complexity skeleton should survive, and the geometric anchoring section deserves one careful reader.

Referee report

Significance

If correct, the result is a striking separation: tileability of a square by a fixed polyomino family is decidable in polynomial time, while exact counting of the same fixed family remains #EXP-complete when the square side length is the only input. The paper is constructive, with explicitly defined constants and a fixed finite family, and it develops a reusable two-stage numerical isolation method together with a rigid geometric compiler. The proof is unusually long, but the reductions are parsimonious and metric, and the claimed companion Lean 4 formalization, if verified, would further support the intricate geometric part. The paper also provides useful quantitative tools, notably the perimeter bound for open Wang rectangles and the rectangular-dissection seam bound, which are of independent interest.

Minor objections (5)

[Sections 5.2 and 5.3] Several displayed constants have lost their superscripts: "R0 = 4Rtab5772", "≤ 5772n", and "1 + 16Q2 ·2Rtab(|Sscan|+1)2" should be R_0 = 4 R_tab 577^2, 577^{2n}, and 1 + 16 Q^2 · 2 R_tab (|S_scan|+1)^2; please fix these so the constants are unambiguous.
[Section 7, Lemma 7.1] The coordinate-separation claim that a boundary dent and the cavity have at least fifteen occupied body cells between them is correct but is stated without the explicit inequalities; please spell out that the cavity begins at relative row/column 16, while side dents occur at relative row/column 0 or P_s-1, so at least fifteen body cells separate them whenever they share a row or column.
[Section 7, Theorem 7.2(2)] The no-three-gap overlap step in the anchoring induction is correct but compressed; I recommend isolating it as a short lemma stating that a length-P_s interval with the displayed origin bounds contains three consecutive positions inside one already-anchored macrocell, and that a length-3 segment on a top body row can meet at most one missing body cell, so the overlap conclusion is fully checkable in every case.
[Section 3] The identity after the definition of L_enc(x) is typeset incorrectly as "2pU(m) + 5m2 + 52"; it should be 2 p_U(m) + 5m/2 + 5/2, which is what the subsequent inequality uses.
[References, [Che26]] Since [Che26] is a GitHub repository rather than a published article, the sentence claiming a companion Lean 4 formalization should specify which statement is formalized and give a version or commit, and the claim should be verified before being treated as an independently checked artifact.

How Pith checks papers → · Full audit of this paper →

The paper

The paper claims

There is a fixed finite family of connected polyominoes whose translation-only square-tiling count, read from the binary side length, is #EXP-complete under polynomial-time metric reductions.

The reading

The paper proves that exact counting can remain #EXP-hard even when every instance is just one number: the binary side length of a square. It constructs a fixed finite family $T^*$ of nonempty connected polyominoes such that the number of translation-only tilings of the $n\times n$ square is #EXP-complete under polynomial-time metric reductions and belongs to #E. Since deciding whether any fixed polyomino family tiles a rectangle can be done efficiently in the binary notation of its dimensions, the result separates a feasible decision problem from an exponentially hard exact-counting problem without varying the tile set or the region shape. The intended computation is recovered from the tiling count by a two-stage numerical isolation argument: a dominant contribution is made arithmetically identifiable, and all other tilings are bounded as junk.

What carries the argument

Two mechanisms carry the argument. The first is a boundary amplifier inside a fixed Wang tile system: side-activity tracks make the all-active boundary class contribute exactly $Q^{4n-4}$ tilings, every proper boundary class at most $Q^{3n-2}$ tilings, and a tableau track, ripple counter, and edge scanner turn the open square count into $Q^{4n-4}Acc^*(n)+Junk(n)$ with a bounded junk term. The second is a rigid geometric compiler: each Wang tile type becomes a connected carrier polyomino whose L-shaped interior cavity records the tile identity and whose dent-and-bump boundary registers encode edge colours and open or closed interface bits. Local no-three-gap rigidity forces every carrier in every tiling of the $P_s n$ square onto the $P_s$-spaced macro-grid; open interfaces are saturated and therefore organize the macro-grid into filled rectangular blocks. The exact polyomino count then equals a sum over rectangular dissections, and a seam bound together with a Wang perimeter bound makes the single-block term dominant, so a floor division recovers the Wang count.

Extended reading notes

Core claim

At the center is Theorem 1.1. The paper builds one fixed family $T^*$ and proves that for $n$ written in binary, the function counting translation-only tilings of the $n\times n$ square is complete for #EXP under polynomial-time metric reductions and lies in #E. The side length encodes a #EXP-complete accepting-path counting problem through an injective self-delimiting map $E_{side}$; a fixed one-head machine $M^*$ then realizes the encoded computation. In the Wang stage, which uses open tilings with unconstrained boundary colours, an open-square counter gives $a_{prod}(n)=Q^{4n-4}(1+C_U(x))+Junk(n)$ on encoded lengths, with $0\le Junk(n)<Q^{4n-4}$, so the accepting count is recovered by integer division. In the geometric stage, carriers anchored on a $P_s$-spaced grid realize each Wang tiling, and the exact sum over rectangular partitions of the macro-grid has a dominant one-block term, yielding the same floor-recovery identity for the polyomino count. Composing the two reductions proves the theorem.

Load-bearing premise

The load-bearing premise is geometric: in every tiling of the large square, each coarse grid point $(iP_s,jP_s)$ is covered by exactly the carrier anchored at that position, and no piece can sit shifted or interleaved off that grid.

Editorial extensions

If this is right

Deciding whether a fixed polyomino family tiles the $n\times n$ square costs polynomial time in the binary length of $n$, while the exact count for the same fixed family is #EXP-complete; the theorem makes the feasibility-versus-counting gap independent of varying the region.
$g_{T^*}$ belongs to #E, so each exact count has a witness of exponential length checkable in exponential time; completeness holds for the full #EXP class under metric reductions.
The binary side length is a complete input for an exponentially hard counting problem: the self-delimiting encoding $E_{side}$ lets one fixed machine start from the side-length bits and produce a #EXP-complete accepting-path count.
The dominant-term-plus-junk design gives a two-stage template for exact counting reductions under fixed local rules, as the paper suggests in its concluding remarks.
The paper also records that the support language of the #EXP-complete counting function $C_U$ is NEXP-hard, so the construction carries decision hardness as well.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Beyond the paper, the same numerical-isolation scheme, amplify the intended boundary class, prove a perimeter-type bound on all other configurations, and recover by division, should transfer to other succinct counting problems with fixed local rules, such as counting configurations of translation-invariant Hamiltonian systems or cellular automata with a binary size parameter.
The paper does not try to minimize the family $T^*$; if the carrier and amplifier sizes can be compressed, the threshold where fixed polyomino counting becomes hard may connect to known small-set undecidability results for polyomino tiling.
A testable extension is to implement the construction for the smallest encoded inputs and check that the integer part of $g_{T^*}(P_s n)/s_{amp}^{2n(n-1)}$ equals $a_{prod}(n)$ exactly; the floor identity predicts this equality for every positive $n$, with finitely many exceptional small side lengths handled by a fixed table.

Original abstract

An important question in counting complexity is whether exact counting can remain hard under restrictions that make feasibility easy. Tilings of squares by a fixed family of polyominoes provide a stringent test of this question, since tileability is polynomial-time decidable and the only varying input is a binary-encoded side length. We prove that there exists a fixed finite family of connected polyominoes for which counting translation-only square tilings is #EXP-complete under polynomial-time metric reductions, while the counting function belongs to #E. The resulting separation reveals that solution multiplicities can retain computational information that feasibility alone cannot capture. The proof develops a two-stage numerical isolation technique that combines a boundary-amplified Wang system with a rigid geometric compiler to recover accepting-computation counts while controlling all noncanonical tilings.

The compiled record

The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.

Compiled by classifier-1.13.0 via TypeSafe API, question bank abstract-p1-20260923, 2026-11-02: 1 request, 4,334 input tokens.

What the abstract itself states, as probabilities: claims first 0.07 · states limitation 0.18 · human participants 0.01 · controlled comparison 0.03 · randomized assignment 0.01 · states quantitative result 0.20 · compares with prior results 0.53 · mentions code or data availability 0.02.

The abstract, sentence by sentence

arXiv listing abstract v1. Results and the main claim are underlined; show every role.

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.

background contribution method result interpretation main claim

What the classifier reports for each sentence. The number is the probability it gave the label.
#	sentence	role	the authors' own work	states the main conclusion	strength
s0	The gap between feasibility and exact counting raises a fundamental question about how much information an input must carry to sustain computational hardness.	gap 0.55	0.06	0.05	asserted 0.70
s1	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.	result 0.71	0.88	0.23	asserted 1.00
s2	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.	result 0.95	0.92	0.89	asserted 1.00
s3	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.	interpretation 0.99	0.52	0.40	asserted 1.00
s4	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.	method 1.00	0.92	0.06	asserted 1.00

What kind of paper the classifier reports this is: theoretical result 1.00 · evidence from proof or derivation 1.00.

What was examined, and what was not

sources read

arXiv listing abstract v1

not examined

full text
figures and tables
references and citing sentences
relations to other papers

levels run

P abstract

not run

S sections
T body sentences
C citations
R cross-paper relations

Every quoted sentence on this record is the authors'. Every label is from Pith's closed vocabulary, with the probability shown beside it. Every number in the measurements table is the authors', checked by code. Record as JSON

Figures

**Figure 1.** Full-frame boundary coupling and east-edge scanning at the Wang level (schematic). In

**Figure 2.** Identity register and one open horizontal carrier interface (schematic, not to scale). Panel

**Figure 3.** Canonical and nontrivial rectangular components at the macrogrid level. In panel (a),

Figures reproduced from arXiv:2610.42063 by the authors.

References

Discussion

Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.