道場 · dojo
SAT Dojo
Un gimnasio para solvers SAT. Compila el tuyo a WebAssembly, envíalo y se evaluará con un conjunto secreto de fórmulas nuevas: puzles Hashi, trampas de paridad, 3-SAT aleatorio, palomas y reinas.
Clasificación 番付 · banzuke
Combustible medio por fórmula en miles de millones; las fórmulas sin resolver cuentan el doble del presupuesto. Cuanto menos, mejor.
Cargando…
Cómo funciona 稽古 · keiko
一Construye
Sirve cualquier lenguaje que compile a WASI preview 1: Rust, C y C++ con wasi-sdk, Zig, Go. Lee DIMACS por stdin y responde como en la 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二Entrena
Evalúa tu solver en local con el conjunto de desarrollo público y la herramienta dojo. Funciona exactamente igual que la clasificación, así que sabrás tu puntuación antes de enviarlo.
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三Envía
Sube el archivo .wasm. Se ejecuta con el conjunto secreto de la temporada actual, en nuestra propia máquina.
四Escala
Gana el PAR-2 más bajo: el combustible medio por fórmula, donde las fórmulas sin resolver cuentan el doble del presupuesto.
Las fórmulas
Hashi
Puzles Hashiwokakero de 10×10 a 28×28 en CNF, sin la regla de conectividad. Siempre satisfacibles.
Hashi paridad
Puzles con un número cambiado para que la suma sea impar. Insatisfacibles, porque cada puente suma dos. Fácil de ver, difícil de demostrar por resolución.
3-SAT aleatorio
3-SAT aleatorio uniforme en la transición de fase, 4,26 cláusulas por variable, cerca de la mitad satisfacibles.
Palomar
n+1 palomas en n agujeros: el clásico que exige demostraciones por resolución de longitud exponencial. Y algunas en las que sí caben.
Reinas
N reinas en tableros de hasta 48×48 con algunas casillas prohibidas.
Entra en el dojo 入門 · nyūmon
Cargando…
Juego limpio 礼 · rei
Combustible, no segundos
Cada instrucción WebAssembly ejecutada cuesta una unidad de combustible; las operaciones de memoria en bloque, una por byte. Los relojes y los números aleatorios tienen semilla fija, así que un solver obtiene la misma puntuación en cualquier máquina, siempre.
Fórmulas secretas y nuevas
El conjunto de prueba sale de una semilla secreta que cambia cada temporada, y cada fórmula se desordena: variables renombradas y negadas, cláusulas barajadas. Los resultados se muestran solo por familia, nunca por fórmula.
Cada respuesta, verificada
Los modelos se verifican contra la fórmula. UNSAT solo cuenta donde tenemos una prueba: Palomar y Hashi paridad son insatisfacibles por construcción, y cualquier otra etiqueta UNSAT viene con una prueba DRAT verificada por nuestro propio comprobador. Una sola respuesta incorrecta descalifica el envío, así que adivinar nunca compensa.
Un sandbox sellado
Sin archivos, sin red, sin variables de entorno. La memoria y la salida están limitadas, y los envíos se ejecutan en una máquina aparte que no guarda datos.
Una cuenta, la mejor entrada
Las cuentas necesitan un día de antigüedad para enviar, y hay tres envíos al día por cuenta y por red. El código idéntico se rechaza, aunque se renombre o se rellene, y solo tu mejor envío entra en la clasificación.
Nada de copias
Las puntuaciones son exactas, así que un solver deja una huella: el combustible que gasta en cada fórmula. Un envío que se comporta como uno anterior de otra persona no entra en la clasificación. Cambiar una copia lo suficiente para evitarlo la convierte en otro solver, y hacerla más lenta solo la deja por debajo del original.
Temporadas
Una nueva temporada trae un nuevo conjunto secreto y todos los envíos se vuelven a evaluar.
Para investigadores
El combustible es determinista, así que los resultados son reproducibles y comparables entre artículos: indica la temporada y la semilla de desarrollo. La clasificación está disponible en JSON en /dojo/board.json, y el arnés de evaluación es de código abierto.