道場 · dojo
SAT道場
SAT 求解器的健身房。把你的求解器編譯成 WebAssembly 並提交，它會在一組隱藏的全新公式上評分：數橋謎題、奇偶陷阱、隨機 3-SAT、鴿籠和皇后。
排行榜 番付 · banzuke
每個公式的平均燃料（單位：十億），未解出的公式以預算的兩倍計。越低越好。
載入中…
運作方式 稽古 · keiko
一建置
任何能編譯成 WASI preview 1 的語言都可以：Rust、搭配 wasi-sdk 的 C 和 C++、Zig、Go。從標準輸入讀取 DIMACS，並依照 SAT 競賽的格式作答。
$ 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二訓練
用 dojo 工具在公開的開發集上於本機為求解器評分。它的執行方式和排行榜完全相同，提交前就能知道分數。
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三提交
上傳 .wasm 檔案。它會在我們自己的機器上，以本季的隱藏測試集執行。
四攀升
PAR-2 最低者勝出：也就是每個公式的平均燃料，未解出的公式以預算的兩倍計。
公式
數橋
從 10×10 到 28×28 的數橋謎題編碼成的 CNF，不含連通性規則。一定可滿足。
數橋奇偶
改動一個數字、讓數字總和變成奇數的謎題。每座橋都會讓總和加二，所以不可滿足。一眼就看得出來，用歸結卻很難證明。
隨機 3-SAT
位於相變點的均勻隨機 3-SAT，每個變數 4.26 個子句，大約一半可滿足。
鴿籠
n+1 隻鴿子放進 n 個籠子：需要指數長度歸結證明的經典問題。另外還有幾個剛好放得下的。
皇后
最大 48×48 棋盤上的 N 皇后問題，附帶幾個禁用格。
踏入道場 入門 · nyūmon
載入中…
公平競賽 礼 · rei
看燃料，不看秒數
每執行一道 WebAssembly 指令消耗一單位燃料，批次記憶體操作則每位元組一單位。時鐘和亂數都有固定種子，所以同一個求解器在任何機器上、任何時候都會拿到相同分數。
隱藏的全新公式
測試集由每季更換的祕密種子產生，每個公式都經過打亂：變數重新命名並取反，子句重新排序。結果只依類別顯示，絕不逐一公式顯示。
每個答案都會驗證
模型會代入公式驗證。UNSAT 只在我們有證明時才算數：鴿籠和數橋奇偶在建構上就不可滿足，其他每個 UNSAT 標籤都附有經我們自己的檢查器驗證過的 DRAT 證明。只要答錯一次，提交就會被取消資格，所以亂猜絕對不划算。
密封的沙盒
沒有檔案、沒有網路、沒有環境變數。記憶體和輸出都有上限，提交會在一台不存放任何資料的獨立機器上執行。
一個帳號，只計最佳
帳號註冊滿一天才能提交，每個帳號和每個網路每天各可提交三次。完全相同的程式碼會被拒絕，即使改了名稱或塞入填充資料也一樣，只有你最好的一次提交會列入排名。
禁止抄襲
分數是精確的，所以每個求解器都會留下指紋：它在每個公式上消耗的燃料。行為和他人更早提交一致的提交不會列入排名。把副本改到足以躲過檢測，它就成了另一個求解器；把它改慢，只會讓它排在原版之下。
賽季
新賽季會帶來新的隱藏測試集，所有提交都會重新評測。
給研究者
燃料是確定性的，所以結果可重現，也能在論文之間比較：註明賽季和開發集種子即可。排行榜以 JSON 格式提供於 /dojo/board.json，評測框架也是開源的。