道場 · dojo
SAT Dojo
Uma academia para solvers SAT. Compile o seu para WebAssembly, envie, e ele é avaliado num conjunto oculto de fórmulas novas: puzzles Hashi, armadilhas de paridade, 3-SAT aleatório, pombos e rainhas.
Ranking 番付 · banzuke
Combustível médio por fórmula, em bilhões; fórmulas não resolvidas contam o dobro do orçamento. Menor é melhor.
Carregando…
Como funciona 稽古 · keiko
一Compile
Qualquer linguagem que compile para WASI preview 1 serve: Rust, C e C++ com wasi-sdk, Zig, Go. Leia DIMACS da stdin e responda como na 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二Treine
Avalie seu solver localmente no dev set público com a ferramenta dojo. Ela roda exatamente como o ranking, então você sabe sua pontuação antes de enviar.
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三Envie
Faça upload do arquivo .wasm. Ele roda no conjunto oculto da temporada atual, na nossa própria máquina.
四Suba
Vence o menor PAR-2: o combustível médio por fórmula, em que fórmulas não resolvidas contam o dobro do orçamento.
As fórmulas
Hashi
Puzzles Hashiwokakero de 10×10 a 28×28 em CNF, sem a regra de conectividade. Sempre satisfatíveis.
Paridade Hashi
Puzzles com um número alterado para que a soma dos números seja ímpar. Insatisfatíveis, pois cada ponte soma dois. Fácil de ver, difícil de provar por resolução.
3-SAT aleatório
3-SAT aleatório uniforme na transição de fase, 4,26 cláusulas por variável, cerca de metade satisfatível.
Casa dos pombos
n+1 pombos em n casas: o clássico que exige provas por resolução de tamanho exponencial. Mais algumas instâncias em que todos cabem.
Rainhas
N rainhas em tabuleiros de até 48×48 com algumas casas proibidas.
Entre no dojo 入門 · nyūmon
Carregando…
Jogo limpo 礼 · rei
Combustível, não segundos
Cada instrução WebAssembly executada custa uma unidade de combustível; operações de memória em massa, uma por byte. Relógios e números aleatórios têm semente fixa, então um solver obtém a mesma pontuação em qualquer máquina, sempre.
Fórmulas ocultas e novas
O conjunto de teste vem de uma semente secreta que muda a cada temporada, e cada fórmula é embaralhada: variáveis renomeadas e negadas, cláusulas misturadas. Os resultados aparecem só por família, nunca por fórmula.
Toda resposta verificada
Os modelos são verificados contra a fórmula. UNSAT só conta onde temos uma prova: casa dos pombos e paridade Hashi são insatisfatíveis por construção, e todo outro rótulo UNSAT vem com uma prova DRAT verificada pelo nosso próprio verificador. Uma única resposta errada desclassifica o envio, então chutar nunca compensa.
Uma sandbox selada
Sem arquivos, sem rede, sem variáveis de ambiente. Memória e saída têm limite, e os envios rodam numa máquina separada que não guarda dados.
Uma conta, o melhor envio
As contas precisam ter um dia para enviar, e são três envios por dia por conta e por rede. Código idêntico é recusado, mesmo renomeado ou com enchimento, e só o seu melhor envio entra no ranking.
Nada de cópias
As pontuações são exatas, então um solver deixa uma impressão digital: o combustível que ele gasta em cada fórmula. Um envio que se comporta como um anterior de outra pessoa não entra no ranking. Mudar uma cópia o bastante para escapar disso a torna um solver diferente, e deixá-la mais lenta só a coloca abaixo do original.
Temporadas
Uma nova temporada traz um novo conjunto oculto, e todos os envios são avaliados de novo.
Para pesquisadores
O combustível é determinístico, então os resultados são reproduzíveis e comparáveis entre artigos: informe a temporada e a semente do dev set. O ranking está disponível em JSON em /dojo/board.json, e o harness é de código aberto.