道場 · dojo
SAT Dojo
Tempat latihan untuk solver SAT. Kompilasi solvermu ke WebAssembly, kirimkan, dan solver itu dinilai pada set tersembunyi berisi formula baru: teka-teki Hashi, jebakan paritas, 3-SAT acak, merpati, dan ratu.
Papan peringkat 番付 · banzuke
Rata-rata fuel per formula dalam miliar, formula yang tak terpecahkan dihitung dua kali anggaran. Makin rendah makin baik.
Memuat…
Cara kerjanya 稽古 · keiko
一Bangun
Bahasa apa pun yang bisa dikompilasi ke WASI preview 1 bisa dipakai: Rust, C dan C++ dengan wasi-sdk, Zig, Go. Baca DIMACS dari stdin dan jawab seperti di kompetisi 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二Latihan
Nilai solvermu secara lokal pada set dev publik dengan alat dojo. Alat ini berjalan persis seperti papan peringkat, jadi kamu tahu skormu sebelum mengirim.
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三Kirim
Unggah file .wasm. File itu dijalankan pada set tersembunyi musim ini, di mesin kami sendiri.
四Panjat
PAR-2 terendah menang: rata-rata fuel per formula, dengan formula yang tak terpecahkan dihitung dua kali anggaran.
Formulanya
Hashi
Teka-teki Hashiwokakero dari 10×10 sampai 28×28 sebagai CNF, tanpa aturan keterhubungan. Selalu dapat dipenuhi.
Hashi paritas
Teka-teki dengan satu angka diubah sehingga jumlah angkanya ganjil. Tidak dapat dipenuhi, karena setiap jembatan menambah dua. Mudah dilihat, sulit dibuktikan dengan resolusi.
3-SAT acak
3-SAT acak seragam di titik transisi fase, 4,26 klausa per variabel, sekitar setengahnya dapat dipenuhi.
Sarang merpati
n+1 merpati di n lubang: soal klasik yang butuh bukti resolusi yang panjangnya eksponensial. Ditambah beberapa yang memang muat.
Ratu
N ratu di papan hingga 48×48 dengan beberapa petak terlarang.
Masuki dojo 入門 · nyūmon
Memuat…
Main adil 礼 · rei
Fuel, bukan detik
Setiap instruksi WebAssembly yang dieksekusi memakan satu unit fuel, operasi memori massal satu per byte. Jam dan angka acak diberi seed tetap, jadi solver mendapat skor yang sama di setiap mesin, setiap kali.
Formula baru yang tersembunyi
Set uji berasal dari seed rahasia yang berganti setiap musim, dan setiap formula diacak: variabel diganti nama dan dinegasikan, klausa dikocok. Hasil hanya ditampilkan per keluarga, tidak pernah per formula.
Setiap jawaban diperiksa
Model diverifikasi terhadap formulanya. UNSAT hanya dihitung jika kami punya buktinya: sarang merpati dan Hashi paritas tidak dapat dipenuhi berdasarkan konstruksinya, dan setiap label UNSAT lainnya disertai bukti DRAT yang diverifikasi oleh pemeriksa buatan kami sendiri. Satu jawaban salah saja mendiskualifikasi kiriman, jadi menebak tidak pernah menguntungkan.
Sandbox tertutup
Tanpa file, tanpa jaringan, tanpa variabel lingkungan. Memori dan output dibatasi, dan kiriman dijalankan di mesin terpisah yang tidak menyimpan data apa pun.
Satu akun, entri terbaik
Akun harus berumur satu hari untuk mengirim, dan ada tiga kiriman per hari per akun dan per jaringan. Kode yang identik ditolak, meskipun diganti nama atau diberi padding, dan hanya kiriman terbaikmu yang masuk peringkat.
Tanpa salinan
Skornya pasti, jadi setiap solver meninggalkan sidik jari: fuel yang dipakainya di setiap formula. Kiriman yang berperilaku seperti kiriman orang lain yang lebih awal tidak masuk peringkat. Mengubah salinan cukup jauh untuk lolos dari itu menjadikannya solver yang berbeda, dan membuatnya lebih lambat hanya menempatkannya di bawah yang asli.
Musim
Musim baru membawa set tersembunyi baru dan semua kiriman dievaluasi ulang.
Untuk peneliti
Fuel bersifat deterministik, jadi hasilnya bisa direproduksi dan dibandingkan antarmakalah: sebutkan musim dan seed dev-nya. Papan peringkat tersedia sebagai JSON di /dojo/board.json, dan harness-nya sumber terbuka.