提问人：knst 提问时间：10/28/2020 最后编辑：knst 更新时间：11/2/2020 访问量：1005
CNF by truth table [已关闭]
CNF by truth table [closed]
问：
闭。这个问题正在寻求有关书籍、工具、软件库等的建议。它不符合 Stack Overflow 准则。它目前不接受答案。
我们不允许向读者、工具、软件库等寻求推荐的问题。您可以编辑问题，以便用事实和引文来回答。
3年前关闭。
我有一个由真值表呈现的布尔函数。
总共有 10 个变量，我想得到一个合理长度的 CNF（不一定是最短的，但足够短）。
我该怎么做？
Python 脚本或任何公开可用的软件，如 Mathematica/Mapple/etc 对我来说也可以正常工作。
答：
2赞
alias
11/1/2020
#1
该软件包允许您开箱即用。（https://www.sympy.org/en/index.htmlsympy)
下面是一个简单的示例。假设您有三个变量，并且真值表对以下集合进行编码：
(x & y & !z) \/ (x & !y & z)
（即，只有对应于 和 的行是 ，而所有其他行都是 ）。您可以轻松地对此进行编码并转换为 CNF，如下所示：x=true, y=true, z=falsex=true, y=false, z=truetruefalse
$ python3
Python 3.8.5 (default, Jul 21 2020, 10:48:26)
[Clang 11.0.3 (clang-1103.0.32.62)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> from sympy import *
>>> x, y, z = symbols('x y z')
>>> simplify_logic((x & y & ~z) | (x & ~y & z), form="cnf")
x & (y | z) & (~y | ~z)
simplify_logic可以根据参数转换为 CNF 或 DNF。请参阅此处：https://github.com/sympy/sympy/blob/c3087c883be02ad228820ff714ad6eb9af1ad868/sympy/logic/boolalg.py#L2746-L2827form
请注意，CNF 扩增通常可能代价高昂，而 Tseitin 编码是避免这种复杂性的首选方法 （https://en.wikipedia.org/wiki/Tseytin_transformation）。但它的缺点是引入了新的变量。
评论
0赞
knst
11/2/2020
效果不快（计算几分钟），但非常好！我微不足道的优化将 CNF 从 530 个条件最小化到 279 个，但只给了我 190 个条件，这是一个很大的改进！sympy
评论