道場 · dojo
SAT Dojo
Una palestra per solver SAT. Compila il tuo in WebAssembly, invialo e verrà valutato su un insieme segreto di formule nuove: puzzle Hashi, trappole di parità, 3-SAT casuale, piccioni e regine.
Classifica 番付 · banzuke
Carburante medio per formula in miliardi, le formule non risolte contano il doppio del budget. Più basso è meglio.
Caricamento…
Come funziona 稽古 · keiko
一Costruisci
Va bene qualsiasi linguaggio che compili per WASI preview 1: Rust, C e C++ con wasi-sdk, Zig, Go. Leggi DIMACS da stdin e rispondi come nella 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二Allenati
Valuta il tuo solver in locale sul dev set pubblico con lo strumento dojo. Funziona esattamente come la classifica, così conosci il tuo punteggio prima di inviare.
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三Invia
Carica il file .wasm. Viene eseguito sull’insieme segreto della stagione in corso, sulla nostra macchina.
四Scala
Vince il PAR-2 più basso: il carburante medio per formula, dove le formule non risolte contano il doppio del budget.
Le formule
Hashi
Puzzle Hashiwokakero da 10×10 a 28×28 in CNF, senza la regola di connessione. Sempre soddisfacibili.
Hashi parità
Puzzle con un numero cambiato in modo che la somma sia dispari. Insoddisfacibili, perché ogni ponte aggiunge due. Facile da vedere, difficile da dimostrare per risoluzione.
3-SAT casuale
3-SAT casuale uniforme alla transizione di fase, 4,26 clausole per variabile, circa la metà soddisfacibili.
Piccionaia
n+1 piccioni in n buche: il classico che richiede dimostrazioni per risoluzione di lunghezza esponenziale. Più alcune in cui ci stanno.
Regine
N regine su scacchiere fino a 48×48 con alcune caselle vietate.
Entra nel dojo 入門 · nyūmon
Caricamento…
Fair play 礼 · rei
Carburante, non secondi
Ogni istruzione WebAssembly eseguita costa un’unità di carburante, le operazioni di memoria bulk una per byte. Orologi e numeri casuali hanno un seed fisso, quindi un solver ottiene lo stesso punteggio su ogni macchina, ogni volta.
Formule segrete e nuove
Il test set nasce da un seed segreto che cambia ogni stagione, e ogni formula viene rimescolata: variabili rinominate e negate, clausole mischiate. I risultati sono mostrati solo per famiglia, mai per singola formula.
Ogni risposta verificata
I modelli vengono verificati sulla formula. UNSAT conta solo dove abbiamo una prova: Piccionaia e Hashi parità sono insoddisfacibili per costruzione, ogni altra etichetta UNSAT è accompagnata da una prova DRAT verificata dal nostro checker. Una sola risposta sbagliata squalifica l’invio, quindi tirare a indovinare non paga mai.
Una sandbox sigillata
Niente file, niente rete, niente variabili d’ambiente. Memoria e output sono limitati, e gli invii girano su una macchina separata che non contiene dati.
Un account, il miglior invio
Per inviare, un account deve avere almeno un giorno, e ci sono tre invii al giorno per account e per rete. Il codice identico viene rifiutato, anche se rinominato o riempito con padding, e solo il tuo invio migliore entra in classifica.
Niente copie
I punteggi sono esatti, quindi un solver lascia un’impronta: il carburante che usa su ogni formula. Un invio che si comporta come uno precedente di qualcun altro non entra in classifica. Modificare una copia abbastanza da sfuggire a questo controllo la rende un solver diverso, e renderla più lenta la mette solo sotto l’originale.
Stagioni
Una nuova stagione porta un nuovo insieme segreto e ogni invio viene rivalutato.
Per i ricercatori
Il carburante è deterministico, quindi i risultati sono riproducibili e confrontabili tra articoli: indica la stagione e il seed del dev set. La classifica è disponibile in JSON su /dojo/board.json, l’harness è open source.