CNF按真值表 [英] CNF by truth table

问题描述

我有一个由真值表显示的布尔函数.

I have a boolean function that is presented by truth table.

总共有10个变量，我想获得具有合理长度的CNF(不必最短，但足够短).

In total it is 10 variables and I'd like to get CNF with a reasonable length (not necessary the shortest, but short enough).

我该怎么办?

Python脚本或任何公共可用的软件(例如Mathematica/Mapple/etc)对我也可以正常工作.

Python script or any public available software such as Mathematica/Mapple/etc will work fine for me as well.

推荐答案

sympy 包使您可以立即执行此操作.( https://www.sympy.org/en/index.html )

The sympy package allows you to do this out-of-the box. (https://www.sympy.org/en/index.html)

这是一个简单的例子.假设您有三个变量，并且真值表对以下集合进行编码:

Here's a simple example. Assuming you've three variables and the truth table encodes the following set:

  (x & y & !z) \/ (x & !y & z)

(即，仅对应于 x = true，y = true，z = false 和 x = true，y = false，z = true 的行 true ，而所有其他均为 false ).您可以轻松地对此进行编码并按如下所示转换为CNF:

(i.e., only the rows corresponding to x=true, y=true, z=false and x=true, y=false, z=true are true, while all others are false). You can easily code this and convert to CNF as follows:

$ 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

simplify_logic can convert to CNF or DNF, based on the form argument. See here: https://github.com/sympy/sympy/blob/c3087c883be02ad228820ff714ad6eb9af1ad868/sympy/logic/boolalg.py#L2746-L2827

请注意，CNF扩展通常可能会非常昂贵，并且Tseitin编码是避免这种复杂性的首选方法( https://en.wikipedia.org/wiki/Tseytin_transformation ).但这有引入新变量的缺点.

Note that CNF expansion can be costly in general, and Tseitin encoding is the preferred method to avoid this complexity (https://en.wikipedia.org/wiki/Tseytin_transformation). But it has the disadvantage of introducing new variables.

这篇关于CNF按真值表的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！