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?選擇 Traptor 類型(使用箭頭鍵) ?熱帶 »?神話? ?謎題應該包括冰沙嗎? (使用箭頭鍵) 「 是的 不? ?拼圖應該包含瓶蓋嗎? (使用箭頭鍵) 「 是的 不 線索 -----# ...省略了一些風味文字...1。小猛禽和沼澤猛禽在同一棟房子裡。 2. 古代陷阱就在巧克力冰沙的左邊。 3.遠古猛禽和檸檬冰沙在同一棟房子裡。 4. 火山誘捕器位於不安誘捕器的正左側。 5. 洞穴猛禽和綠色瓶蓋在同一棟房子裡。 6. 在Lake Traptor 和Snapper Traptor 之間有兩棟房子。 7. 綠瓶蓋和猛龍在同一棟房子裡。 8. 黑瓶蓋和椰子冰沙之間有一間房子。 9. 小猛禽和奇異果冰沙之間有一棟房子。 10. 居民陷阱和巧克力冰沙在同一個房子裡。 11. 紅瓶蓋和居民陷阱在同一棟房子裡。 12. 紅色瓶蓋位於囤積者陷阱的正左側。 13. 楊桃冰沙和黃色瓶蓋之間有兩棟房子。 14. 特拉普托湖和黑瓶蓋在同一棟房子裡。 15. 追獵者陷阱和猛烈陷阱在同一棟房子裡。 解決方案 ┏────────────┳──────────────────────────────────────── ────────────┳────────────────────────────────────── ───────────────────────────────────────── ────────── ─────────┳──────────────────────────────────────── ────────────┳────────────────────────────────────── ───────────────────────────────────────── ────────── ───────────┳────────────────────────────────────── ──┓ ┃ 巢 ┃ MythicalTraptorPrimary ┃ MythicalTraptorSecondary ┃ MythicalTraptorTertiary ┃ Smoothie ┃ Bottlecap ┃ ┡────────────╇──────────────────────────────────────── ────────────╇────────────────────────────────────── ───────────────────────────────────────── ──────── ────────────────────────────────────────────────── ────────────────────────────────────────────────── ────────────────────────────────────────────────── ─────────────── ────────────────────╇──────────────── ────────────────────────┩ │ 1 │ 兇猛誘捕者 │ 洞穴誘捕者 │ 潛獵者誘捕者 │ 楊桃冰沙 │ 綠色瓶蓋 │ │ 2 │ 古代猛禽 │ 湖猛禽 │ 履帶猛禽 │ 檸檬冰沙 │ 黑色瓶蓋 │ │ 3 │ 小猛禽 │ 沼澤猛禽 │ 居民猛禽 │ 巧克力奶昔 │ 紅色瓶蓋 │ │ 4 │ 巨型誘捕者 │ 火山誘捕者 │ 囤積者誘捕者 │ 椰子奶昔 │ 黃色瓶蓋 │ │ 5 │ 躁動的掠食者 │ 山地掠食者 │ 鯛魚掠食者 │ 獼猴桃冰沙 │ 藍色瓶蓋 │ └──────┴────────────────────────┴────────────────── ─ ──────────┴──────────────────────────┴───────────── ─── ──────────┴────────────────────┘
2024 年 2 月,我需要什麼才算「完成」?
添加 HTML 模板,因為我建立這些模板的網站要求我包含 BR 標籤之類的內容。
改進輸出中的語法尼特,例如風味文字中的大寫。
新增我複製/貼上到提交中的頁首/頁尾資源。
也許有一天,我會考慮使用網路介面。我可以使用 pyodide 來提升該專案嗎?另一個邏輯程式介面(例如 PySAT、答案集程式設計或來自該 HN 執行緒的其他介面)呢?
這些都可能發生。但這個專案終於達到了令我滿意的地步,所以我很高興能分享和寫下它。
2/18:使輸出更簡單、更簡潔、更美。使用新的格式和變更更新此自述文件。最後,使用拼圖產生器建立一個新拼圖!
2/17:更新謎題簽名以僅接受解決方案,並從中推斷元素和元素類別。為解決方案添加更好的顯示。
11/26:清理謎題/解答產生邏輯。讓使用者選擇拼圖大小。
11/25:將一些常見型別命名為型別別名(感謝 Python 3.12)。使用日誌記錄代替列印。
在generate.py
中加入線索類型的測試。
修復我在clues.py
中引入的錯誤。該文件很難理解,但也很難為其編寫單元測試;手動將布林表達式轉換為 CNF 並不有趣。
調整解決方案中線索的權重。準備整合謎題和解決方案課程。
刪除複選框式的 Smoothie 選擇,因為它只會妨礙快速製作拼圖。
繼續添加測試。完成sat_utils.py
的單元測試,並啟動一對clues.py
的單元測試,儘管由於手動計算 DNF 到 CNF 轉換的困難,該檔案很難測試。
接下來的步驟是統一謎題和解決方案,創建更好的__repr__
,並簡化我們表示謎題大小的方式( Puzzle
上的屬性,整數 1 到 N 的元組,只是數字n_houses
等)。
去掉黑色並使用ruff進行格式化。更新依賴項。增加新的CLI,使用更簡單、更清晰; python -m src.main
。
重新命名SATLiteral
-> PuzzleElement
(冰沙、貓等);這澄清了它不是布林意義上的字面量,而是一個名稱,例如拼圖中的字元。
創建一個新類型SATLiteral
(它是風衣中的str
);這表示布林變數意義上的文字,例如「Value el is at house loc 」或「Value el is not at house loc 」。在內部,它們由某個整數i及其負數-i表示。
使用(新的) SATLiteral
作為comb(el: str, loc: int) -> SATLiteral
的返回類型,將拼圖元素映射到文字,並neg(el: SATLiteral) -> SATLiteral
來否定文字。
新增Clause: tuple[SATLiteral, ...]
表示文字的「∨」(布林 OR;析取);例如, (1, -5, 6)
是一個析取,表示x_1
為真、 x_5
不為真或x_6
為真。
加ClueCNF: list[Clause]
,表示Clause
s 的「∧」(布爾 AND;合取)。 CNF 中的難題是「OR 的 AND」(「∨ 的 ∧」或「子句的 ∧」)。
更清晰地列印拼圖。減少線索減少的冗長。
每次運行時隨機產生謎題(帶有種子)。
將範例移動到它們自己的文件中。更新至 Python 3.12(測試版)。增加更多 lint 規則。清理進口。
新增開發工具(black、ruff、pyright);在預提交中運行 black & ruff。更新一些類型。
「∧」是布林值 AND
「∨」是布林值 OR
子句是“文字的∨”
CNF 是“子句的 ∧”,或等效的“∨ 的 ∧”(“OR 的 AND”)
相比之下,DNF 是「∨ of ∧s」。 DNF 是 SAT 問題的答案; 「A 或 B 或 C」的 DNF 表示 A、B 和 C 都是有效(令人滿意)的分配。因此,將 CNF 轉換為 DNF 是 NP 困難的,因為從 DNF 中您可以讀出 CNF 的解決方案。
CNF 是 ∨ 的 ∧,其中 ∨ 是變數或其否定(文字);文字的 ∨ 也稱為子句。 DNF 是 ∧s 的 ∨;文字的 ∧ 稱為術語。
這個計畫的核心是將斑馬謎題表達為布林可滿足性(SAT)問題(維基百科)。
已知 3-SAT 問題是NP 完全問題。也就是說,可能沒有多項式時間演算法來解決它。但這僅描述了一般情況。
我們的問題很小而且很明確(畢竟,我們是專門為人類創建這些問題的!)。這使得它非常適合現代 SAT 求解器,Hettinger 的演講(和筆記)完美地證明了這一點。