Tiling Foundry

Finite tilings / inspectable decisions

Tiling Foundry

Can a region be tiled using a fixed set of 23 Wang tiles? Tiling Foundry turns a Cubic Monotone 1-in-3 SAT formula into such a region using the Yang–Zhang construction. Four decision paths compare results, separate checkers validate SAT witnesses, and a PDF dossier records the run.

Run the demo Follow the technical tour Explore the pipeline Inspect the worked example

Project map

One construction, several independent checks

  1. The fixed tile vocabulary contains the 23 tiles used by every Wang solver.
  2. Boolean Z3 checks the source formula.
  3. Yang–Zhang constructs one finite Wang region.
  4. Reference and optimized native paths solve the same region.
  5. Wang Z3 provides a separate finite-region oracle.
  6. Independent checkers validate returned witnesses.
  7. Visualization follows verification and changes no decision.

Verified output

A checked tiling from one SAT run

A compact square Wang witness preview for the captured SAT source.
observed. Selected verified SAT square output for the captured instance. Source contract: wang-solution-v1.

Independent checkers validated the square tiling shown here. Read the named example for its input and checks, and the visualization component for the square, generalized, and hex views of that same witness.

Reading path

Story, contracts, evidence

Use the pipeline story to follow the input through each component, the reference index for specifications and implementation guides, and the evidence index for measurements with their dates, inputs, and limits. The dossier guide explains how to run your own input and inspect the recorded result.