道場 · dojo
SAT Dojo
A gym for SAT solvers. Compile yours to WebAssembly, submit it, and it is scored on a hidden set of fresh formulas: Hashi puzzles, parity traps, random 3-SAT, pigeons and queens.
Leaderboard 番付 · banzuke
Mean fuel per formula in billions, unsolved formulas count twice the budget. Lower is better.
Loading…
How it works 稽古 · keiko
一Build
Any language that compiles to WASI preview 1 works: Rust, C and C++ with wasi-sdk, Zig, Go. Read DIMACS on stdin and answer like in the SAT competition.
$ cargo build --release --target wasm32-wasip1
stdin p cnf 3 2
1 -2 0
2 3 0
stdout s SATISFIABLE
v 1 2 -3 0二Train
Score your solver locally on the public dev set with the dojo tool. It runs exactly like the leaderboard, so you know your score before you submit.
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三Submit
Upload the .wasm file. It runs on the hidden set of the current season, on our own machine.
四Climb
The lowest PAR-2 wins: the mean fuel per formula, where unsolved formulas count twice the budget.
The formulas
Hashi
Hashiwokakero puzzles from 10×10 to 28×28 as CNF, without the connectivity rule. Always satisfiable.
Hashi parity
Puzzles with one number changed so the numbers add up to an odd sum. Unsatisfiable, since every bridge adds two. Easy to see, hard to prove by resolution.
Random 3-SAT
Uniform random 3-SAT at the phase transition, 4.26 clauses per variable, about half of them satisfiable.
Pigeonhole
n+1 pigeons in n holes: the classic that needs exponentially long resolution proofs. Plus a few that do fit.
Queens
N queens on boards up to 48×48 with a few forbidden squares.
Enter the dojo 入門 · nyūmon
Loading…
Fair play 礼 · rei
Fuel, not seconds
Every executed WebAssembly instruction costs one unit of fuel, bulk memory operations one per byte. Clocks and random numbers are seeded, so a solver gets the same score on every machine, every time.
Hidden, fresh formulas
The test set comes from a secret seed that changes every season, and every formula is scrambled: variables renamed and negated, clauses shuffled. Results are shown per family only, never per formula.
Every answer checked
Models are verified against the formula. UNSAT counts only where we have a proof: pigeonhole and Hashi parity are unsatisfiable by construction, every other UNSAT label comes with a DRAT proof our own checker verified. A single wrong answer disqualifies the submission, so guessing never pays.
A sealed sandbox
No files, no network, no environment. Memory and output are capped, and submissions run on a separate machine that holds no data.
One account, best entry
Accounts have to be a day old to submit, and there are three submissions a day per account and per network. Identical code is refused, even renamed or padded, and only your best submission is ranked.
No copies
Scores are exact, so a solver leaves a fingerprint: the fuel it uses on every formula. A submission that behaves like an earlier one by someone else isn't ranked. Changing a copy enough to escape that makes it a different solver, and making it slower only puts it below the original.
Seasons
A new season brings a new hidden set and every submission is evaluated again.
For researchers
Fuel is deterministic, so results are reproducible and comparable between papers: name the season and the dev seed. The leaderboard is available as JSON at /dojo/board.json, the harness is open source.