道場 · dojo
SAT道場
SATソルバーのためのジムです。ソルバーをWebAssemblyにコンパイルして提出すると、非公開の新しい論理式で採点されます。橋をかけろのパズル、パリティの罠、ランダム3-SAT、鳩の巣、クイーン。
ランキング 番付 · banzuke
1式あたりの平均燃料（単位：10億）。解けなかった式は予算の2倍として数えます。低いほど上位です。
読み込み中…
しくみ 稽古 · 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が最も低いソルバーが勝ちます。1式あたりの平均燃料で、解けなかった式は予算の2倍として数えます。
論理式
橋をかけろ
10×10から28×28までの橋をかけろのパズルを、連結性ルールを除いてCNFにしたもの。必ず充足可能です。
橋をかけろ・パリティ
数字をひとつ変えて合計を奇数にしたパズル。橋は必ず2ずつ加えるので充足不能です。見ればすぐわかるのに、導出原理で証明するのは困難です。
ランダム3-SAT
相転移点（変数あたり4.26節）での一様ランダム3-SAT。約半分が充足可能です。
鳩の巣
n個の巣にn+1羽の鳩：指数長の導出証明が必要になる古典問題。収まる場合も少し混ぜています。
クイーン
最大48×48の盤面に、いくつかの禁止マスを加えたNクイーン問題。
いざ、道場へ 入門 · nyūmon
読み込み中…
フェアプレー 礼 · rei
秒ではなく燃料
実行されたWebAssembly命令は1つにつき燃料1単位、バルクメモリ操作は1バイトにつき1単位。時計と乱数はシード固定なので、どのマシンでも、何度実行しても同じスコアになります。
非公開の新しい論理式
テストセットはシーズンごとに変わる秘密のシードから生成され、各式はかき混ぜられます。変数の名前変更と否定、節のシャッフル。結果は系統ごとにのみ表示され、式ごとには表示されません。
すべての答えを検証
モデルは論理式と照合して検証されます。UNSATが認められるのは証明がある場合だけです。鳩の巣と橋をかけろ・パリティは構成上充足不能で、それ以外のUNSATラベルには自前のチェッカーで検証したDRAT証明が付いています。誤答が1つでもあれば失格になるので、当てずっぽうは割に合いません。
密閉されたサンドボックス
ファイルなし、ネットワークなし、環境変数なし。メモリと出力には上限があり、提出物はデータを一切持たない別のマシンで実行されます。
1アカウント、最高記録のみ
提出できるのは作成から1日経ったアカウントだけで、提出はアカウントごと・ネットワークごとに1日3回までです。同一のコードは、名前を変えても水増ししても受け付けず、ランキングに載るのは最も良い提出だけです。
コピー禁止
スコアは厳密なので、ソルバーには指紋が残ります。各式で消費する燃料です。別の人の以前の提出と同じ挙動をする提出はランキングに載りません。それを逃れるほどコピーを変えれば別のソルバーになり、遅くしてもオリジナルより下になるだけです。
シーズン
新しいシーズンには新しい非公開セットが用意され、すべての提出物が再評価されます。
研究者の方へ
燃料は決定的なので、結果は再現可能で論文間でも比較できます。シーズンと開発用シードを明記してください。ランキングは /dojo/board.json でJSONとして取得でき、評価ハーネスはオープンソースです。