Refactor Wang Z3 around shared edge terms

README.md

@@ -104,6 +104,14 @@ Boolean Z3 solves the original formula rather than the Wang region, so its row
 is not a speedup claim. The much faster UNSAT rows use deliberately shallow
 contradictions, not hard UNSAT search.
 
+The Wang Z3 oracle now models one finite edge-tuple relation per active cell
+and shares a single color term across each internal edge. A controlled
+single-sample SAT comparison on the same CPU reduced the prepared-Region path
+from 10.666 s to 2.605 s and the complete-file path from 10.560 s to 2.620 s,
+while peak process RSS decreased slightly. The model, duplicate-tile semantics,
+test evidence, command, and measurement limits are recorded in the
+[edge-table report](docs/wang_z3_edge_table_2026-08-24.md).
+
 ## Goal
 
 The intended end-to-end pipeline is:
@@ -158,7 +166,7 @@ tileability.
 
 ## Current status
 
-Implemented and tested as of 21 August 2026:
+Implemented and tested as of 24 August 2026:
 
 - canonical static definition of the 23 atomic Wang tiles;
 - generalized-tile family metadata kept outside solver semantics;
@@ -206,7 +214,8 @@ Implemented and tested as of 21 August 2026:
   the native `TILESET` symbol without importing ctypes into models or oracles;
 - independent Boolean and Wang witness checkers plus Z3 oracles: the Boolean
   path preserves repeated clause positions, while the Wang path consumes the
-  copied `Region`, enforces boundary and oriented adjacency constraints, and
+  copied `Region`, constrains each active cell to a finite edge-tuple relation,
+  shares color terms across active internal edges, enforces boundaries, and
   returns a dense tiling only for SAT;
 - a shared `libwang.so` build and tested C-to-Python formula and region
   adapters that copy results into immutable Python storage, report native

docs/development_principles.md

@@ -6,7 +6,7 @@ description: How Tiling Foundry separates source data, derived state, native lif
 section: Architecture and correctness
 document_kind: Architecture reference
 status: Current implementation
-updated: 2026-08-21
+updated: 2026-08-24
 nav_order: 10
 ---
 
@@ -149,9 +149,12 @@ There are two distinct oracle contracts:
 - Boolean Z3 (implemented): `Formula -> Boolean constraints ->
   SAT/UNSAT/UNKNOWN` and an assignment only for SAT. It performs no parsing,
   I/O, ctypes work, region construction, or reduction.
-- Wang Z3 (implemented): `Region + canonical TILESET -> tiling constraints ->
-  SAT/UNSAT/UNKNOWN` and a dense tiling only for SAT. It receives the same
-  concrete region as the native solver and does not rebuild Yang–Zhang.
+- Wang Z3 (implemented): `Region + TILESET -> per-cell edge-table constraints
+  with shared internal edge terms -> SAT/UNSAT/UNKNOWN` and a dense tiling only
+  for SAT. It receives the same concrete region as the native solver and does
+  not rebuild Yang–Zhang. For generic duplicate edge tuples, witness recovery
+  returns a valid positional tile ID from the constraint-equivalent entries;
+  the public contract does not select one duplicate over another.
 
 The Boolean witness checker remains pure Python and counts clause positions,
 not unique variables: `(x, x, y)` counts `x` twice. The Wang checker separately

docs/solver_comparison_benchmark.md

@@ -6,7 +6,7 @@ description: Reproducible protocol for comparing the native and Python Z3 decisi
 section: Cross-engine benchmarks
 document_kind: Benchmark protocol
 status: Current protocol
-updated: 2026-08-21
+updated: 2026-08-24
 nav_order: 10
 ---
 
@@ -146,3 +146,9 @@ two runs are treated as a controlled comparison.
 records the first seven-sample, CPU-pinned smoke baseline, including complete
 timing ranges, process RSS, correctness results, the shallow-UNSAT explanation,
 and the limits on cross-problem interpretation.
+
+The later
+[Wang Z3 edge-table report]({{ '/wang_z3_edge_table_2026-08-24/' | relative_url }})
+records the oracle's constraint-model refactor and its directly comparable
+single-sample before/after check. It does not rewrite the historical baseline
+or introduce a timing threshold.

docs/wang_z3_edge_table_2026-08-24.md

