道場 · dojo
SAT Dojo
Une salle de sport pour solveurs SAT. Compile le tien en WebAssembly, soumets-le, et il est évalué sur un ensemble secret de formules inédites : grilles de Hashi, pièges de parité, 3-SAT aléatoire, pigeons et dames.
Classement 番付 · banzuke
Carburant moyen par formule en milliards, une formule non résolue compte pour deux fois le budget. Plus c’est bas, mieux c’est.
Chargement…
Comment ça marche 稽古 · keiko
一Construire
Tout langage qui compile vers WASI preview 1 convient : Rust, C et C++ avec wasi-sdk, Zig, Go. Lis du DIMACS sur stdin et réponds comme à 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二S’entraîner
Évalue ton solveur en local sur le jeu de dév public avec l’outil dojo. Il fonctionne exactement comme le classement, tu connais donc ton score avant de soumettre.
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三Soumettre
Envoie le fichier .wasm. Il est exécuté sur l’ensemble secret de la saison en cours, sur notre propre machine.
四Grimper
Le PAR-2 le plus bas gagne : le carburant moyen par formule, où chaque formule non résolue compte pour deux fois le budget.
Les formules
Hashi
Des grilles de Hashiwokakero de 10×10 à 28×28 en CNF, sans la règle de connexité. Toujours satisfiables.
Hashi parité
Des grilles dont un chiffre a été modifié pour que la somme soit impaire. Insatisfiables, puisque chaque pont ajoute deux. Facile à voir, difficile à prouver par résolution.
3-SAT aléatoire
3-SAT aléatoire uniforme à la transition de phase, 4,26 clauses par variable, environ la moitié satisfiables.
Tiroirs
n+1 pigeons dans n trous : le classique qui exige des preuves par résolution de longueur exponentielle. Plus quelques-unes où ça rentre.
Dames
N dames sur des échiquiers jusqu’à 48×48, avec quelques cases interdites.
Entre dans le dojo 入門 · nyūmon
Chargement…
Fair-play 礼 · rei
Du carburant, pas des secondes
Chaque instruction WebAssembly exécutée coûte une unité de carburant, les opérations mémoire en bloc une par octet. Horloges et nombres aléatoires ont une graine fixe : un solveur obtient le même score sur chaque machine, à chaque fois.
Formules secrètes et inédites
Le jeu de test provient d’une graine secrète qui change à chaque saison, et chaque formule est brouillée : variables renommées et niées, clauses mélangées. Les résultats ne sont affichés que par famille, jamais par formule.
Chaque réponse vérifiée
Les modèles sont vérifiés par rapport à la formule. UNSAT ne compte que là où nous avons une preuve : les tiroirs et Hashi parité sont insatisfiables par construction, et toute autre étiquette UNSAT s’accompagne d’une preuve DRAT vérifiée par notre propre vérificateur. Une seule mauvaise réponse disqualifie la soumission : deviner ne paie jamais.
Un bac à sable scellé
Pas de fichiers, pas de réseau, pas de variables d’environnement. Mémoire et sortie sont plafonnées, et les soumissions tournent sur une machine séparée qui ne contient aucune donnée.
Un compte, une meilleure entrée
Un compte doit avoir un jour pour soumettre, et chaque compte comme chaque réseau a droit à trois soumissions par jour. Un code identique est refusé, même renommé ou gonflé artificiellement, et seule ta meilleure soumission est classée.
Pas de copies
Les scores sont exacts, donc un solveur laisse une empreinte : le carburant qu’il consomme sur chaque formule. Une soumission qui se comporte comme une soumission antérieure de quelqu’un d’autre n’est pas classée. Modifier une copie assez pour y échapper en fait un autre solveur, et la ralentir ne fait que la placer sous l’original.
Saisons
Une nouvelle saison apporte un nouvel ensemble secret, et chaque soumission est réévaluée.
Pour les chercheurs
Le carburant est déterministe : les résultats sont reproductibles et comparables d’un article à l’autre, il suffit d’indiquer la saison et la graine du jeu de dév. Le classement est disponible en JSON sur /dojo/board.json, le banc d’évaluation est open source.