From c5fe8dbad88523a35d4cf90a0ddfb5846024f43a Mon Sep 17 00:00:00 2001 From: Manuel Magnabosco Date: Mon, 24 Aug 2026 23:49:18 +0200 Subject: [PATCH] Refactor Wang Z3 around shared edge terms --- README.md | 13 +- docs/development_principles.md | 11 +- docs/solver_comparison_benchmark.md | 8 +- docs/wang_z3_edge_table_2026-08-24.md | 120 ++++++++++++++++++ python/oracles/tiling_solver.py | 126 +++++++++---------- tests/python/test_tiling_oracle.py | 167 ++++++++++++++++++++++++++ 6 files changed, 371 insertions(+), 74 deletions(-) create mode 100644 docs/wang_z3_edge_table_2026-08-24.md diff --git a/README.md b/README.md index 61c0446..6f5d9d1 100644 --- a/README.md +++ b/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 diff --git a/docs/development_principles.md b/docs/development_principles.md index 7651883..b7b1053 100644 --- a/docs/development_principles.md +++ b/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 diff --git a/docs/solver_comparison_benchmark.md b/docs/solver_comparison_benchmark.md index a82774f..505f5a7 100644 --- a/docs/solver_comparison_benchmark.md +++ b/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. diff --git a/docs/wang_z3_edge_table_2026-08-24.md b/docs/wang_z3_edge_table_2026-08-24.md new file mode 100644 index 0000000..75fb933 --- /dev/null +++ b/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. diff --git a/python/oracles/tiling_solver.py b/python/oracles/tiling_solver.py index 7e9a806..a685ea1 100644 --- a/python/oracles/tiling_solver.py +++ b/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) diff --git a/tests/python/test_tiling_oracle.py b/tests/python/test_tiling_oracle.py index a747aa8..d5baeba 100644 --- a/tests/python/test_tiling_oracle.py +++ b/tests/python/test_tiling_oracle.py @@ -1,4 +1,8 @@ +from itertools import product import unittest +from unittest.mock import Mock, patch + +from z3 import unknown from model.region import Region from model.tileset import ( @@ -8,15 +12,21 @@ COLOR_NONE, COLOR_V, COLOR_V0_A, + E, + N, + S, TILESET, TILE_F0, TILE_F1, TILE_L0, + Tileset, + W, ) from oracles.tiling_check import is_valid_tiling from oracles.tiling_solver import ( TilingSolveResult, TilingSolveStatus, + _edge_terms, solve_tiling, ) @@ -24,6 +34,26 @@ NO_BOUNDARY = (COLOR_NONE, COLOR_NONE, COLOR_NONE, COLOR_NONE) +def _is_brute_force_sat(region: Region, tileset: Tileset) -> bool: + active_indices = tuple( + index for index, active in enumerate(region.active) if active + ) + for selected_tiles in product( + range(len(tileset)), + repeat=len(active_indices), + ): + tiling: list[int | None] = [None] * len(region.active) + for index, tile_id in zip( + active_indices, + selected_tiles, + strict=True, + ): + tiling[index] = tile_id + if is_valid_tiling(region, tileset, tiling): + return True + return False + + class TilingSolveResultTests(unittest.TestCase): def test_carries_a_tiling_only_for_sat(self) -> None: tiling = (7, None) @@ -113,6 +143,51 @@ def test_does_not_match_across_inactive_cells(self) -> None: class TilingSolverTests(unittest.TestCase): + def test_shares_exactly_the_active_internal_edge_terms(self) -> None: + region = Region( + width=2, + height=2, + active=(True,) * 4, + boundary=(NO_BOUNDARY,) * 4, + ) + + edges = _edge_terms(region) + top_left = edges[0] + top_right = edges[1] + bottom_left = edges[2] + bottom_right = edges[3] + assert top_left is not None + assert top_right is not None + assert bottom_left is not None + assert bottom_right is not None + + self.assertIs(top_left[E], top_right[W]) + self.assertIs(top_left[S], bottom_left[N]) + self.assertIs(top_right[S], bottom_right[N]) + self.assertIs(bottom_left[E], bottom_right[W]) + + def test_does_not_share_constraints_across_an_inactive_cell(self) -> None: + all_b = (COLOR_B, COLOR_B, COLOR_B, COLOR_B) + all_v = (COLOR_V, COLOR_V, COLOR_V, COLOR_V) + tileset = (all_b, all_v) + region = Region( + width=3, + height=1, + active=(True, False, True), + boundary=( + (COLOR_NONE, COLOR_NONE, COLOR_NONE, COLOR_B), + NO_BOUNDARY, + (COLOR_NONE, COLOR_V, COLOR_NONE, COLOR_NONE), + ), + ) + + result = solve_tiling(region, tileset) + + self.assertEqual(result.status, TilingSolveStatus.SAT) + self.assertEqual(result.tiling, (0, None, 1)) + self.assertIsNotNone(result.tiling) + self.assertTrue(is_valid_tiling(region, tileset, result.tiling)) + def test_solves_a_single_forced_tile(self) -> None: region = Region( width=1, @@ -192,6 +267,98 @@ def test_reports_unsat_for_forced_adjacency_mismatches(self) -> None: self.assertEqual(result.status, TilingSolveStatus.UNSAT) self.assertIsNone(result.tiling) + def test_matches_brute_force_on_small_generic_tilesets(self) -> None: + generic_tileset = ( + (COLOR_B, COLOR_B, COLOR_B, COLOR_B), + (COLOR_B, COLOR_V, COLOR_B, COLOR_V), + (COLOR_V, COLOR_B, COLOR_V, COLOR_B), + (COLOR_B, COLOR_B, COLOR_B, COLOR_B), + ) + regions = ( + Region( + width=2, + height=1, + active=(True, True), + boundary=(NO_BOUNDARY, NO_BOUNDARY), + ), + Region( + width=2, + height=1, + active=(True, True), + boundary=( + (COLOR_NONE, COLOR_NONE, COLOR_NONE, COLOR_B), + (COLOR_NONE, COLOR_V, COLOR_NONE, COLOR_NONE), + ), + ), + Region( + width=1, + height=2, + active=(True, True), + boundary=( + (COLOR_B, COLOR_NONE, COLOR_NONE, COLOR_NONE), + (COLOR_NONE, COLOR_NONE, COLOR_V, COLOR_NONE), + ), + ), + Region( + width=3, + height=1, + active=(True, False, True), + boundary=(NO_BOUNDARY,) * 3, + ), + ) + + for region in regions: + with self.subTest( + width=region.width, + height=region.height, + active=region.active, + ): + result = solve_tiling(region, generic_tileset) + expected = _is_brute_force_sat(region, generic_tileset) + + self.assertEqual( + result.status is TilingSolveStatus.SAT, + expected, + ) + if result.tiling is not None: + self.assertTrue( + is_valid_tiling(region, generic_tileset, result.tiling) + ) + + def test_returns_an_equivalent_id_for_duplicate_tiles(self) -> None: + duplicated_tile = (COLOR_B, COLOR_0, COLOR_B, COLOR_0) + tileset = (duplicated_tile, duplicated_tile) + region = Region( + width=1, + height=1, + active=(True,), + boundary=((COLOR_B, COLOR_0, COLOR_B, COLOR_0),), + ) + + result = solve_tiling(region, tileset) + + self.assertEqual(result.status, TilingSolveStatus.SAT) + self.assertIn(result.tiling, ((0,), (1,))) + self.assertIsNotNone(result.tiling) + self.assertTrue(is_valid_tiling(region, tileset, result.tiling)) + + def test_preserves_unknown_without_requesting_a_model(self) -> None: + solver = Mock() + solver.check.return_value = unknown + region = Region( + width=1, + height=1, + active=(True,), + boundary=(NO_BOUNDARY,), + ) + + with patch("oracles.tiling_solver.Solver", return_value=solver): + result = solve_tiling(region, TILESET) + + self.assertEqual(result.status, TilingSolveStatus.UNKNOWN) + self.assertIsNone(result.tiling) + solver.model.assert_not_called() + def test_rejects_invalid_tileset_storage(self) -> None: region = Region( width=1,