逻辑模块的改进

Sachin, Chris, 我注意到你写了我在这里提到的大部分代码。在逻辑模块中，我有些不喜欢的地方：- [ ] to_cnf 不够高效，特别是如果你只关心满足性。这是问题 #7174。- [ ] 如果你想要精确的等价，而不仅仅是满足性等价，那么对于 to_cnf 没有太多可以做的，但如果它能够去除明显的冗余项，例如 x | ~x，或者有个函数可以做到这一点，那就太好了。- [ ] simplify_logic 有一点误导，因为它实际上试图返回某种正常形式，而这可能并不是“最简单”的（例如，我将 Implies(x, y) 看作比 y | ~x 更简单）。此外，如上所述，如果只有一个函数来清理表达式中的一些明显冗余，例如 x | ~x，那就太好了。- [x] 除此之外， simplify_logic 不允许你选择是否使用 POS 还是 SOP。如果两者的长度相同，它会选择 SOP。这些问题的结果是，有时很难获得表达式的最小 cnf 形式。to_cnf 返回一个包含 x | ~x 的大型表达式，而 simplify_logic 返回 dnf 形式。- [ ] POSform 和 SOPform 接收的输入不是符号。- [x] 为什么 to_dnf 不在 `__init__.py` 中？- [ ] bool_equal 非常混淆。我误用了它一段时间。它的意思是“存在”对应关系，而名称暗示两个表达式在“所有”对应关系中是等价的。- [ ] 我还没有深入分析它，但 bool_equal 似乎效率低下。如果问题 7174 被修复，使用满足性会更快。逻辑表达式 a 和 b 具有匹配的对应关系，如果 satisfiable(Equivalent(a, b)) 返回一个模型。如果 satisfiable(Not(Equivalent(a, b))) 返回 False，则它们是完全相等的。- [x] 这已经有另一个问题了，但我们迫切需要 True 和 False 的基本类型。我已经厌倦了在各处特殊处理它们了。最糟糕的是，如果你做了类似 ~Equivalent(a, b) 的操作，而不是 Not(Equivalent(a, b))，并且 a 和 b 实际上是完全相同的（因此 Equivalent 只返回 True），表达式会降为 ~True，即 ~1，这给出了 -2，这在逻辑上不是假的。除此之外，当一个函数没有考虑到 True 或 False 输入的可能性，并且因此在简单的输入上抛出异常时，这很令人讨厌。