Heute, im Jahr 2024, wird das Projekt weitgehend nicht mehr gepflegt. Ich nutze es als Spielplatz für einige Dinge, die ich ausprobieren möchte, aber ich empfehle niemandem, darauf aufzubauen.
Erinnern Sie sich an Logikrätsel, die so aussahen? Sie hatten Hinweise wie:
Zwischen Tushar und Maui gibt es ein Haus.
Rubys Lieblingsvideospiel ist Pokemon.
Der Chai-Trinker mag die Farbe Blau nicht.
Als Kind liebte ich diese, und der Vortrag von Raymond Hettinger auf der PyCon 2019 inspirierte mich dazu, mich noch einmal mit diesen Problemen auseinanderzusetzen. Er zeigte uns, wie wir sie lösen können; Ich wollte lernen, wie man sie generiert.
Mithilfe moderner Python- und Constraint Satisfaction (SAT)-Löser kann dieses Projekt zur Erstellung zufälliger Zebra-Rätsel verwendet werden.
Dieses Projekt verwendet Python 3.12 und Poetry.
Der Einstiegspunkt zu diesem Projekt ist src/main.py
; Führen Sie es dementsprechend mit [poetry run] python -m src.main
aus. Wir verwenden Fragebogen, um eine CLI mit einfacher Interaktivität zu erstellen.
Weitere wichtige Dateien sind:
puzzle.py
enthält die Hauptklasse Puzzle, die hauptsächlich aus Hinweisen und Puzzleelementen besteht
clues.py
definiert einen Hinweis (eine Aussage auf höherer Ebene, die wir in ein CNF umwandeln können) und mehrere Fabriken, wie found_at
oder same_house
; generate.py
verfügt über Dienstprogramme zum Erstellen von Hinweisen
elements.py
und traptor_elements.py
enthalten verschiedene Puzzle-Elemente
Schließlich enthält sat_utils.py
die grundlegenden Dienstprogramme für die Interaktion mit dem SAT-Löser Pycosat. Dieser Code wurde fast vollständig von Raymond Hettinger für seinen Vortrag im Jahr 2019 geschrieben (danke!).
❯ Poesie run python -m src.main? Wie groß ist das Puzzle? (Pfeiltasten verwenden) » 5 4 3? Wählen Sie einen Traptortyp (verwenden Sie die Pfeiltasten). ? Tropisch » ? Mythisch? ? Sollte das Puzzle Smoothies enthalten? (Pfeiltasten verwenden) " Ja NEIN? ? Sollte das Puzzle Flaschenverschlüsse enthalten? (Pfeiltasten verwenden) " Ja NEIN Hinweise -----# ... Einige Flavor-Texte weggelassen ...1. Der Kleine Fallensteller und der Sumpffallenden befinden sich im selben Haus. 2. Der Ancient Traptor befindet sich direkt links vom Schokoladen-Smoothie. 3. Der Ancient Traptor und der Zitronen-Smoothie befinden sich im selben Haus. 4. Der Volcano Traptor befindet sich direkt links vom Restless Traptor. 5. Der Cave Traptor und die Green Bottlecaps befinden sich im selben Haus. 6. Zwischen dem Lake Traptor und dem Snapper Traptor befinden sich zwei Häuser. 7. Grüne Flaschenverschlüsse und der Fierce Traptor befinden sich im selben Haus. 8. Es gibt ein Haus zwischen schwarzen Kronkorken und dem Kokosnuss-Smoothie. 9. Es gibt ein Haus zwischen dem Kleinen Traptor und dem Kiwi-Smoothie. 10. Der Dweller Traptor und der Schokoladen-Smoothie befinden sich im selben Haus. 11. Red Bottlecaps und der Dweller Traptor befinden sich im selben Haus. 12. Rote Flaschenverschlüsse befinden sich direkt links vom Hoarder Traptor. 13. Zwischen dem Starfruit-Smoothie und den Yellow-Flaschenverschlüssen liegen zwei Häuser. 14. Die Flaschenverschlüsse von Lake Traptor und Black befinden sich im selben Haus. 15. Der Stalker Traptor und der Fierce Traptor befinden sich im selben Haus. Lösung ┏━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━ ┳━━━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━ ━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━ ━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━━━━┓ ┃ Nest ┃ MythicalTraptorPrimary ┃ MythicalTraptorSecondary ┃ MythicalTraptorTertiary ┃ Smoothie ┃ Bottlecap ┃ ┡━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━ ╇━━━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━ ━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━ ━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━━━━┩ │ 1 │ der Fierce Traptor │ der Cave Traptor │ der Stalker Traptor │ der Starfruit-Smoothie │ Grüne Flaschenverschlüsse │ │ 2 │ der Ancient Traptor │ der Lake Traptor │ der Crawler Traptor │ der Zitronen-Smoothie │ Schwarze Flaschenverschlüsse │ │ 3 │ der Kleine Fallensteller │ der Sumpf-Falle │ der Bewohner-Falle │ der Schokoladen-Smoothie │ Rote Flaschenverschlüsse │ │ 4 │ der Große Traptor │ der Vulkan-Fraptor │ der Hamsterer-Fraptor │ der Kokosnuss-Smoothie │ Gelbe Flaschenverschlüsse │ │ 5 │ der Restless Traptor │ der Mountain Traptor │ der Snapper Traptor │ der Kiwi-Smoothie │ Blaue Flaschenverschlüsse │ └──────┴──────────────────────── ┴──────────────────────────┴───── ────────────────────┴──────────── ────────────┴───────────────────┘
Was muss ich im Februar 2024 tun, um dies als „erledigt“ zu betrachten?
Fügen Sie HTML-Vorlagen hinzu, da die Website, für die ich diese erstelle, erfordert, dass ich Dinge wie BR-Tags einbinde.
Verbessern Sie die Grammatikdetails in der Ausgabe, wie z. B. die Groß- und Kleinschreibung im Flavour-Text.
Fügen Sie die Kopf-/Fußzeilenressourcen hinzu, die ich kopiere/in die Einreichung einfüge.
Vielleicht werde ich eines Tages über ein Webinterface nachdenken. Könnte ich das Projekt mit Pyodid vorantreiben, oder würde das C-basierte Pycosat Probleme verursachen? Was ist mit einer anderen Logikprogrammierschnittstelle wie PySAT, Antwortsatzprogrammierung oder anderen aus diesem HN-Thread?
Dies kann passieren. Aber das Projekt ist endlich an einem Punkt angekommen, mit dem ich zufrieden bin, und deshalb freue ich mich darauf, es zu teilen und darüber zu schreiben.
2/18: Ausgaben einfacher, weniger ausführlich und hübscher gestalten. Aktualisieren Sie diese README-Datei mit neuen Formatierungen und Änderungen. Verwenden Sie endlich den Puzzle-Generator, um ein neues Puzzle zu erstellen!
17.02.: Puzzle-Signatur aktualisieren, um nur die Lösung zu akzeptieren und daraus die Elemente und Elementklassen abzuleiten. Fügen Sie der Lösung eine schönere Anzeige hinzu.
26.11.: Bereinigen Sie die Logik zur Rätsel-/Lösungsgenerierung. Lassen Sie den Benutzer die Puzzlegröße auswählen.
25.11.: Benennen Sie einige gängige Typen als Typaliase (danke, Python 3.12). Verwenden Sie Protokollierung statt Ausdrucke.
Fügen Sie Tests für Hinweistypen in generate.py
hinzu.
Beheben Sie einen Fehler, den ich in clues.py
eingeführt habe. Diese Datei ist so schwer zu verstehen, aber es ist auch schwierig, dafür Unit-Tests zu schreiben. Das manuelle Konvertieren boolescher Ausdrücke in CNF macht keinen Spaß.
Passen Sie die Gewichtung der Hinweise in der Lösung an. Bereiten Sie sich auf die Integration der Rätsel- und Lösungsklassen vor.
Entfernen Sie die Kontrollkästchen-artige Smoothie-Auswahl, da sie beim schnellen Lösen von Rätseln nur im Weg ist.
Fügen Sie weitere Tests hinzu. Beenden Sie die Unit-Tests für sat_utils.py
und starten Sie ein paar für clues.py
, obwohl diese Datei aufgrund der Schwierigkeit der manuellen Berechnung von DNF-zu-CNF-Konvertierungen sehr schwer zu testen ist.
Die nächsten Schritte bestehen darin, das Rätsel und die Lösung zu vereinheitlichen, ein besseres __repr__
zu erstellen und die Art und Weise zu vereinfachen, wie wir die Größe des Rätsels darstellen (Attribut auf Puzzle
, Tupel von Ints 1 bis N, nur die Anzahl n_houses
usw.).
Schwarz entfernen und Ruff zum Formatieren verwenden. Abhängigkeiten aktualisieren. Fügen Sie eine neue CLI mit einfacherer und klarerer Verwendung hinzu. python -m src.main
.
SATLiteral
umbenennen -> PuzzleElement
(Smoothie, Katze usw.); Dies verdeutlicht, dass es sich nicht um ein Literal im booleschen Sinne handelt, sondern vielmehr um einen Namen für beispielsweise Zeichen in einem Puzzle.
Erstellen Sie einen neuen Typ SATLiteral
(ein str
im Trenchcoat); Dies stellt das Literal im Sinne einer booleschen Variablen dar, etwa „Wert el liegt am Hausstandort “ oder „Wert el liegt nicht am Hausstandort “. Intern werden diese durch eine ganze Zahl i und ihr negatives Gegenstück -i dargestellt.
Verwenden Sie (das neue) SATLiteral
als Rückgabetyp von comb(el: str, loc: int) -> SATLiteral
, um Puzzle-Elemente Literalen zuzuordnen, und neg(el: SATLiteral) -> SATLiteral
um ein Literal zu negieren.
Clause: tuple[SATLiteral, ...]
das ein „∨“ (boolesches ODER; Disjunktion) von Literalen darstellt; Beispielsweise ist (1, -5, 6)
eine Disjunktion, die angibt, dass x_1
wahr ist, x_5
nicht wahr ist oder x_6
wahr ist.
Fügen Sie ClueCNF: list[Clause]
hinzu, das ein „∧“ (boolesches AND; Konjunktion) von Clause
s darstellt. Ein Rätsel in CNF ist ein „UND von ODER“ („∧ von ∨s“ oder „∧ von Klauseln“).
Drucken Sie das Puzzle deutlicher aus. Reduzieren Sie die Ausführlichkeit der Hinweisreduzierung.
Generiere das Puzzle (mit einem Startwert) bei jedem Durchlauf zufällig.
Verschieben Sie Beispiele in ihre eigenen Dateien. Update auf Python 3.12 (Beta). Fügen Sie weitere Lint-Regeln hinzu. Importe bereinigen.
Entwicklungstools hinzufügen (Black, Ruff, Pyright); Führen Sie Black & Ruff im Pre-Commit aus. Aktualisieren Sie einige Typen.
„∧“ ist das boolesche UND
„∨“ ist das boolesche ODER
Eine Klausel ist ein „∨ von Literalen“
Ein CNF ist ein „∧ von Klauseln“ oder äquivalent ein „∧ von ∨s“ („AND von ORs“)
Im Gegensatz dazu ist ein DNF ein „∨ von ∧s“. Der DNF ist die Antwort auf ein SAT-Problem; Ein DNF von „A oder B oder C“ besagt, dass A, B und C alle gültige (erfüllende) Zuweisungen sind. Die Umwandlung eines CNF in einen DNF ist daher NP-schwer, da man aus dem DNF Lösungen zum CNF ablesen kann.
CNF ist ein ∧ von ∨s, wobei ∨ über Variablen oder ihren Negationen (Literalen) steht; Ein ∨ von Literalen wird auch Klausel genannt. DNF ist ein ∨ von ∧s; Ein ∧ von Literalen wird als Term bezeichnet.
Der Kern dieses Projekts besteht darin, das Zebra-Puzzle als boolesches Erfüllbarkeitsproblem (SAT) auszudrücken (Wikipedia).
Das 3-SAT-Problem ist bekanntermaßen NP-vollständig . Das heißt, es gibt wahrscheinlich keinen polynomiellen Algorithmus, um es zu lösen. Dies beschreibt jedoch nur den allgemeinen Fall.
Unser Problem ist klein und genau spezifiziert (schließlich erstellen wir diese speziell für Menschen!). Dadurch eignet es sich hervorragend für moderne SAT-Löser, und Hettingers Vortrag (und Notizen) demonstrieren dies wunderbar.