问题描述
总共有10个变量,我想获得具有合理长度的CNF(不必最短,但足够短)。
我该怎么办?
Python脚本或任何公共可用的软件(例如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)。但这有引入新变量的缺点。