@@ -0,0 +1,120 @@
+---
+layout: page
+title: Wang Z3 edge-table model
+permalink: /wang_z3_edge_table_2026-08-24/
+description: Constraint model, correctness evidence, and before/after smoke measurement for the Wang Z3 edge-table oracle.
+section: Cross-engine benchmarks
+document_kind: Oracle model report
+status: Current implementation
+updated: 2026-08-24
+nav_order: 30
+---
+
+# Wang Z3 edge-table model — 24 August 2026
+
+## Scope and outcome
+
+The Python Wang Z3 oracle still consumes only an immutable `Region` and a
+generic immutable tileset. It does not parse formulas, rebuild the
+Yang–Zhang reduction, call the native solver, or evaluate Boolean clauses.
+
+The refactored model represents tile membership once per active cell and
+represents every active internal adjacency as one shared color term. It
+replaces the previous per-adjacency support implications without changing the
+public `solve_tiling()` result contract. `SAT`, `UNSAT`, `UNKNOWN`, dense
+row-major witnesses, inactive cells, boundary colors, and generic tilesets are
+preserved.
+
+## Constraint model
+
+The preceding encoding created one integer tile-ID variable per active cell.
+For each east or south adjacency and each tile ID it added an implication from
+the source tile to an `Or` of compatible neighbor IDs. On the 444-active-cell
+SAT smoke region, 832 internal edges therefore produced 19,136 support
+implications before boundary and domain constraints were counted.
+
+The current encoding creates `(N,E,S,W)` integer color terms for every active
+cell. Row-major construction reuses the south term of the active cell above as
+the current north term and the east term of the active cell to the left as the
+current west term. An internal edge is consequently one Z3 term, not two terms
+plus an equality and not a replicated tile-support table.
+
+Each active cell receives one finite table-membership constraint:
+
+```text
+Or(
+    And(Nc == N0, Ec == E0, Sc == S0, Wc == W0),
+    And(Nc == N1, Ec == E1, Sc == S1, Wc == W1),
+    ...
+)
+```
+
+Every required boundary color is a direct equality on the corresponding edge
+term. Inactive cells receive no terms and do not share constraints across a
+hole.
+
+The SMT model does not carry a separate tile-ID variable. After `SAT`, the
+four model colors are mapped back to the matching positional tileset ID. The
+canonical 23-tile set has 23 distinct edge tuples. A generic tileset may
+contain duplicate tuples; because such entries are indistinguishable under
+Wang constraints, witness reconstruction currently normalizes them internally
+to one equivalent positional ID. This remains a valid witness; the public
+contract does not select a specific duplicate or satisfying model.
+
+## Correctness evidence
+
+Focused tests now cover:
+
+- exact object identity for every active horizontal and vertical shared edge;
+- semantic independence across an inactive cell with opposite forced colors;
+- SAT/UNSAT agreement with exhaustive enumeration on small generic tilesets;
+- boundary and adjacency contradictions in both orientations;
+- valid positional-ID reconstruction for duplicate edge tuples;
+- dense witness validation by the independent Python checker;
+- propagation of Z3 `UNKNOWN` without requesting a model.
+
+The shared end-to-end SAT and UNSAT fixtures continue through the independent
+checker. No native solver, C verifier, tileset definition, region model, or
+Yang–Zhang builder code changed.
+
+## Controlled smoke measurement
+
+The before/after comparison used the same smallest SAT input, one fresh sample
+per scope, CPU affinity 2, Python 3.13.5, Z3 4.16.0, and the Ryzen 5 3600
+benchmark host. The case contains 451 dense positions and 444 active cells.
+Both source states derive from commit `2e4d8a3`; the only measured oracle
+mechanism change was replacement of adjacency support implications by the
+edge-table model.
+
+```sh
+taskset -c 2 uv run --frozen python benchmarks/python/compare_solvers.py \
+  --case pipeline_sat --engine python-wang-z3 \
+  --scope wang-solve-verified \
+  --scope file-to-verified-decision \
+  --samples 1 --iterations 1 --timeout-seconds 60 \
+  --c-flags '-std=c17 -Wall -Wextra -Wpedantic -O2'
+```
+
+| Scope | Support-implication model | Edge-table model | Time change | RSS change |
+| --- | ---: | ---: | ---: | ---: |
+| `wang-solve-verified` | 10.666394831 s / 88,396 KiB | 2.604701225 s / 87,060 KiB | -75.58% | -1.51% |
+| `file-to-verified-decision` | 10.560000602 s / 88,580 KiB | 2.620350503 s / 86,984 KiB | -75.19% | -1.80% |
+
+Every measured run returned `SAT`, produced a complete dense tiling, and
+passed the independent checker. The result supports retaining the simpler
+edge-table encoding: it removes replicated adjacency tables, materially lowers
+the smoke time, and does not purchase the speedup with higher process peak RSS.
+
+## Interpretation and limits
+
+This is a single-sample, host-specific mechanism check, not an asymptotic claim
+or a CI threshold. It is deliberately comparable to the immediately preceding
+single-sample state; the seven-sample historical cross-engine baseline remains
+a record of the older encoding, not a current performance promise.
+
+The oracle is still a general Z3 model and remains much slower than the native
+solver on this structured region. The measurement covers one small SAT witness
+and says nothing about hard UNSAT behavior or larger scaling presets. Those
+presets remain opt-in under the
+[comparison protocol]({{ '/solver_comparison_benchmark/' | relative_url }}),
+and any broader performance conclusion requires fresh repeated samples.

python/oracles/tiling_solver.py

@@ -3,7 +3,7 @@
 from dataclasses import dataclass
 from enum import Enum
 
