WeakC4 Steady-State Lab

A static page for building, sharing, playing through and exhaustively verifying WeakC4 steady-state diagrams on the 7x6 board.

Everything runs client side. No build step, no bundler, no network access: index.html plus seven scripts, and an optional WebAssembly engine loaded on demand.

What it is for

Everything past ply 12 is already solved, so this is not a discovery tool, and nobody is going to find a new steady state by leaving a browser tab open. What it is actually good at:

Understanding the language. Play Yellow against a diagram and watch the move log name the rule that fired for each Red reply. That teaches what a steady state is faster than any prose, and needs no solving at all.

Checking a claim without a toolchain. Anyone can load a diagram and verify it exhaustively in the browser. For a result you want taken seriously, "here is a link, check it yourself" is worth more than a table of numbers.

Arguing with evidence. If someone believes a diagram works, send a link that plays out the exact line beating it. Counterexamples travel as URLs.

Human insight plus machine verification. Ply 12 and below is exactly what remains open and exactly what automated search cannot brute-force. The realistic path to anything new is a person committing to most of a diagram, marking a few cells ?, and letting the tool fill and certify the rest. That is what auto-complete is for.

What it does

Levels. Paint priority levels 0-9 across the 42 cells. Click paints the selected level; right-click marks a cell undecided. The level layer is stored separately from the stones, so adding and removing a stone in Position mode never destroys the level underneath, and levels stay visible on top of any stone played after the root.

? means undecided. It is a tool-level symbol, not a level: every level means something and the language has no blank, so there is no value that reads as "unset". Auto-complete fills exactly the undecided cells and treats every other level as fixed. A diagram containing one is incomplete and gets no verification verdict.

Play. You are Yellow, the diagram is Red. Red's replies are re-derived from the diagram on every render, so editing a level instantly re-plays the line. The move log names the rule that fired for each Red move.

Position. Click columns to build a root, or paste a move sequence.

Clicking alternates colours, which is awkward when you have a position in mind rather than a game. For those, paste the stones instead: six rows of R and Y with ? elsewhere, no levels needed. The order is derived for you, so any position reachable by some legal game will load whether or not you can see which one. Red and Yellow counts must be equal, since Red moves at the root.

Verification. Runs automatically after every edit, in a Web Worker. Red follows the diagram and every legal Yellow reply is searched. A win is a real certification. A failure is drawn onto the board as a numbered ghost line, so you can see how the diagram breaks while editing it. Simplify blanks every marker that is not load-bearing; it is computed alongside the verification, so the button reports how many it would clear before you press it, and says nothing to blank when the diagram is already minimal.

It is fast enough to run on every keystroke, typically single-digit milliseconds and rarely past a tenth of a second, so there is no re-check button. A winning diagram is the slow case; a losing one stops at its first counterexample. The 5 million node budget exists only to bound a pathological case and is never approached by a real diagram.

Auto-complete. CEGIS with a CDCL SAT solver, in a second worker. Each SAT model is a candidate diagram; the verifier turns each losing line into a clause. The board shows the live candidate with its deepest counterexample behind it.

It completes diagrams; it does not solve open roots. Roughly, on a ply-16 root: four undecided cells finish in about 20 candidates, twelve in about 560, and fourteen in about 3,900. Past about fourteen it usually will not converge. The panel reports how many cells are undecided before you start and says plainly when the scope is wide.

The saved phases are scrambled every 25 candidates. Phase saving otherwise makes each model a near neighbour of the last: measured, 59% of consecutive candidates differed in exactly one cell out of fourteen, so the search crawled through a neighbourhood while each clause it earned only ruled that neighbourhood out. Scrambling throws it elsewhere in the space, and on a ply-12 root with 14 undecided cells took the search from over fourteen minutes to about two and a half seconds. The interval barely matters, so it is diversification itself doing the work.

Share. The URL carries the position and the diagram and updates as you edit.

The heavy engine

Solve whole root runs the real research pipeline: dsat.cpp linked against CaDiCaL, compiled to WebAssembly. It is the same source the native tooling runs, not a reimplementation, so it cannot drift from it. It is loaded on demand, because it is about a megabyte.

