我有一个由真值表表示的 bool 函数。
总共有10个变量,我想得到一个合理长度的CNF(不一定是最短的,但足够短)。
我该怎么做?
Python 脚本或任何公共(public)可用的软件(例如 Mathematica/Mapple/etc)也适合我。
最佳答案
sympy
包允许您开箱即用地执行此操作。 (https://www.sympy.org/en/index.html)
这是一个简单的例子。假设您有三个变量,并且真值表对以下集合进行编码:
(x & y & !z) \/ (x & !y & z)
(即,只有与 x=true, y=true, z=false
和 x=true, y=false, z=true
对应的行是 true
,而所有其他都是 false
)。您可以轻松地对其进行编码并转换为 CNF,如下所示:
$ 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
可以根据 form
参数转换为 CNF 或 DNF。参见这里:https://github.com/sympy/sympy/blob/c3087c883be02ad228820ff714ad6eb9af1ad868/sympy/logic/boolalg.py#L2746-L2827
请注意,CNF 扩展通常成本高昂,而 Tseitin 编码是避免这种复杂性的首选方法 ( https://en.wikipedia.org/wiki/Tseytin_transformation )。但它的缺点是引入了新的变量。
关于python - CNF 真值表,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/64562464/