Tiling Foundry

Component order, data flow, independence, and trust boundaries from a CM1-in-3 formula to checked Wang presentations.

The complete pipeline

A CM1-in-3 formula enters four decision paths. When they agree on SAT, their returned witnesses must pass independent checks. When they agree on UNSAT, the run records that result without claiming an independent UNSAT certificate. The dossier and optional PDF reuse the recorded input, results, and checks. Use the demo guide to run a new formula through this sequence.

The captured formula moves through Boolean Z3, Yang-Zhang reduction, both native solvers, Wang Z3, verification, and presentation.
observed. One validated v2 capture in fixed component order. Open the static contact sheet. Source contract: wang-run-dossier-v2#named-components.

Data flow

The source formula enters two deliberately different paths. The Boolean Z3 component decides the formula directly. Independently, the Yang–Zhang component constructs a finite region over the fixed tile vocabulary. The reference solver, optimized solver, and Wang Z3 oracle consume that same region and tileset, identified by their hashes. The paper proves the reduction’s equivalence; the builder implements it, and the tests check that implementation on concrete inputs.

Step Input Output Relationship
Boolean Z3 canonical formula status and optional assignment independent source-level decision
Yang–Zhang canonical formula region, tileset, provenance semantic construction
Reference solver region and tileset status and optional tiling executable baseline
Optimized solver same region and tileset status and optional tiling independent invocation of the shared native core
Wang Z3 same region and tileset status and optional model independent finite-region oracle
Verification returned witnesses and original inputs named checker receipts independent cross-check
Visualization verified square witness square, generalized, and checked hex views presentation-only

Independence

The reference path remains executable and understandable. The optimized path retains the same public semantics while selecting six measured private mechanisms. Boolean Z3 does not call the reduction, and Wang Z3 does not call a native solver. Independent checkers consume returned assignments or tilings; they do not trust a raster.

Trust boundaries

  • SAT is accepted only with the applicable witness checks.
  • UNSAT from a solver is a terminal observation, not a standalone certificate.
  • UNKNOWN is preserved where an oracle can return it; it is never rewritten as UNSAT.
  • Timeout, errors, disagreement, or incomplete traces stop the demo; none means UNSAT.
  • Trace replay presents recorded semantic events but does not solve again.
  • Generalized and hex views are downstream transformations, not new solvers.

The worked example follows one named SAT source through these boundaries. Maintained APIs and methods remain in the reference index; measurements and dated observations remain in evidence.