-from z3 import ArithRef, Implies, Int, Or, Solver, sat, unsat
+from z3 import And, ArithRef, Int, Or, Solver, sat, unsat
 
 from model.region import Region
 from model.tileset import (
@@ -12,6 +12,7 @@
     DIR_COUNT,
     E,
     S,
+    Tile,
     Tileset,
 )
 
@@ -49,94 +50,85 @@ def _validate_tileset(tileset: Tileset) -> None:
             raise ValueError("tile contains an invalid color")
 
 
+def _edge_terms(
+    region: Region,
+) -> tuple[tuple[ArithRef, ArithRef, ArithRef, ArithRef] | None, ...]:
+    """Create one color term per exposed edge and share every internal edge."""
+    terms: list[
+        tuple[ArithRef, ArithRef, ArithRef, ArithRef] | None
+    ] = [None] * len(region.active)
+
+    for y in range(region.height):
+        for x in range(region.width):
+            index = y * region.width + x
+            if not region.active[index]:
+                continue
+
+            above = terms[index - region.width] if y > 0 else None
+            left = terms[index - 1] if x > 0 else None
+            north = above[S] if above is not None else Int(f"edge_{index}_n")
+            west = left[E] if left is not None else Int(f"edge_{index}_w")
+            terms[index] = (
+                north,
+                Int(f"edge_{index}_e"),
+                Int(f"edge_{index}_s"),
+                west,
+            )
+
+    return tuple(terms)
+
+
 def solve_tiling(region: Region, tileset: Tileset) -> TilingSolveResult:
     """Solve an existing region without parsing or rebuilding its reduction.
 
-    The immutable tileset is validated before use. SAT returns one dense
-    row-major tile ID per active cell and ``None`` for inactive cells; UNSAT
-    and UNKNOWN return no tiling.
+    Each cell is constrained to one tileset edge tuple and adjacent cells
+    share their internal edge-color term. SAT returns one dense row-major tile
+    ID per active cell and ``None`` for inactive cells; UNSAT and UNKNOWN
+    return no tiling. Duplicate edge tuples remain valid, constraint-equivalent
+    tile IDs.
     """
     _validate_tileset(tileset)
 
     solver = Solver()
-    variables: list[ArithRef | None] = [
-        Int(f"tile_{index}") if active else None
-        for index, active in enumerate(region.active)
-    ]
-    compatibility = {
-        direction: tuple(
-            tuple(
-                adjacent_id
-                for adjacent_id, adjacent in enumerate(tileset)
-                if tile[direction]
-                == adjacent[(direction + 2) % DIR_COUNT]
-            )
-            for tile in tileset
-        )
-        for direction in (E, S)
-    }
+    edges = _edge_terms(region)
+    tile_id_by_edges: dict[Tile, int] = {}
+    for tile_id, tile in enumerate(tileset):
+        tile_id_by_edges.setdefault(tile, tile_id)
 
-    for index, variable in enumerate(variables):
-        if variable is None:
+    for index, cell_edges in enumerate(edges):
+        if cell_edges is None:
             continue
 
         solver.add(
             Or(
-                *(variable == tile_id for tile_id in range(len(tileset)))
+                *(
+                    And(
+                        *(
+                            cell_edges[direction] == color
+                            for direction, color in enumerate(tile)
+                        ),
+                    )
+                    for tile in tile_id_by_edges
+                )
             )
         )
         for direction, required_color in enumerate(region.boundary[index]):
             if required_color != COLOR_NONE:
-                solver.add(
-                    Or(
-                        *(
-                            variable == tile_id
-                            for tile_id, tile in enumerate(tileset)
-                            if tile[direction] == required_color
-                        )
-                    )
-                )
-
-    for y in range(region.height):
-        for x in range(region.width):
-            index = y * region.width + x
-            variable = variables[index]
-            if variable is None:
-                continue
-
-            neighbors = []
-            if x + 1 < region.width:
-                neighbors.append((E, index + 1))
-            if y + 1 < region.height:
-                neighbors.append((S, index + region.width))
-
-            for direction, neighbor_index in neighbors:
-                neighbor = variables[neighbor_index]
-                if neighbor is None:
-                    continue
-                for tile_id, adjacent_ids in enumerate(
-                    compatibility[direction]
-                ):
-                    solver.add(
-                        Implies(
-                            variable == tile_id,
-                            Or(
-                                *(
-                                    neighbor == adjacent_id
-                                    for adjacent_id in adjacent_ids
-                                )
-                            ),
-                        )
-                    )
+                solver.add(cell_edges[direction] == required_color)
 
     status = solver.check()
     if status == sat:
         model = solver.model()
         tiling = tuple(
             None
-            if variable is None
-            else model.eval(variable, model_completion=True).as_long()
-            for variable in variables
+            if cell_edges is None
+            else tile_id_by_edges[
+                tuple(
+                    model.eval(edge, model_completion=True).as_long()
+                    for edge in cell_edges
+                )
+            ]
+            for cell_edges in edges
         )
         return TilingSolveResult(TilingSolveStatus.SAT, tiling)