道場 · dojo
SAT Dojo
Een sportschool voor SAT-solvers. Compileer de jouwe naar WebAssembly, stuur hem in en hij wordt beoordeeld op een geheime set verse formules: Hashi-puzzels, pariteitsvallen, random 3-SAT, duiven en koninginnen.
Ranglijst 番付 · banzuke
Gemiddelde brandstof per formule in miljarden, onopgeloste formules tellen voor twee keer het budget. Lager is beter.
Laden…
Zo werkt het 稽古 · keiko
一Bouwen
Elke taal die naar WASI preview 1 compileert werkt: Rust, C en C++ met wasi-sdk, Zig, Go. Lees DIMACS van stdin en antwoord zoals in de 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二Trainen
Beoordeel je solver lokaal op de openbare devset met de dojo-tool. Die werkt precies zoals de ranglijst, dus je kent je score al voordat je instuurt.
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三Insturen
Upload het .wasm-bestand. Het draait op de geheime set van het huidige seizoen, op onze eigen machine.
四Klimmen
De laagste PAR-2 wint: de gemiddelde brandstof per formule, waarbij onopgeloste formules voor twee keer het budget tellen.
De formules
Hashi
Hashiwokakero-puzzels van 10×10 tot 28×28 als CNF, zonder de samenhangsregel. Altijd vervulbaar.
Hashi-pariteit
Puzzels waarin één getal is veranderd zodat de som oneven is. Onvervulbaar, want elke brug telt twee keer mee. Makkelijk te zien, moeilijk te bewijzen met resolutie.
Random 3-SAT
Uniform random 3-SAT bij de faseovergang, 4,26 clausules per variabele, ongeveer de helft vervulbaar.
Duiventil
n+1 duiven in n hokjes: de klassieker die exponentieel lange resolutiebewijzen nodig heeft. Plus een paar waarbij het wel past.
Koninginnen
N koninginnen op borden tot 48×48 met een paar verboden velden.
Betreed de dojo 入門 · nyūmon
Laden…
Fair play 礼 · rei
Brandstof, geen seconden
Elke uitgevoerde WebAssembly-instructie kost één eenheid brandstof, bulk-geheugenoperaties één per byte. Klokken en willekeurige getallen hebben een vaste seed, dus een solver krijgt op elke machine telkens dezelfde score.
Geheime, verse formules
De testset komt uit een geheime seed die elk seizoen verandert, en elke formule wordt door elkaar gehusseld: variabelen hernoemd en geïnverteerd, clausules geschud. Resultaten worden alleen per familie getoond, nooit per formule.
Elk antwoord gecontroleerd
Modellen worden tegen de formule gecontroleerd. UNSAT telt alleen waar we een bewijs hebben: duiventil en Hashi-pariteit zijn per constructie onvervulbaar, elk ander UNSAT-label komt met een DRAT-bewijs dat onze eigen checker heeft geverifieerd. Eén fout antwoord diskwalificeert de inzending, gokken loont dus nooit.
Een verzegelde sandbox
Geen bestanden, geen netwerk, geen omgevingsvariabelen. Geheugen en uitvoer zijn begrensd, en inzendingen draaien op een aparte machine zonder gegevens.
Eén account, beste inzending
Accounts moeten een dag oud zijn om in te sturen, en er zijn drie inzendingen per dag per account en per netwerk. Identieke code wordt geweigerd, ook hernoemd of opgevuld, en alleen je beste inzending komt in de ranglijst.
Geen kopieën
Scores zijn exact, dus een solver laat een vingerafdruk achter: de brandstof die hij op elke formule verbruikt. Een inzending die zich gedraagt als een eerdere van iemand anders komt niet in de ranglijst. Wie een kopie genoeg verandert om daaraan te ontsnappen, heeft een andere solver gemaakt, en hem trager maken zet hem alleen onder het origineel.
Seizoenen
Een nieuw seizoen brengt een nieuwe geheime set en elke inzending wordt opnieuw beoordeeld.
Voor onderzoekers
Brandstof is deterministisch, dus resultaten zijn reproduceerbaar en vergelijkbaar tussen papers: noem het seizoen en de dev-seed. De ranglijst is als JSON beschikbaar op /dojo/board.json, de harness is open source.