This is a different operation from auto-complete, though it answers the same question: it holds your decided cells fixed and completes the rest. What differs is the method. dsat maps out every position the diagram could ever face and decides them together, rather than proposing a diagram and testing it, so its size is set by the game tree while auto-complete's is set by the levels. Undecide everything and its UNSAT is about the root itself, across the whole language at levels 0-9.

Whatever it returns is re-verified by the in-page verifier before being accepted, so a diagram is only kept if two independent implementations agree.

Measured against the native binary (which is built with -O3 -march=native -funroll-loops, so this is not a soft baseline), on the parity roots, levels 0-9:

root	verdict	native	wasm	ratio
7659	FOUND	16.7 s	23.2 s	1.39x
6354	UNSAT	8.5 s	6.9 s	0.81x
6261	UNSAT	7.6 s	21.0 s	2.78x
4532	FOUND	75.3 s	32.0 s	0.43x

Same verdicts everywhere; the time goes either way by up to about 3x per root. A SAT solver is branchy pointer-chasing over a contiguous heap, which is what wasm does well, and -march=native buys little there. (7659 and 6354 were both certified UNSAT in the old seven-marker language; 7659 is FOUND in this one.)

It runs in hybrid mode, not full direct. Full direct costs about 620 B per envelope state, which puts ply-14 roots near 30 GB and far past wasm32's 4 GiB ceiling. Hybrid bounds memory by construction through the cut ply and the culprit-expansion cap, so the browser can pick a budget it can honour. The cut is root_ply + 16, matching dsat_campaign.py, where 16 is the measured sweet spot.

An UNSAT from here is sound with respect to the language, but nothing in this repository independently audits it. Treat it as strong evidence rather than a settled result.

What the progress line means. The run has two phases.

Mapping positions walks everything reachable from the root down to the cut ply. The gauge under the status is the share of the state budget spent, not work completed: the engine cannot know how much is left, and a full bar means it overflowed rather than finished. This is the long phase, measured at 0.7 s at ply 16 and 8 s at ply 14, growing sharply below that.

Searching is a single SAT call, so there is no fraction-complete and no bar to draw. It is not opaque though. A dead end is a branch the solver proved impossible, and the count is the standard measure of how much ground has been ruled out. Variables settled are those fixed for good; the formula carries reachability and circuit variables as well as the 42 cells, so this is not a count of decided markers. Both only ever rise. The learnt-clause count is deliberately not shown: it falls whenever the database is reduced, which reads as the search going backwards.

Roots this size settle in zero or one refinement rounds, so there is rarely an iteration count to watch.

Where the engine comes from

engine/dsat_7x6.js and engine/dsat_7x6.wasm are committed build artifacts. The exact C++ they were compiled from is in native/ (four files; see its README). It is a read-only copy: the engine is developed in the connect4 research repository, which also holds the CaDiCaL checkout, and its build script writes native/. So this repository cannot rebuild the engine by itself, and a pull request cannot meaningfully change it.

What it can do is check it. engine/PROVENANCE.json records the hashes of the native/ sources, the CaDiCaL commit, the emscripten version and the exact build flags; tests/run_engine_test.js fails if the artifacts stop matching those hashes, or stop returning the recorded verdicts, or return a diagram that engine.js rejects.

Rebuilding, from the research repository:

git clone --depth 1 https://github.com/emscripten-core/emsdk.git ~/emsdk
cd ~/emsdk && python emsdk.py install latest && python emsdk.py activate latest
cd /path/to/connect4 && bash tools/build_wasm.sh 7 6

That compiles CaDiCaL and dsat.cpp, installs the artifacts and native/ here, rewrites PROVENANCE.json, and runs tools/wasm_parity.js, which requires the wasm and the native binary to return identical verdicts on the parity roots. A mismatch fails the build.

Two things that are not obvious:

• kitten.c, CaDiCaL's embedded sub-solver, is C rather than C++. Globbing *.cpp links cleanly right up to a wall of undefined kitten_* symbols.
• The script compiles at -O3 but links at -O2 on purpose. emscripten only runs wasm-metadce at -O3 or with a shrink level, and that one binary is blocked by some Windows Application Control policies while every other binaryen tool runs. metadce only prunes unused JS/wasm boundary exports, so skipping it costs a little size and nothing else.

No wasm-specific C++. dsat reports every result as JSON on stdout and touches no files, so the same source is compiled for both targets.

Semantics

