Wang Z3 oracle
What it is
Wang Z3 is an independent Python oracle for a finite Region and immutable
tileset. It returns a dense row-major tiling model when the region is SAT.
Why it exists
This oracle checks the native decision paths with a different implementation and constraint engine. It neither parses the source formula nor rebuilds the Yang–Zhang reduction, so the shared region identity is an explicit boundary.
Inputs and outputs
Input is the hash-bound region and tileset produced once by the native
construction. Output preserves SAT, UNSAT, or UNKNOWN and an optional dense
model. z3-encoding-summary-v1 records project-owned term and assertion order,
counts, identity, status, and copied model.
Mechanism
The model creates (N,E,S,W) edge-color terms in row-major order, shares terms
across active internal adjacencies, restricts each cell to a canonical tile
tuple, and applies exposed boundary colors. Its fixed configuration uses one
thread and a fixed random seed.
Primary animation
wang_z3 shows the project’s edge-term construction and returned result, not
the solver engine’s internal search.
z3-encoding-summary-v1+wang-tileset-snapshot-v1+wang-region-snapshot-v1.
Position in the pipeline
Wang Z3 consumes the same constructed region as both native solvers and joins them at agreement. It is an independent cross-check, not a fallback or a producer of hints for either native path.
Observed example
For pipeline_sat.cm13, the oracle returns SAT over the same region and tile
identities as the native runs, and its dense model passes the pure Python
tiling checker.
Trust boundary
The summary stabilizes project construction order and the copied result only. It does not claim to expose Z3 branching, propagation, proof search, or debug events. A rendered frame is not the tiling checker.
Artifacts and references
See the Wang Z3 model reference,
comparison protocol,
and python/oracles/tiling_solver.py.