道場 · dojo
SAT-додзё
Спортзал для SAT-решателей. Скомпилируй свой в WebAssembly, отправь, и он будет оценён на скрытом наборе свежих формул: головоломки Hashi, ловушки чётности, случайный 3-SAT, голуби и ферзи.
Рейтинг 番付 · banzuke
Среднее топливо на формулу в миллиардах; нерешённые формулы считаются как двойной бюджет. Чем меньше, тем лучше.
Загрузка…
Как это работает 稽古 · keiko
一Собери
Подойдёт любой язык, который компилируется в WASI preview 1: Rust, C и C++ с wasi-sdk, Zig, Go. Читай DIMACS из stdin и отвечай как на 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二Тренируйся
Оцени свой решатель локально на открытом наборе для разработки с помощью утилиты 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: среднее топливо на формулу, где нерешённые формулы считаются как двойной бюджет.
Формулы
Hashi
Головоломки Hashiwokakero от 10×10 до 28×28 в виде CNF, без правила связности. Всегда выполнимы.
Чётность Hashi
Головоломки с одним изменённым числом, так что сумма чисел нечётна. Невыполнимы, ведь каждый мост добавляет двойку. Легко увидеть, трудно доказать резолюцией.
Случайный 3-SAT
Равномерный случайный 3-SAT в точке фазового перехода, 4,26 дизъюнкта на переменную, примерно половина выполнима.
Принцип Дирихле
n+1 голубей в n клетках: классика, требующая экспоненциально длинных резолютивных доказательств. Плюс несколько вариантов, где все помещаются.
Ферзи
N ферзей на досках до 48×48 с несколькими запрещёнными клетками.
Войди в додзё 入門 · nyūmon
Загрузка…
Честная игра 礼 · rei
Топливо, а не секунды
Каждая выполненная инструкция WebAssembly стоит одну единицу топлива, массовые операции с памятью — одну на байт. Часы и случайные числа работают от фиксированного зерна, так что решатель получает одинаковый результат на любой машине, каждый раз.
Скрытые свежие формулы
Тестовый набор строится из секретного зерна, которое меняется каждый сезон, и каждая формула перемешана: переменные переименованы и инвертированы, дизъюнкты перетасованы. Результаты показываются только по семействам, никогда по отдельным формулам.
Каждый ответ проверяется
Модели проверяются на формуле. UNSAT засчитывается только там, где у нас есть доказательство: принцип Дирихле и чётность Hashi невыполнимы по построению, а каждая другая метка UNSAT сопровождается доказательством DRAT, проверенным нашим собственным чекером. Один неверный ответ дисквалифицирует посылку, так что угадывать бесполезно.
Герметичная песочница
Никаких файлов, сети и переменных окружения. Память и вывод ограничены, а посылки выполняются на отдельной машине, где нет никаких данных.
Один аккаунт — лучшая посылка
Отправлять можно с аккаунта не младше суток, и лимит — три посылки в день на аккаунт и на сеть. Одинаковый код отклоняется, даже переименованный или раздутый, и в рейтинге учитывается только твоя лучшая посылка.
Никаких копий
Результаты точные, поэтому решатель оставляет отпечаток: топливо, которое он тратит на каждую формулу. Посылка, которая ведёт себя как более ранняя посылка другого автора, не попадает в рейтинг. Если изменить копию настолько, чтобы обойти это, получится уже другой решатель, а если её замедлить, она просто окажется ниже оригинала.
Сезоны
Новый сезон приносит новый скрытый набор, и все посылки оцениваются заново.
Для исследователей
Топливо детерминировано, поэтому результаты воспроизводимы и сравнимы между статьями: укажи сезон и зерно набора для разработки. Рейтинг доступен в JSON по адресу /dojo/board.json, код тестового стенда открыт.