道場 · dojo
SAT Dojo
Siłownia dla solverów SAT. Skompiluj swój do WebAssembly, zgłoś go, a zostanie oceniony na ukrytym zbiorze świeżych formuł: łamigłówki Hashi, pułapki parzystości, losowe 3-SAT, gołębie i hetmany.
Ranking 番付 · banzuke
Średnie paliwo na formułę w miliardach, nierozwiązane formuły liczą się jako podwójny budżet. Mniej znaczy lepiej.
Ładowanie…
Jak to działa 稽古 · keiko
一Zbuduj
Nada się każdy język kompilowany do WASI preview 1: Rust, C i C++ z wasi-sdk, Zig, Go. Czytaj DIMACS ze stdin i odpowiadaj jak w 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二Trenuj
Oceń swój solver lokalnie na publicznym zbiorze deweloperskim za pomocą narzędzia dojo. Działa dokładnie jak ranking, więc znasz swój wynik, zanim go zgłosisz.
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三Zgłoś
Wgraj plik .wasm. Zostanie uruchomiony na ukrytym zbiorze bieżącego sezonu, na naszej własnej maszynie.
四Wspinaj się
Wygrywa najniższy PAR-2: średnie paliwo na formułę, przy czym nierozwiązane formuły liczą się jako podwójny budżet.
Formuły
Hashi
Łamigłówki Hashiwokakero od 10×10 do 28×28 jako CNF, bez reguły spójności. Zawsze spełnialne.
Parzystość Hashi
Łamigłówki z jedną zmienioną liczbą, tak że suma liczb jest nieparzysta. Niespełnialne, bo każdy most dodaje dwa. Łatwo to zauważyć, trudno udowodnić rezolucją.
Losowe 3-SAT
Jednostajnie losowe 3-SAT w punkcie przejścia fazowego, 4,26 klauzuli na zmienną, mniej więcej połowa spełnialna.
Zasada szufladkowa
n+1 gołębi w n przegródkach: klasyk wymagający wykładniczo długich dowodów rezolucyjnych. Do tego kilka instancji, w których wszystkie się mieszczą.
Hetmany
N hetmanów na planszach do 48×48 z kilkoma zakazanymi polami.
Wejdź do dojo 入門 · nyūmon
Ładowanie…
Uczciwa gra 礼 · rei
Paliwo, nie sekundy
Każda wykonana instrukcja WebAssembly kosztuje jedną jednostkę paliwa, masowe operacje na pamięci jedną na bajt. Zegary i liczby losowe mają stałe ziarno, więc solver dostaje ten sam wynik na każdej maszynie, za każdym razem.
Ukryte, świeże formuły
Zbiór testowy pochodzi z tajnego ziarna, które zmienia się co sezon, a każda formuła jest przemieszana: zmienne przemianowane i zanegowane, klauzule przetasowane. Wyniki są pokazywane tylko dla rodzin, nigdy dla pojedynczych formuł.
Każda odpowiedź sprawdzona
Modele są weryfikowane względem formuły. UNSAT liczy się tylko tam, gdzie mamy dowód: zasada szufladkowa i parzystość Hashi są niespełnialne z konstrukcji, a każda inna etykieta UNSAT ma dowód DRAT zweryfikowany przez nasz własny checker. Jedna błędna odpowiedź dyskwalifikuje zgłoszenie, więc zgadywanie się nie opłaca.
Szczelna piaskownica
Bez plików, bez sieci, bez zmiennych środowiskowych. Pamięć i wyjście są ograniczone, a zgłoszenia działają na osobnej maszynie, która nie przechowuje żadnych danych.
Jedno konto, najlepszy wynik
Konto musi mieć co najmniej dobę, by zgłaszać, a limit to trzy zgłoszenia dziennie na konto i na sieć. Identyczny kod jest odrzucany, nawet po zmianie nazwy lub dopełnieniu, a w rankingu liczy się tylko twoje najlepsze zgłoszenie.
Żadnych kopii
Wyniki są dokładne, więc solver zostawia odcisk palca: paliwo, które zużywa na każdej formule. Zgłoszenie, które zachowuje się jak wcześniejsze zgłoszenie innej osoby, nie trafia do rankingu. Zmiana kopii na tyle, by tego uniknąć, czyni z niej inny solver, a spowolnienie jej tylko spycha ją poniżej oryginału.
Sezony
Nowy sezon przynosi nowy ukryty zbiór, a każde zgłoszenie jest oceniane od nowa.
Dla badaczy
Paliwo jest deterministyczne, więc wyniki są powtarzalne i porównywalne między publikacjami: podaj sezon i ziarno zbioru deweloperskiego. Ranking jest dostępny jako JSON pod /dojo/board.json, a środowisko testowe jest open source.