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？选择 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 来提升该项目吗？或者基于 C 的 pycosat 会导致问题吗？另一个逻辑编程接口（例如 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 的演讲（和笔记）完美地证明了这一点。
