道場 · 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，评测框架开源。