Upstream's language since 2026-09-26 (2swap/WeakC4 26c8d14, after dave-zyx's model), exactly as solution/validate_solution.py implements it:

1. take an immediate win (lowest column);
2. otherwise block Yellow's immediate win (lowest column);
3. otherwise play the cell whose level is the lowest level held by exactly one playable cell. A level held by two or more playable cells is skipped -- a tie is never an error. If no level is unique, the diagram names no move, and that line counts as a loss.

char	meaning
0-9	priority level; 0 is strongest. The palette and the engine use these ten, as the published solution does
a-d	weaker levels upstream also accepts; they import and verify, but the engine does not search them
R Y	Red / Yellow stone at the root (upstream's spelling)
?	undecided, tool only; never fires, auto-complete fills these

Every empty cell holds some level: there is no blank. "Clear" and "Simplify" write 9, the weakest palette level, which is consulted only once every lower level in play is absent or tied. On the board a 9 cell is drawn empty, the way the old language drew claimeven, so a mostly-filled diagram shows only the levels that do work; hovering a cell still names it.

The old seven-marker language

Diagrams, JSON artifacts and share links from before the switch still load. They are translated: !->0, @->1, a live claimeven/claimodd cell->2, +->3, =->4, -->5, and an opposite-parity (inert) claim cell->9. For any diagram that verified under the old rules this plays identically: at every reachable position exactly one cell fired at the first non-empty old level, the levels keep their order, old miai (skipped unless unique) is how every level behaves now, and 9 is only consulted after a lower level would already have fired. Checked on the whole old upstream corpus: all 1,295 translations match an independent Python translation, and every re-verified one still wins. A diagram that did not verify may change verdict, because a tie that was fatal before is now skipped.

Columns are numbered 1 to 7, matching the digits in a move sequence and the "column 4" wording in the project notes. Rows count 1 to 6 from the bottom.

The board uses two ring treatments, and the legend under it names whichever are on screen: an accent ring is the move the diagram selects, a green ring is the winning four. Faded stones are a counterexample line rather than the root position, and carry their move number. Where a column would drop is shown on hover; clicking anywhere in a column plays it.

Correctness

The page's agent is a port, so it is pinned to the Python reference rather than trusted:

npm test          # all three suites, no dependencies to install

or individually:

node tests/run_crosscheck.js

against the committed fixture. That replays 4,000 random positions and diagrams through engine.js, comparing every selected move against upstream's own query_steady_state, plus 250 full exhaustive verdicts against upstream's verify_leaf, plus URL codec and importer round-trips, plus the whole pre-switch corpus through the legacy translator (matched against an independent Python translation, with a sample re-verified under the new rules). Any mismatch is a hard failure.

The fixture is generated by weakc4/gen_js_crosscheck.py in the research repository and committed here, so the test needs node and nothing else.

node tests/run_sat_tests.js

checks the SAT solver against brute force and pigeonhole instances, exercises clause deletion, and runs the synthesizer end to end. It also guards the CEGIS invariant directly: no clause may be satisfied by its own candidate, and the candidate must never repeat.

node tests/run_engine_test.js

checks that the committed WebAssembly artifacts still hash to what engine/PROVENANCE.json records, and that they still return the recorded verdicts on one UNSAT root and one root with a known diagram. Those verdicts come from the native engine; the UNSAT is not independently audited. The diagram it returns is re-verified with engine.js, so the test only passes when two independent implementations agree.

A root that already contains a four-in-a-row has no verdict to give: the game is over. verify() refuses it (ROOT_TERMINAL), as upstream's verify_leaf does.

The SAT solver

sat.js is written by hand for this page, not a vendored library. It is a standard CDCL solver in the MiniSat mould, just under 400 lines:

• two-watched-literal unit propagation
• 1UIP conflict analysis with clause learning
• VSIDS-style variable activity with rescaling, and phase saving
• Luby restarts
• LBD-based learnt clause deletion
• incremental in the one direction CEGIS needs: clauses are only ever added between solve() calls, so every learnt clause stays valid

It does not have the inprocessing that makes a modern solver fast: no vivification, no subsumption, no bounded variable elimination, no chronological backtracking. Variable selection is a linear scan rather than a heap, which is fine at 238 variables and would not be at 238,000.

It is tested rather than trusted. What ships, and what you can run yourself: 600 random 3-SAT instances checked against brute force, 150 more driven incrementally with clause deletion forced on, pigeonhole up to 7 into 6 both normally and under forced deletion, and the synthesizer end to end.

Deletion gets its own tests because it is the most dangerous code in the file. A lost watch or a clause deleted while still cited as a reason would corrupt propagation, and the default maxLearnts of 8000 means ordinary use never reaches reduceDB at all, so it would otherwise ship unexercised. A wrong UNSAT matters more than a wrong SAT here: a SAT answer is a candidate diagram that the verifier checks independently, while an UNSAT is reported to you as a conclusion.

That is reassuring, not a proof. If you need a solver you can lean on, use a real one.

Why it is not compiled to WASM

The obvious upgrade is to replace sat.js with CaDiCaL compiled for the browser. It would not help, and the measurements say why. Time spent in a CEGIS run, by workload:

workload	SAT solve	exhaustive verify	clause build
every cell undecided, ply 8 (8,919 candidates in 20 s, no solution)	86.6%	4.7%	8.7%
10 undecided on a ply-8 root (solved, 224 candidates in 0.8 s)	2.8%	91.3%	5.9%
14 undecided on a ply-12 root (solved, 3,417 candidates in 2.4 s)	55.4%	21.8%	22.8%

The bottleneck moves with the workload, and never sits somewhere a faster solver would pay off. It owns 86.6% of the first case, which is the one that does not finish anyway. It owns 2.8% of the second, where the verifier dominates and the whole run takes under a second regardless. Only the third splits its time, and even there the SAT half is barely more than the rest combined.

So a faster solver would mostly make a hopeless search fail sooner. With every cell undecided the search ran 8,919 candidates in 20 seconds without converging, and the deepest counterexample plateaued rather than trending toward a solution. The space is 7^34 and each clause removes a vanishing slice of it, so a 10x throughput gain buys one digit against a gap of many orders of magnitude. The binding constraint is how little each counterexample rules out, which is a property of the encoding rather than of the language it runs in.

That is why the panel reports how many cells are undecided before a search starts, and says plainly when the scope is too wide to expect a result. Leaving it running overnight finds nothing that a few minutes would not.

Where the search stands

The bottleneck is measured, not guessed. Each clause carries roughly 120 literals out of 224 variables, so one counterexample removes a vanishing slice of the space. Everything tried against that, and what the evidence said:

change	result
harvest 8/24/48 counterexamples, keep the shallowest	within noise on throughput and repair difficulty, and costs extra search per candidate. Left off.
learnt-clause reduction (LBD)	kept. Bounds the database, 10,550 down to 4,093 learnt clauses over the same run, and stops the decay of an unbounded DB.
an exact winning-move oracle in the clause: "at the culprit state the diagram must pick one of these winning moves" in place of "one of these ~86 cell/marker pairs must change"	median clause 86 literals down to 80, and about 6% slower for 869,618 solver calls. Reverted.
"exactly one marker fires" as a structural constraint, so an ambiguous diagram is never proposed at all	unsound as posed. Reverted.
scrambling the saved SAT phases (described under Auto-complete)	kept, and the only one that mattered.

The two clause changes are the interesting failures, because both look obviously right. The oracle misses because of what the counterexamples actually are. Over one 60-second run on a ply-12 root:

the counterexample was	count
the diagram naming no move	70,319
two or more cells firing at once	26,245
Red playing a losing move	8,454
the line drawing	1,846

90% are the diagram naming no unique move, not the diagram playing a losing one. Two thirds of the losing lines therefore have no culprit for an oracle to point at, and where there is one it sits about three quarters of the way along, so cutting there saves roughly one decision in eleven. "Was that move losing" is the right question for dsat, whose per-state encoding makes ambiguity unsatisfiable by construction, and the wrong one here.

Forbidding ambiguity structurally is the right idea, and the circuit for it is correct: pin all 42 cells to a known winning diagram, constrain every frontier it reaches, and the instance stays SAT. What fails is saying where the constraint applies. It is naturally keyed by height profile, since that is what determines the exposed cells, but the profile does not determine whether the state is quiet — on one root, 939 of 2,838 profiles reached occur as both quiet and tactical states — so it forces a unique move where the rules do not require one, and excludes valid diagrams. The synth repair test catches it at once.

Saying it properly needs a reachability variable per state, asserted only for the quiet states a diagram actually reaches. That is dsat's encoding, and dsat already exists. The weak clause is not a bug in the in-page search to be fixed by a better constraint; it is the price of an encoding with 210 variables and no state space.

The Connect 4 solver built for the oracle ships anyway: engine/c4solver_7x6.wasm, 13 KB, the same solver.hpp the research tooling uses, exposing c4_solve and c4_winning_moves and keeping its transposition table warm between calls. Measured against the native binary under the same warm-table conditions, 300 weak solves at ply 8 to 29: 12,388 ms native against 12,746 ms in the browser, 1.03x, with identical verdicts on every position. Cost is a function of depth: about 5 ms per weak solve at ply 12 and beyond, against 2.5 minutes from the empty board. Nothing in the page loads it; the test suite is what exercises it.

Both searches now answer the same question — complete the undecided cells, keep the rest — and differ in how. dsat pins the decided cells as unit clauses, which costs it nothing: its size is set by the game tree, and the markers do not constrain the game tree. The in-page search encodes only the markers, so every cell you decide makes its problem smaller. That is why the choice between them is really a question about the root, not about the diagram.

So treat the in-page search as a diagram completer, not a solver: on a ply-16 root, four undecided cells solve in about 20 candidates and twelve in about 560, while a root with everything undecided does not converge at all.

An UNSAT verdict here is sound with respect to the clauses it accumulated, but it is not an audited impossibility proof, and it is bounded by whichever markers you pinned. Say what it covers if you report it.

Layout

The page is built to fit one screen. The board scales to the viewport rather than being a fixed size: its max-width derives from 100dvh, and because cells are square, bounding the width bounds the height. Level glyphs scale with it through container query units. Below a usable cell size the board stops shrinking and the page scrolls instead.

On a narrow screen the columns stack, the palette drops its labels to keep its two rows of five, and the page scrolls vertically. Explanatory prose sits in collapsed details blocks so it costs no height until asked for.

Browser support

Uses :has(), container query units, color-mix() and 100dvh. That means Chrome/Edge 111+, Safari 16.4+, Firefox 121+. Older browsers will render the board but lose some of the cell styling.

Keyboard support is partial. Every control is a real button, digits 1 to 7 play a column in Play mode, digits 0 to 9 pick that level in Levels mode, and Backspace undoes. Painting a level onto a particular cell is mouse only: the cells are not focusable and there is no arrow-key selection. That is a known gap rather than a decision.

Running it

Any static host works. Locally:

python -m http.server 8765

then open http://localhost:8765. Opening index.html from the file system mostly works, but browsers block Workers on file://, so verification falls back to the main thread and the search is unavailable.

GitHub Pages

The page sits at the repository root, so Settings > Pages > deploy from branch, main, / (root) serves it as is. All asset paths are relative, so it works from a project subpath such as user.github.io/repo/.

Nothing here is generated from research data: no diagram library, no solution artifacts, no graph. tests/crosscheck.json is a random-position test fixture, not research output, and is only needed by the node tests.

License

MIT, see LICENSE.

engine/ contains compiled code from CaDiCaL and from emscripten, both permissively licensed. Their license texts are reproduced verbatim in THIRD_PARTY_LICENSES.md.

The steady-state idea is 2swap's, from WeakC4; the numeric language it now uses is dave-zyx's. This page reimplements upstream's validate_solution.py semantics from reading it; no code was copied, and the test suite pins the two together case by case.

Files

file	role
index.html	markup
style.css	styling, light and dark
engine.js	board mechanics, the agent, exhaustive verifier, URL codec, importer and legacy translator
sat.js	CDCL SAT solver
synth.js	CEGIS encoding and loop
app.js	UI
verify.worker.js	verification and simplification off the main thread
synth.worker.js	synthesis off the main thread
dsat.worker.js	the WebAssembly engine, off the main thread
engine/	compiled engines and their provenance: dsat for whole roots, c4solver for game-tree queries
native/	read-only snapshot of the C++ dsat is compiled from; not used by the page (see its README)
tests/	node test runners and the Python-generated fixture
.github/workflows/ci.yml	runs every test suite on each pull request
LICENSE	MIT
THIRD_PARTY_LICENSES.md	CaDiCaL and emscripten, verbatim