道場 · 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, код тестового стенда відкритий.