Optimized native solver

What it is

The optimized solver is a second public native entry point over the same Wang search core. It selects six private serial mechanisms while retaining the reference path’s inputs, outputs, search meaning, and mandatory verification.

Why it exists

Performance work needs isolated mechanisms, direct counters, and a stable baseline. Keeping this path beside the reference solver makes equivalence and regressions testable without turning measured choices into universal claims.

Inputs and outputs

The input and public result contracts match the reference path: immutable region and tileset, optional initial domains, SAT with caller-owned witness, UNSAT, or ERROR. Optional metrics count direct work and storage; optional trace records the actual optimized invocation.

Mechanism

The retained mechanisms are a geometrically growing DFS stack, omission of non-consumable initial trail entries, transfer of verified SAT domains, byte-wise support tables, queue deduplication, and a private lazy MRV index. Each has separate evidence and preserves row-major tie breaking.

Primary animation

optimized_trace is the primary observed asset. optimized_mechanisms is a secondary didactic overview; it makes no timing or speedup claim.

Observed optimized domain states at root, propagation, decision, search, and result milestones. — **observed.** Selected semantic milestones from the complete optimized trace. Open the static contact sheet. Source contract: `wang-explain-manifest-v3`.

Seven didactic frames show stack, trail, ownership, byte-support, queue, and lazy-MRV state, ending with a static summary. — **didactic.** Six concrete panels show the retained serial mechanisms and their private state changes. Open the static contact sheet. Source contract: `wang-optimized-mechanisms-v1`.

Open the six-mechanism summary at full size.

Position in the pipeline

This is an independent invocation on the same reduction consumed by the reference solver and Wang Z3. Its result joins them at agreement and verification; neither trace nor metrics are used as solver input.

Observed example

The pipeline_sat.cm13 optimized run returns a checked SAT witness with a complete trace. The separately named search-UNSAT capture in the dossier index exercises conflict, backtrack, and exhaustion without becoming a second canonical story.

Trust boundary

Correctness comes from status equivalence, checked witnesses, differential tests, and the independent verifier. The observed trace describes one run; the didactic mechanism asset does not establish performance. Dated reports remain scoped to their corpus and environment.

Artifacts and references

Start with the optimization methodology and serial solver reference. The six accepted reports are collected in the evidence index.