zebra
1.0.0
2024 年の現在、プロジェクトはほとんどメンテナンスされていません。私はこれを試してみたいことのための遊び場として使用していますが、これを基にして構築することはお勧めしません。
次のような論理パズルを覚えていますか?彼らは次のような手がかりを持っていました。
トゥシャールとマウイの間に一軒の家があります。
ルビーの好きなビデオゲームはポケモンです。
チャイを飲む人は青色が好きではありません。
私は子供の頃からこれらの問題が大好きで、Raymond Hettinger の PyCon 2019 の講演を見て、これらの問題を再検討するきっかけになりました。彼はそれらを解決する方法を私たちに教えてくれました。それらを生成する方法を学びたかったのです。
最新の Python と制約満足 (SAT) ソルバーを使用するこのプロジェクトを使用して、ランダムなゼブラ パズルを作成できます。
このプロジェクトでは Python 3.12 と Poetry を使用します。
このプロジェクトへのエントリポイントはsrc/main.pyです。したがって、 [poetry run] python -m src.mainで実行します。質問を使用して、シンプルな対話性を備えた CLI を作成します。
その他の重要なファイルは次のとおりです。
puzzle.pyにはメインの Puzzle クラスが含まれており、主に手がかりとパズル要素の周りに接着されています。
clues.py手がかり (CNF に変換できる高レベルのステートメント) と、 found_atやsame_houseなどのいくつかのファクトリーを定義します。 generate.py手がかりを作成するユーティリティがあります
elements.pyとtraptor_elements.pyにはさまざまなパズル要素があります
最後に、 sat_utils.pyは、SAT ソルバー pycosat と対話するための基本ユーティリティが含まれています。このコードは、ほぼ完全に Raymond Hettinger が 2019 年の講演のために書いたものです (ありがとう!)。
❯ 詩は Python -m src.main を実行しますか?パズルの大きさはどのくらいですか? (矢印キーを使用します)
» 5
4
3?トラプターのタイプを選択します (矢印キーを使用します)。
?トロピカル
» ?神話的な？ ?パズルにはスムージーを含めるべきですか? (矢印キーを使用します)
" はい
いいえ？ ?パズルにはボトルキャップを含めるべきですか? (矢印キーを使用します)
" はい
いいえ
手がかり
-----# ... フレーバーテキスト一部省略 ...1．レッサー トラプターとスワンプ トラプターは同じ家にいます。
2. エンシェント トラプターはチョコレート スムージーのすぐ左にあります。
3. エンシェント トラプターとレモン スムージーは同じ家にあります。
4. Volcano Traptor は Restless Traptor のすぐ左にあります。
5. Cave Traptor と緑のボトルキャップは同じ家にあります。
6. レイク トラプターとスナッパー トラプターの間に 2 軒の家があります。
7. 緑のボトルキャップと激しいトラプターは同じ家にあります。
8. 黒いボトルキャップとココナッツスムージーの間に一軒の家があります。
9. レッサー トラプターとキウイ スムージーの間に家が 1 つあります。
10. ドゥウェラー トラプターとチョコレート スムージーは同じ家にあります。
11. 赤いボトルキャップとドゥウェラー トラプターは同じ家にあります。
12. 赤いボトルキャップはホーダー トラプターのすぐ左にあります。
13. スターフルーツのスムージーと黄色いボトルキャップの間に家が 2 つあります。
14. レイク トラプターと黒いボトルキャップは同じ家にあります。
15. ストーカー トラプターと激しいトラプターは同じ家にいます。
解決
┏━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━━ ━━━━━━━━━┳━━━━━ ━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━ ━━━━━━━━━━━━━━━┓
│ ネスト │ MythicalTraptorPrimary │ MythicalTraptorSecondary │ MythicalTraptorTertiary │ スムージー │ ボトルキャップ │
┡━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━━ ━━━━━━━━━╇━━━━━ ━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━ ━━━━━━━━━━━━━━━┩
│ 1 │ 熾烈なトラプター │ ケイブ・トラプター │ ストーカー・トラプター │ スターフルーツ・スムージー │ 緑のボトルキャップ │
│ 2 │ エンシェント・トラプター │ レイク・トラプター │ クローラー・トラプター │ レモンスムージー │ 黒いボトルキャップ │
│ 3 │ レッサー トラプター │ スワンプ トラプター │ ドゥウェラー トラプター │ チョコレート スムージー │ 赤いボトルキャップ │
│ 4 │ グレーター トラプター │ ボルケーノ トラプター │ ホーダー トラプター │ ココナッツ スムージー │ 黄色いボトルキャップ │
│ 5 │ 落ち着きのないトラプター │ マウンテン トラプター │ スナッパー トラプター │ キウイのスムージー │ 青いボトルキャップ │
━─────┴─────────┴─────── ─────┴───────────┴─────── ──────┴───────────┘2024 年 2 月にこれを「完了」とみなすには何が必要ですか?
HTML テンプレートを追加します。これを構築するサイトでは BR タグなどを含める必要があるためです。
フレーバー テキストの大文字化など、出力の文法を改善します。
ヘッダー/フッターのリソースをコピーして提出物に貼り付けます。
いつか、Web インターフェースを検討するかもしれません。ピオダイドを使用してプロジェクトを持ち上げることはできますか? それとも C ベースのピコサットが問題を引き起こすでしょうか? PySAT、解答セット プログラミング、またはこの HN スレッドのその他のロジック プログラミング インターフェイスについてはどうですか?
これらのことが起こる可能性があります。しかし、このプロジェクトは最終的に私が満足できる段階に達したので、それについて共有し、書くことに興奮しています。
2/18: 出力をよりシンプルにし、冗長さを減らし、よりわかりやすくします。新しいフォーマットと変更を加えてこの README を更新してください。パズル ジェネレーターを使用して、ついに新しいパズルを作成します。
2/17: 解決策のみを受け入れるようにパズルの署名を更新し、そこから要素と要素クラスを推測します。ソリューションにさらに分かりやすい表示を追加します。
11/26: パズル/解決策生成ロジックをクリーンアップ。ユーザーがパズルのサイズを選択できるようにします。
11/25: いくつかの一般的な型に型エイリアスとして名前を付けます (Python 3.12 に感謝)。印刷の代わりにログを使用します。
generate.py内に手がかりタイプのテストを追加します。
clues.pyで導入したバグを修正します。このファイルは理解するのが非常に難しいですが、単体テストを記述するのも困難です。ブール式を手動で CNF に変換するのは楽しいことではありません。
ソリューション内の手がかりの重みを調整します。パズルとソリューションのクラスを統合する準備をします。
チェックボックス風のスムージー選択は、パズルをすばやく作成しようとするときに邪魔になるだけなので、削除します。
テストの追加を続けます。 sat_utils.pyの単体テストを終了し、 clues.pyの単体テストをいくつか開始します。ただし、DNF から CNF への変換を手作業で計算するのが難しいため、このファイルをテストするのは非常に困難です。
次のステップは、パズルと解決策を統合し、より適切な__repr__を作成し、パズルのサイズを表す方法 ( Puzzleの属性、1 から N までの整数のタプル、単なる数値n_housesなど) を簡素化することです。
黒を削除し、ラフを使用してフォーマットします。依存関係を更新します。よりシンプルで明確な使用法を備えた新しい CLI を追加します。 python -m src.main 。
SATLiteral -> PuzzleElement (スムージー、猫など) の名前を変更します。これは、これがブール値の意味でのリテラルではなく、パズル内の文字などの名前であることを明確にしています。
新しいタイプのSATLiteral (トレンチコートのstrです) を作成します。これは、「値elは house locにあります」または「値el はhouse locにありません」のような、ブール変数の意味でのリテラルを表します。内部的には、これらは整数iとその負の値-iで表されます。
(新しい) SATLiteral comb(el: str, loc: int) -> SATLiteralの戻り値の型として使用し、パズル要素をリテラルにマッピングし、 neg(el: SATLiteral) -> SATLiteral使用してリテラルを否定します。
Clause: tuple[SATLiteral, ...] 。たとえば、 (1, -5, 6) 、 x_1が true、 x_5が true ではない、またはx_6が true であることを示す論理和です。
Clauseの "∧" (ブール AND; 接続詞) を表すClueCNF: list[Clause]を追加します。 CNF のパズルは「OR の AND」(「∨ の∧」または「節の∧」) です。
パズルをより鮮明に印刷します。手がかり削減の冗長性を減らします。
実行するたびにパズル (シード付き) をランダムに生成します。
サンプルを独自のファイルに移動します。 Python 3.12 (ベータ版) に更新します。 lint ルールをさらに追加します。インポートをクリーンアップします。
開発ツール (black、ruff、pyright) を追加します。プリコミットでブラック＆ラフを実行します。一部のタイプを更新します。
「∧」はブール値の AND です。
「∨」はブール値の OR です。
句は「リテラルの∨」です
CNF は「∧ of Clauses」、または同等の「∧ of ∨s」（「AND of OR」）です。
対照的に、DNF は「∧ の ∨」です。 DNF は SAT の問題に対する答えです。 「A or B or C」という DNF は、A、B、および C がすべて有効な (満足のいく) 割り当てであることを示します。したがって、DNF から CNF への解を読み取ることができるため、CNF から DNF への変換は NP 困難です。
CNF は ∨ の ∧ であり、∨ は変数またはその否定 (リテラル) です。リテラルの ∨ は文節とも呼ばれます。 DNF は ∧ の ∨ です。リテラルの ∧ は項と呼ばれます。
このプロジェクトの核心は、ゼブラ パズルをブール充足可能性(SAT) 問題として表現することにあります (Wikipedia.
3-SAT 問題はNP 完全問題として知られています。つまり、おそらくそれを解決する多項式時間アルゴリズムは存在しません。ただし、これは一般的なケースについてのみ説明しています。
私たちの問題は小さく、明確に規定されています (結局のところ、私たちは特に人間のためにこれらを作成しているのです!)。このため、これは現代の SAT ソルバーに最適であり、ヘッティンガーの講演 (およびメモ) はこれを見事に示しています。
