Chaque puzzle Griductive fait une promesse audacieuse : vous n'aurez jamais besoin de deviner. Chaque cellule peut etre determinee par la logique seule, et chaque puzzle a exactement une reponse correcte.
Ce n'est pas un objectif de conception — c'est une garantie mathematique, assuree par la meme classe de solveur utilisee en recherche operationnelle et en verification de circuits. Cet article explique comment.
Pourquoi l'unicite est importante
Si un puzzle a deux solutions valides, il doit y avoir au moins une cellule ou Suspect et Innocent satisfont tous les indices. A cette cellule, aucun raisonnement ne peut vous dire lequel est correct — vous seriez oblige de deviner. Deviner viole le contrat fondamental d'un puzzle de deduction.
Le generateur ne produit donc pas simplement des puzzles qui se trouvent avoir une seule solution. Il prouve qu'aucune deuxieme solution n'existe avant qu'un puzzle ne soit publie.
Le pipeline en cinq phases
Chaque puzzle Griductive est construit a travers un pipeline en cinq phases. Voici ce qui se passe a chaque etape.
Phase 1 : Generer une solution aleatoire
Le generateur commence par creer une grille de solution valide — une attribution aleatoire de Suspect et Innocent a chaque cellule. C'est la verite de reference que le joueur devra finalement deduire.
A ce stade, aucun indice n'existe encore. La grille n'est qu'une configuration aleatoire qui satisfait les contraintes structurelles de base (dimensions de la grille, nombre de suspects dans les intervalles valides).
Phase 2 : Construire le pool d'indices
Ensuite, le generateur enumere exhaustivement chaque indice possible qui est vrai sur la grille de solution.
Griductive dispose de plus de 26 types d'indices distincts — comptage, comparaison, spatiaux, existentiels, unicite, connectivite, et plus encore. Pour chaque type, le generateur teste chaque parametrage valide par rapport a la grille. Une grille 4x4 peut produire des milliers d'indices candidats. Seuls les indices qui s'evaluent a vrai sur la solution sont conserves.
C'est la matiere premiere avec laquelle le generateur travaille : un vaste pool d'enonces vrais, dont la plupart sont redondants.
Phase 3 : Selectionner un ensemble minimal d'indices (la partie difficile)
C'est ici que le vrai travail commence. Le generateur doit choisir un petit sous-ensemble d'indices du pool tel que :
- Les indices sont suffisants — ensemble, ils contraignent l'espace des solutions a exactement une grille valide.
- Aucun indice n'est redondant — retirer un seul indice permettrait plusieurs solutions.
Le generateur utilise une approche de satisfaction de contraintes gloutonne :
- Commencer sans aucun indice selectionne. L'espace des solutions est grand ouvert — de nombreuses grilles pourraient etre valides.
- Evaluer chaque indice candidat selon sa capacite a reduire l'espace des solutions. Un indice qui elimine 80 % des possibilites restantes obtient un score plus eleve qu'un indice qui en elimine 10 %.
- Selectionner l'indice le mieux note et l'ajouter a l'ensemble.
- Re-resoudre le modele de contraintes avec l'ensemble d'indices mis a jour.
- Repeter jusqu'a ce que le solveur confirme qu'il ne reste qu'une seule solution.
- Elagage : parcourir l'ensemble final et retirer tout indice qui n'est pas necessaire pour l'unicite. Cela garde le puzzle propre et evite de donner au joueur des informations gratuites.
Le resultat est un ensemble d'indices serre et equitable — suffisant pour resoudre completement le puzzle, sans indices inutiles.
Phase 4 : Evaluer la difficulte
Avec l'ensemble d'indices verrouille, le generateur evalue la difficulte du puzzle sur une echelle de 0 a 100. Quatre facteurs contribuent :
- Ratio d'indices simples (35 %) — Combien d'indices sont des enonces directs de comptage ou d'identite. Plus il y a d'indices simples, plus le puzzle est facile.
- Ratio d'indices complexes (30 %) — Combien d'indices necessitent un raisonnement en plusieurs etapes ou spatial. Ceux-ci exigent des chaines de deduction plus profondes.
- Rarete de l'information (20 %) — Combien peu d'indices sont donnes par rapport a la taille de la grille. Moins d'indices signifie moins de materiel avec lequel travailler.
- Echelle de la grille (15 %) — Les grilles plus grandes sont inherement plus difficiles a suivre. Un puzzle 5x5 a presque trois fois plus de cellules qu'un 3x3.
Chaque type d'indice a egalement une note de complexite intrinseque basee sur le raisonnement qu'il exige. Un indice comme « Julia est une suspecte » est a peu pres aussi simple que possible. Un indice comme « Julia est la seule personne de la rangee 3 avec exactement 1 voisin suspect » necessite de croiser plusieurs cellules et obtient un score beaucoup plus eleve.
Phase 5 : Generer les indices d'aide et formater la sortie
Enfin, le generateur construit la sequence d'indices d'aide — un ordre de resolution recommande qui guide les joueurs bloques a travers le puzzle, une etape logique a la fois. Les indices d'aide sont ordonnes par profondeur de dependance : les cellules qui peuvent etre deduites immediatement arrivent en premier, et les cellules qui necessitent de longues chaines de deductions prealables arrivent en dernier.
Le puzzle final est emballe avec toutes les donnees dont le jeu a besoin : metadonnees, ensemble d'indices, sequence d'aide et score de difficulte.
Le solveur : comment l'unicite est prouvee
Au coeur du pipeline se trouve Google OR-Tools CP-SAT — un solveur de programmation par contraintes qui combine propagation de contraintes, programmation en nombres entiers et resolution SAT.
Comment un puzzle devient un probleme mathematique
Chaque cellule de la grille est modelisee comme une variable booleenne : Suspect (1) ou Innocent (0). Chaque indice devient une ou plusieurs contraintes mathematiques sur ces variables.
Par exemple :
- « Il y a exactement 2 suspects dans la rangee 3 » devient :
cell[3,0] + cell[3,1] + cell[3,2] + cell[3,3] = 2 - « Tous les suspects de la colonne A sont connectes » devient : une contrainte de connectivite assurant que les cellules suspectes de la colonne A forment une chaine contigue sans interruption.
- « La rangee 1 a plus de suspects que la colonne B » devient :
sum(row_1) > sum(col_B)
Comment l'unicite est verifiee
Apres avoir assemble l'ensemble d'indices, le generateur pose a CP-SAT une question precise : « Etant donne ces contraintes, existe-t-il plus d'une affectation valide ? »
CP-SAT ne trouve pas seulement une solution — il peut enumerer toutes les solutions. Si le solveur en trouve exactement une, le puzzle est valide. S'il en trouve deux ou plus, le generateur retourne a la Phase 3 et ajoute un autre indice.
C'est une preuve formelle, pas une heuristique. CP-SAT explore exhaustivement l'ensemble de l'espace des solutions. S'il dit qu'il y a une solution, il y en a exactement une — point final.
Pourquoi ne pas simplement utiliser la force brute ?
Une grille 5x5 a 25 cellules, chacune avec 2 valeurs possibles. Cela fait 2^25 = 33 millions de grilles possibles. Les tester toutes par force brute est lent et ne passe pas a l'echelle.
CP-SAT est considerablement plus rapide grace a la propagation de contraintes : quand un indice dit « la rangee 3 a exactement 2 suspects », le solveur reduit immediatement l'espace de recherche pour chaque cellule de la rangee 3 sans verifier chaque combinaison individuellement. Les indices complexes composent cet effet. En pratique, CP-SAT prouve l'unicite d'un puzzle 5x5 en quelques millisecondes.
Ce qui pourrait mal tourner (et comment nous le prevenons)
« Et si un indice etait ambigu ? »
Chaque type d'indice a une definition mathematique formelle. « Voisins » signifie toujours les cellules environnantes (jusqu'a 8), diagonales incluses. « Connecte » signifie toujours une chaine contigue de cellules adjacentes. « Entre » signifie toujours des cellules dans la meme rangee ou colonne, en excluant les extremites.
Ces definitions sont integrees directement dans le modele de contraintes — il n'y a pas d'etape d'interpretation en langage naturel ou l'ambiguite pourrait s'infiltrer. La reference Details clarificatifs dans le jeu montre aux joueurs exactement ce que signifie chaque mot-cle spatial.
« Et si le solveur avait un bug ? »
Le solveur CP-SAT est un outil bien teste, largement utilise, maintenu par l'equipe d'optimisation de Google. Mais nous ne nous fions pas uniquement a la confiance. Chaque puzzle genere est verifie independamment :
- Un solveur automatise tente de resoudre chaque puzzle etape par etape, en simulant un joueur humain. S'il ne peut pas atteindre une solution complete par deduction logique seule, le puzzle est rejete.
- Des verifications de coherence des indices d'aide verifient que chaque indice d'aide dans la sequence est logiquement valide — que la cellule indiquee est reellement deductible a partir des indices et des cellules precedemment revelees, et non a partir d'informations cachees.
« Et si la generation d'indices manquait des cas limites ? »
Chaque type d'indice possede une fonction d'evaluation formelle qui est testee par rapport a des configurations de puzzles connues. La phase de generation du pool d'indices n'inclut que les indices qui s'evaluent a vrai sur la solution reelle — un indice faux sur la solution ne peut jamais apparaitre dans le puzzle.
Le resultat
Quand vous ouvrez un puzzle Griductive, voici ce qui s'est deja passe :
- Une solution aleatoire a ete generee.
- Des milliers d'indices candidats ont ete evalues par rapport a celle-ci.
- Un sous-ensemble minimal et non redondant a ete selectionne.
- Un solveur formel a prouve qu'exactement une solution satisfait ces indices.
- Un solveur automatise a independamment verifie que le puzzle est resolvable par pure deduction.
- Un score de difficulte a ete calcule et une sequence d'aide a ete generee.
Chaque puzzle, chaque jour, dans les quatre tailles de grille. Sans exception.
La promesse tient : si vous etes bloque, il y a un indice que vous n'avez pas encore pleinement exploite. Si vous pensez que deux reponses sont possibles, relisez les indices — la logique les resoudra. Et si vous voulez une preuve, le Graphe logique vous montrera la chaine de deduction exacte des indices a la solution.
La suite : des indices qui racontent une histoire
Pour le moment, les indices de Griductive se lisent comme des enonces logiques precis — clairs et sans ambiguite, mais un peu cliniques, il faut l'admettre. « Il y a exactement 2 suspects dans la rangee 3 » remplit sa fonction, mais cela ne vous donne pas vraiment l'impression d'etre un detective sur une affaire.
Nous travaillons activement a changer cela. L'objectif est de diversifier la facon dont les indices sont exprimes — en y integrant une touche thematique tout en preservant la meme precision logique sous-jacente. Imaginez des indices lies a des evenements saisonniers, ou formules comme des temoignages d'une scene de crime specifique. Au lieu d'une formule sterile, vous liriez quelque chose qui ressemble a une veritable piece a conviction d'une enquete.
La contrainte cle n'a pas change : chaque indice doit rester coherent, sans ambiguite et formellement verifiable. Le solveur se moque de savoir si un indice ressemble a un manuel de mathematiques ou a un roman policier — il ne s'interesse qu'au contenu logique. Cette separation est ce qui rend une expression plus riche possible sans compromettre l'exactitude.
Memes garanties. Meme rigueur. Mais des puzzles qui ressemblent moins a des equations et plus a des affaires qui meritent d'etre resolues.
Pas de devinette. Pas de chance. Mathematiquement garanti.