Browser solver 0.3.0

What's Changed

• Bump astral-sh/setup-uv from 10.1.0 to 10.2.0 by @dependabot[bot] in #31

Full Changelog: solver-web-v0.1.0...solver-web-v0.3.0

Browser solver 0.1.0

Full Changelog: v1.0.0...solver-web-v0.1.0

v1.0.0 — Exam Ready

v1.0.0 — Exam Ready

Tiling Foundry implements the Yang–Zhang 23-Wang-tile construction with reference and optimized serial solvers, Boolean and Wang Z3 oracles, independent witness checks, and shared figures and PDF dossiers. This release adds a documented setup and offline demonstration path for new CM1-in-3 inputs.

Run the release

Install the Linux prerequisites, then:

git clone --branch v1.0.0 --depth 1 https://github.com/xtraid/tiling-foundry.git
cd tiling-foundry
make demo-setup
make demo-check
make demo INPUT=tests/instances/demo_sat.cm13 TIMEOUT=300
make demo INPUT=tests/instances/pipeline_unsat_search.cm13 TIMEOUT=300

Setup needs a C17 compiler, make, Git, Python 3.11+, uv, and pdfLaTeX. It prepares separate locked core and renderer environments; the renderer uses Python 3.14. Debian 13 and Arch Linux/Omarchy have been exercised. Arch requires texlive-latex for pdfLaTeX and the report packages. No GPU or global pip installation is required.

The first setup needs network access. Keep both environments and the uv-managed Python interpreter installed for offline use. The two demo commands use the installed environments without downloads. Each invocation retains a new diagnostic directory; the PDF path is printed after successful validation. For an input of your own, use make demo INPUT='path/to/new formula.cm13' TIMEOUT=300.

What changed

• make demo-setup checks the native compiler and real PDF template, synchronizes both lockfiles, builds the shared library and verifies Z3, fonts and rendering.
• make demo copies and hashes a new input, captures each of the four engines once and produces a complete dossier with figures and PDF from that capture.
• make demo-check narrates six checks: valid parsing, domain rejection, SAT witness validation, a known UNSAT case, engine agreement, and rejection of an altered witness.
• The demo keeps logs and input copies on failure and handles timeout and interruption across its child processes.
• Dense routing labels, contact sheets and narrow-region trace figures have been corrected. The README, presentation and dossier guide explain the commands and evidence boundaries; CI exercises the documented setup and demo.

Correctness and compatibility

SAT means the returned witnesses passed independent checks. UNSAT means the four engines agreed on that terminal result; the trace is diagnostic evidence, not an independent UNSAT certificate. Timeout, cancellation, UNKNOWN, disagreement, errors and incomplete traces never substitute for UNSAT.

For new inputs, expected_status is null and the recorded engine agreement drives presentation. Known cases retain their supplied expectation as an additional assertion. Updated readers accept earlier v2 dossiers; earlier strict readers reject the nullable variant. Dossier v1, the C core, ABI and independent oracles remain unchanged by this release branch.

Verification and limits

Preparation included isolated setup, offline SAT/UNSAT runs with input/hash and bundle validation, complete PDF review, process/error tests, renderer and documentation checks, and an Omarchy rehearsal. The final corrected UNSAT PDF was opened and fully read on Omarchy at commit 0215b73; that run took 66.289 seconds. This is pre-release environment evidence and is distinct from verification of the public tag.

Linux is the supported platform; Windows and macOS are not supported. Completion time is not guaranteed for arbitrary inputs. The default global timeout is 300 seconds, and each native trace is limited to 100000 events. Wide region overviews require PDF zoom or the original PNGs. Parallel solving remains future work.

See the dossier guide for the input format, complete-output rules and diagnostic options.