CNF按真值表 - 编程之家

如何解决CNF按真值表

总共有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）。但这有引入新变量的缺点。