Presentazione

How does a formula become a region, how does search find or rule out a tiling, and how is a returned SAT witness checked? This tour answers those questions with the implemented construction and recorded solver states. To produce a report for a new formula, use the demo guide. The pipeline gives the component map; Reference holds the detailed specifications.

Construction → native solver → verification → worked result.

Yang–Zhang construction

φ SAT ⇔ Rφ tileable with the fixed 23-tile set. This equivalence comes from the Yang–Zhang reduction. The project implements its construction and tests the resulting software; those tests do not replace the mathematical proof. The view below shows the constructed region for the same small SAT instance used by the solver examples.

Read the colored spans from left to right: a variable chooses a Boolean value; forwarders preserve it; crossovers reorder signals without changing their values; each clause requires exactly one true occurrence. The source and target rows show where each signal goes, not a chosen assignment.

Construction animation → · Reduction statement and proof details →.

Native solver

Domains → propagation → MRV and decision → conflict and rollback → verified SAT.

Domains and boundary

A domain is the set of tiles still permitted at an active cell. DIDACTIC notation (these three cells are not an observed trace):

State	Candidate tiles	Meaning
Unresolved	D(a) = {2,5,8}	Three choices remain
Singleton	D(b) = {4}	One tile is fixed
Conflict	D(c) = {}	This active cell has no candidate

Boundary restriction intersects each exposed cell’s domain with the tiles matching its prescribed boundary colors. The recorded root already contains those restrictions; it does not show a before-boundary state. Inactive cells are outside the problem: their zero masks are not conflicts.

Propagation

In the canonical SAT capture, cell 0 supports east-edge colors 2 and 3. Its neighbor, cell 1, loses tiles 0 and 3: neither has a supported west edge. The neighbor’s domain shrinks from eight candidates to six.

Propagation only removes unsupported candidates. At a fixed point, the queue is empty and local constraints cannot remove more; unresolved cells may remain. Technical details → propagation.

MRV and decision

Each number below is the number of candidate tiles remaining in an active cell. Green cells are singleton domains; purple cells tie for the smallest unresolved domain. MRV selects cell 0, highlighted in yellow: its domain has two candidates, and row-major order breaks the tie among 363 cells.

Singleton cells are not MRV candidates. A decision tries one remaining tile; propagation removes candidates without making another DFS choice. Technical details → MRV.

Conflict and rollback

Separate search-UNSAT capture, reference solver. The SAT example above has no backtracking. Here, after the depth-one choice reaches a fixed point, the next DFS frame selects cell 492 with D(492) = {0,3}. Its saved state has recorded change marker 3990; it tries tile 0. The table follows two cells:

Branch state	D(492)	D(614)
Before the choice	{0,3}	{6,8}
Tile 0 applied	{0}	{6,8}
Propagation fails	{0}	{}
Rollback completed	{0,3}	{6,8}
Next candidate applied	{3}	{6,8}

1. Apply the decision. The yellow outline marks cell 492, at the left of the third row from the bottom. Its two-candidate domain becomes a singleton.

2. Propagate to an empty domain. Later in the same branch, cell 614 loses its last tile. This restriction follows from edge compatibility.

3. Record the conflict. A failed candidate is not yet an UNSAT result: the DFS frame still has tile 3 to try.

4. Restore the saved state. Rollback reverses 124 trail entries, affecting 122 cells, from recorded marker 4114 back to 3990. Some cells changed more than once. Every domain now equals its value immediately before this choice; the depth-one decision remains in place.

5. Try the next candidate. The existing DFS frame next chooses tile 3 at cell 492. This picture records the choice before its domain reduction; the following event applies {3} and propagation resumes.

The explicit stack retains each frame’s cell, remaining candidates and entry marker. It descends after successful propagation, or unwinds exhausted frames. The complete capture finishes UNSAT after all branches; this excerpt is observed diagnostic evidence, not an UNSAT certificate. Technical details → iterative DFS and undo trail.

Technical provenance of the branch excerpt

Source: pipeline_unsat_search.cm13, reference solver, complete 4,370-event search-UNSAT capture. The five images use zero-based sequences 3995, 4118, 4120, 4121 and 4122; image headings count events from one. The before-state is sequence 3993, decision 3994 saves marker 3990, and sequence 4123 applies the next candidate. Replay confirms that states 3993 and 4121 are identical. Displayed trace markers include the initial-propagation prefix; they are not live C trail offsets, which restart from zero when search begins.

Source formula · Trace manifest, snapshots and SHA-256 identities.

Verified SAT

Return to the canonical SAT example: all active domains are singleton.

Singleton domains → extract tile IDs → independent verifier → publish SAT.

The verifier checks every active placement, exposed boundary and shared edge directly from the tileset. A rejected candidate produces ERROR. The checked tiling can then be shown as a Wang witness. Technical details → SAT publication.

Verification dependencies

The formula reaches Boolean Z3 directly. Yang–Zhang supplies one shared region and tileset to both native paths and Wang Z3. Reference and optimized use the same native core; the two Z3 encodings use the same Z3 library.

Boolean Z3 bypasses the reduction; Wang Z3 bypasses native search. Independent checks validate returned SAT witnesses. UNSAT has no witness to check, and an observed UNSAT trace is not a certificate. Named checks and receipts → · Full dependency and trust boundaries →.

One solved example

Three variables, three clauses → Boolean SAT → Yang–Zhang region → native SAT → independent checks → verified Wang witness → optional generalized / hex.

Open the worked SAT example →. Its existing enlarged panels show this complete sequence on one capture, including all six passing receipts. Square, generalized and hex are views of the checked witness. The search-UNSAT rollback excerpt above remains separate.

Optimized: six implementation mechanisms

The solver semantics stay the same. The six-panel visual summary shows growing stack storage, initial trail omission, verified-domain ownership transfer, byte support lookup, queue deduplication and lazy MRV indexing. Each panel identifies the private state or work it changes; measured performance remains in Evidence.