道場 · dojo
SAT-Dojo
Ein Fitnessstudio für SAT-Solver. Kompilier deinen Solver zu WebAssembly, reich ihn ein, und er wird auf einem geheimen Satz frischer Formeln bewertet: Hashi-Rätsel, Paritätsfallen, zufälliges 3-SAT, Tauben und Damen.
Rangliste 番付 · banzuke
Mittlerer Treibstoff pro Formel in Milliarden, ungelöste Formeln zählen das doppelte Budget. Weniger ist besser.
Lädt…
So funktioniert’s 稽古 · keiko
一Bauen
Jede Sprache, die nach WASI Preview 1 kompiliert, funktioniert: Rust, C und C++ mit wasi-sdk, Zig, Go. Lies DIMACS von stdin und antworte wie in der 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二Trainieren
Bewerte deinen Solver lokal auf dem öffentlichen Dev-Set mit dem Dojo-Tool. Es läuft genau wie die Rangliste, so kennst du deine Punktzahl schon vor dem Einreichen.
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三Einreichen
Lade die .wasm-Datei hoch. Sie läuft auf dem geheimen Satz der aktuellen Saison, auf unserer eigenen Maschine.
四Aufsteigen
Der niedrigste PAR-2 gewinnt: der mittlere Treibstoff pro Formel, wobei ungelöste Formeln das doppelte Budget zählen.
Die Formeln
Hashi
Hashiwokakero-Rätsel von 10×10 bis 28×28 als CNF, ohne die Zusammenhangsregel. Immer erfüllbar.
Hashi-Parität
Rätsel, in denen eine Zahl geändert wurde, sodass die Summe ungerade ist. Unerfüllbar, denn jede Brücke zählt doppelt. Leicht zu sehen, schwer per Resolution zu beweisen.
Zufälliges 3-SAT
Gleichverteiltes zufälliges 3-SAT am Phasenübergang, 4,26 Klauseln pro Variable, etwa die Hälfte davon erfüllbar.
Schubfach
n+1 Tauben in n Löchern: der Klassiker, der exponentiell lange Resolutionsbeweise braucht. Dazu ein paar, bei denen es aufgeht.
Damen
N Damen auf Brettern bis 48×48 mit ein paar verbotenen Feldern.
Betritt das Dojo 入門 · nyūmon
Lädt…
Fair Play 礼 · rei
Treibstoff statt Sekunden
Jede ausgeführte WebAssembly-Instruktion kostet eine Einheit Treibstoff, Bulk-Memory-Operationen eine pro Byte. Uhren und Zufallszahlen sind fest geseedet, also bekommt ein Solver auf jeder Maschine jedes Mal dieselbe Punktzahl.
Geheime, frische Formeln
Das Test-Set entsteht aus einem geheimen Seed, der sich jede Saison ändert, und jede Formel wird verwürfelt: Variablen umbenannt und negiert, Klauseln gemischt. Ergebnisse gibt es nur pro Familie, nie pro Formel.
Jede Antwort geprüft
Modelle werden gegen die Formel geprüft. UNSAT zählt nur, wo wir einen Beweis haben: Schubfach und Hashi-Parität sind konstruktionsbedingt unerfüllbar, jedes andere UNSAT-Label kommt mit einem DRAT-Beweis, den unser eigener Checker verifiziert hat. Eine einzige falsche Antwort disqualifiziert die Einreichung, Raten lohnt sich also nie.
Eine versiegelte Sandbox
Keine Dateien, kein Netzwerk, keine Umgebungsvariablen. Speicher und Ausgabe sind begrenzt, und Einreichungen laufen auf einer separaten Maschine ohne Daten.
Ein Konto, bester Eintrag
Konten müssen einen Tag alt sein, um einzureichen, und es gibt drei Einreichungen am Tag pro Konto und pro Netzwerk. Identischer Code wird abgelehnt, auch umbenannt oder aufgefüllt, und nur deine beste Einreichung kommt in die Wertung.
Keine Kopien
Die Punktzahlen sind exakt, also hinterlässt ein Solver einen Fingerabdruck: den Treibstoff, den er für jede einzelne Formel braucht. Eine Einreichung, die sich wie eine frühere einer anderen Person verhält, kommt nicht in die Wertung. Wer eine Kopie so weit ändert, dass sie dem entgeht, hat einen anderen Solver gebaut, und sie langsamer zu machen bringt sie nur hinter das Original.
Saisons
Eine neue Saison bringt ein neues geheimes Test-Set, und jede Einreichung wird neu bewertet.
Für Forschende
Treibstoff ist deterministisch, also sind Ergebnisse reproduzierbar und zwischen Papers vergleichbar: Nenn die Saison und den Dev-Seed. Die Rangliste gibt es als JSON unter /dojo/board.json, das Test-Harness ist Open Source.