wangTilesFast

Fast Wang tiles solver in Nim using MiniSat as backend. Successor to TileSAT — same input format, ~2-3 orders of magnitude faster on medium/large grids.

The CNF is streamed straight into minisat's stdin (/dev/stdin) and the result is read from a tmpfs file in /dev/shm — nothing touches disk, so no gzip is needed anywhere.

Build & run

nim c src/wang.nim
./src/wang input/aperiodic11                 # solve at input's default size
./src/wang input/aperiodic11 -W=64 -H=64     # override grid size
./src/wang input/aperiodic11 -W=96 -H=96 --bench

Run ./src/wang -h for all options.

Drawing solutions

./src/wang input/aperiodic11 -W=40 -H=40 --print=none --svg=output/aperiodic11_40_40.svg

Same look as TileSAT's drawTiles.py (N/E/S/W color triangles per tile + numbered tile legend), but the SVG is written directly by the solver — no python3/tkinter/canvasvg and no graphic environment needed. --tile-size=N sets the tile size in pixels (default 40).

Encoding research (aperiodic11: 11 tiles, 4 colors, Jeandel–Rao set)

Six encodings benchmarked (bench/encodings.tsv, bench/round2.tsv). Cell constraint = exactly-one tile per cell unless noted; the adjacency encoding is what matters:

encoding	adjacency clauses	solve 58×58
support (TileSAT baseline)	x[c][t] → ⋁ compatible x[c'][·], forward only	78.3 s
support2 (winner)	support in both directions	0.45 s
conflict	binary ¬x∧¬x' per incompatible pair	8.1 s
conflictnoamo	conflict, AMO dropped (still sound)	6.9 s
edge	channeled through edge-color vars	6.9 s
supportconflict	support + conflict	1.5 s

Findings:

• Bidirectional support implications are the whole ballgame — 176× faster than forward-only at 58×58, and the gap grows with size. Unit propagation flows right-to-left/bottom-to-top as well, so placing any tile immediately prunes all neighbors' domains, like arc consistency.
• Redundant additions (conflict clauses on top: support2conflict) only add overhead at most sizes.
• Pairwise AMO beats Sinz for the 11-tile cell groups (tiny groups; aux vars just dilute the search).
• Dropping AMO (sound for conflict/edge encodings) is a nice clause-count trick but propagation strength matters more.

Scaling with support2 + tuned params: 64×64 in 0.6 s, 96×96 in 1.9 s, 128×128 in 5.7 s.

MiniSat parameter tuning

Two independent studies: one-at-a-time sweeps (bench/tune80.txt on aperiodic11, bench/tune64_aperiodic13.txt on the 13-tile aperiodic set), winners validated across sizes (bench/tune_combos.txt, bench/tune_combos13.txt).

aperiodic11 (solve_ms at 64/80/96/112):

config	64	80	96	112	geomean
minisat defaults	476	1760	7676	9104	2765
-var-decay=0.85 -rfirst=2000	660	771	1993	1988	1191
-rfirst=2000 -no-pre	694	368	1757	4766	1211

13-tile aperiodic set (solve_ms at 48/64/72/80 — note the harder cliff):

config	48	64	72	80	geomean
minisat defaults	639	2010	16940	79380	6455
-var-decay=0.85 -rfirst=2000	440	1147	8838	27957	3341
-rfirst=2000	501	1099	2484	4944	1614
-rfirst=2000 -no-pre	297	695	1935	4635	1163

• -rfirst=2000 (restart later) is the one robust winner on both tile sets — up to 16× at 80×80 on the 13-tile set. Satisfiable structured instances reward committing to a region instead of restarting away.
• -no-pre (skip SatELite preprocessing) helps both sets; the support2 encoding is already tight, so preprocessing mostly burns time.
• -var-decay=0.85 helped aperiodic11 but hurt the 13-tile set 2-6× — a warning about single-instance tuning.
• Hurts everywhere: reduced phase-saving (timeouts on the 13-tile set), rinc=1.5, rnd-freq.
• -rfirst=2000 -no-pre is baked in as the default (best cross-set geomean: 1187 vs 1995 for the old vd085 combo). Override with --msat="..." or disable with --no-tuned.

Layout

• src/wang.nim — solver (encoder + minisat runner + verifier)
• bench/encodings.sh, bench/round2.sh — encoding sweeps
• bench/tune.sh, bench/tune_combos.sh, bench/tune_combos13.sh — minisat parameter tuning (tune.sh takes [SIZE] [ENC] [CPULIM] [INPUT])
• input/ — tile sets copied from TileSAT (aperiodic11, aperiodic, aritmetica)