zebra
1.0.0
Aujourd’hui, en 2024, le projet n’est en grande partie pas maintenu. Je l'utilise comme terrain de jeu pour certaines choses que je veux essayer, mais je ne recommande à personne de s'appuyer sur cela.
Vous vous souvenez des énigmes logiques qui ressemblaient à ceci ? Ils avaient des indices comme :
Il y a une maison entre Tushar et Maui.
Le jeu vidéo préféré de Ruby est Pokémon.
Le buveur de chai n’aime pas la couleur bleue.
J'ai adoré ces problèmes quand j'étais enfant, et regarder la conférence PyCon 2019 de Raymond Hettinger m'a inspiré à revisiter ces problèmes. Il nous a montré comment les résoudre ; Je voulais apprendre à les générer.
En utilisant Python moderne et des solveurs de satisfaction de contraintes (SAT), ce projet peut être utilisé pour créer des puzzles zébrés aléatoires.
Ce projet utilise Python 3.12 et Poetry.
Le point d'entrée de ce projet est src/main.py ; par conséquent, exécutez-le avec [poetry run] python -m src.main . Nous utilisons un questionnaire pour créer une CLI avec une interactivité simple.
Les autres fichiers importants sont :
puzzle.py contient la classe principale Puzzle, qui consiste principalement à coller des indices et des éléments de puzzle
clues.py définit un indice (une instruction de niveau supérieur que nous pouvons convertir en CNF) et plusieurs usines, comme found_at ou same_house ; generate.py a des utilitaires pour créer des indices
elements.py et traptor_elements.py ont divers éléments de puzzle
Enfin, sat_utils.py contient les utilitaires de base pour interagir avec le solveur SAT pycosat. Ce code a été presque entièrement écrit par Raymond Hettinger pour sa conférence de 2019 (merci !).
❯ poésie run python -m src.main ? Quelle est la taille du puzzle ? (Utilisez les touches fléchées)
» 5
4
3 ? Choisissez un type de Traptor (utilisez les touches fléchées)
? Tropical
» ? Mythique? ? Le puzzle devrait-il inclure des smoothies ? (Utilisez les touches fléchées)
" Oui
Non? ? Le puzzle doit-il inclure des capsules de bouteilles ? (Utilisez les touches fléchées)
" Oui
Non
Indices
-----# ... Certains textes d'ambiance sont omis ...1. Le Lesser Traptor et le Swamp Traptor sont dans la même maison.
2. L'Ancien Traptor est directement à gauche du smoothie au chocolat.
3. L'Ancien Traptor et le smoothie Citron sont dans la même maison.
4. Le Volcano Traptor est directement à gauche du Restless Traptor.
5. Les capsules Cave Traptor et Green sont dans la même maison.
6. Il y a deux maisons entre le Lake Traptor et le Snapper Traptor.
7. Les capsules vertes et le Fierce Traptor sont dans la même maison.
8. Il y a une maison entre les capsules noires et le smoothie à la noix de coco.
9. Il y a une maison entre le Lesser Traptor et le smoothie Kiwi.
10. Le Dweller Traptor et le smoothie au chocolat sont dans la même maison.
11. Les capsules rouges et le Dweller Traptor sont dans la même maison.
12. Les capsules rouges sont directement à gauche du Hoarder Traptor.
13. Il y a deux maisons entre le smoothie Starfruit et les capsules jaunes.
14. Les capsules Lake Traptor et Black sont dans la même maison.
15. Le Stalker Traptor et le Fierce Traptor sont dans la même maison.
Solution
┏━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━ ┳━━━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━ ━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━ ━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━━━━┓
┃ Nest ┃ MythicalTraptorPrimary ┃ MythicalTraptorSecondary ┃ MythicalTraptorTertiaire ┃ Smoothie ┃ Capsule de bouteille ┃
┡━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━ ╇━━━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━ ━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━ ━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━━━━┩
│ 1 │ le Fierce Traptor │ le Cave Traptor │ le Stalker Traptor │ le smoothie Starfruit │ Capsules vertes │
│ 2 │ l'Ancien Traptor │ le Lake Traptor │ le Crawler Traptor │ le smoothie au Citron │ Capsules noires │
│ 3 │ le Petit Traptor │ le Swamp Traptor │ le Dweller Traptor │ le Smoothie au chocolat │ Capsules rouges │
│ 4 │ le Greater Traptor │ le Volcano Traptor │ le Hoarder Traptor │ le smoothie à la noix de coco │ Capsules jaunes │
│ 5 │ le Restless Traptor │ le Mountain Traptor │ le Snapper Traptor │ le smoothie Kiwi │ Capsules bleues │
└──────┴──────────────────────── ┴──────────────────────────┴───── ────────────────────┴──────────── ────────────┴───────────────────┘En février 2024, de quoi ai-je besoin pour considérer que cela est « terminé » ?
Ajoutez des modèles HTML, car le site pour lequel je les crée nécessite que j'inclue des éléments tels que des balises BR.
Améliorez les détails de grammaire dans le résultat, comme la majuscule dans le texte d'ambiance.
Ajoutez les ressources d'en-tête/pied de page que je copie/colle dans la soumission.
Peut-être qu'un jour, j'envisagerai une interface Web. Puis-je lancer le projet en utilisant pyodide, ou le pycosat basé sur C causerait-il des problèmes ? Qu'en est-il d'une autre interface de programmation logique, comme PySAT, la programmation d'ensembles de réponses ou d'autres de ce fil HN ?
Cela peut arriver. Mais le projet est enfin arrivé à un stade qui me satisfait, et je suis donc ravi de le partager et d'écrire à ce sujet.
2/18 : rendre les sorties plus simples, moins verbeuses, plus jolies. Mettez à jour ce README avec le nouveau formatage et les modifications. Utilisez le générateur de puzzles pour créer enfin un nouveau puzzle !
17/02 : mise à jour de la signature du puzzle pour accepter uniquement la solution, en déduisant les éléments et les classes d'éléments. Ajoutez un affichage plus agréable pour la solution.
26/11 : Nettoyer la logique de génération de puzzles/solutions. Laissez l'utilisateur choisir la taille du puzzle.
25/11 : Nommez certains types courants comme alias de type (merci, Python 3.12). Utilisez la journalisation au lieu des impressions.
Ajoutez des tests pour les types d'indices dans generate.py .
Correction d'un bug que j'ai introduit dans clues.py . Ce fichier est très difficile à comprendre, mais il est également difficile d'écrire des tests unitaires ; convertir manuellement des expressions booléennes en CNF n’est pas amusant.
Ajustez le poids des indices dans la solution. Préparez-vous à intégrer les cours de puzzle et de solution.
Supprimez la sélection Smoothie en forme de case à cocher, car elle ne fait que gêner lorsque vous essayez de créer rapidement des puzzles.
Continuez à ajouter des tests. Terminez les tests unitaires pour sat_utils.py et démarrez-en quelques-uns pour clues.py , bien que ce fichier soit très difficile à tester en raison de la difficulté de calculer manuellement les conversions DNF en CNF.
Les prochaines étapes consistent à unifier le puzzle et la solution, à créer un meilleur __repr__ et à simplifier la façon dont nous représentons la taille du puzzle (attribut sur Puzzle , tuple d'entiers 1 à N, juste le nombre n_houses , etc.).
Supprimez le noir et utilisez la collerette pour le formatage. Mettre à jour les dépendances. Ajoutez une nouvelle CLI avec une utilisation plus simple et plus claire ; python -m src.main .
Renommer SATLiteral -> PuzzleElement (smoothie, chat, etc.) ; cela précise qu'il ne s'agit pas d'un littéral au sens booléen mais plutôt d'un nom pour, par exemple, des personnages dans un puzzle.
Créez un nouveau type SATLiteral (qui est une str dans un trench-coat) ; cela représente le littéral dans le sens de variable booléenne, comme "La valeur el est à la maison loc " ou "La valeur el n'est pas à la maison loc ." En interne, ceux-ci sont représentés par un entier i et son homologue négatif -i .
Utilisez (le nouveau) SATLiteral comme type de retour de comb(el: str, loc: int) -> SATLiteral , mappant les éléments du puzzle aux littéraux, et neg(el: SATLiteral) -> SATLiteral pour annuler un littéral.
Ajouter Clause: tuple[SATLiteral, ...] représentant un "∨" (OU booléen ; disjonction) de littéraux ; par exemple, (1, -5, 6) est une disjonction indiquant que x_1 est vrai, x_5 n'est pas vrai ou x_6 est vrai.
Ajoutez ClueCNF: list[Clause] , représentant un "∧" (booléen AND; conjonction) de Clause s. Un puzzle en CNF est un « ET de OU » (« ∧ de ∨s » ou « ∧ de Clauses »).
Imprimez le puzzle plus clairement. Réduisez la verbosité de la réduction des indices.
Générez aléatoirement le puzzle (avec une graine) à chaque exécution.
Déplacez les exemples dans leurs propres fichiers. Mise à jour vers Python 3.12 (bêta). Ajoutez plus de règles de charpie. Nettoyer les importations.
Ajouter des outils de développement (black, ruff, pyright) ; exécutez black & ruff en pré-commit. Mettez à jour certains types.
"∧" est le booléen ET
"∨" est le booléen OU
une clause est un "∨ de littéraux"
un CNF est un "∧ de clauses", ou de manière équivalente un "∧ de ∨s" ("ET de OU")
Un DNF, en revanche, est un « ∨ de ∧s ». Le DNF est la réponse à un problème SAT ; un DNF de « A ou B ou C » indique que A, B et C sont toutes des affectations valides (satisfaisantes). La conversion d'un CNF en DNF est donc NP-difficile, car à partir du DNF, vous pouvez lire des solutions vers le CNF.
CNF est un ∧ de ∨s, où ∨ est sur les variables ou leurs négations (littéraux) ; un ∨ de littéraux est aussi appelé clause. DNF est un ∨ de ∧s ; un ∧ de littéraux est appelé un terme.
Le cœur de ce projet consiste à exprimer le puzzle zébré sous la forme d'un problème de satisfiabilité booléenne (SAT) (Wikipedia.
Le problème 3-SAT est connu pour être NP-complet . Autrement dit, il n’existe probablement pas d’algorithme en temps polynomial pour le résoudre. Cependant, cela ne décrit que le cas général.
Notre problème est petit et bien spécifié (après tout, nous les créons spécifiquement pour les humains !). Cela en fait un excellent choix pour les solveurs SAT modernes, et le discours (et les notes) de Hettinger le démontre magnifiquement.
