简化布尔表达式算法

Question

有人知道一个简化布尔表达式的算法吗？

我记得布尔代数和Karnaught地图,但这适用于EVERITHING为布尔值的数字硬件.我想要考虑一些子表达式不是布尔值的东西.

例如:

a == 1 && a == 3

这可以转换为纯布尔表达式:

a1 && a3 

但这是表达是不可简化的,而对于算术的一点点知识,everibody可以确定表达式只是:

false

有些人知道一些链接？

Answer 1

您可能对K-maps和Quine-McCluskey算法感兴趣.

我认为SymPy能够解决和简化布尔表达式,查看源代码可能很有用.

Answer 2

您的特定示例将由SMT 求解器解决。（它确定变量的任何设置都不能使表达式为真；因此它始终为假。更一般的简化超出了此类求解器的范围。）表明表达式等效于true或false当然是 N​​P-hard 甚至没有在交易中加入算术，所以即使有这么多实用的软件也很酷。根据范围内有多少算术知识，问题可能是不可判定的。

Answer 3

这个问题有两个部分，逻辑简化和表示简化。

为了逻辑简化，Quine-McCluskey。为了简化表示，使用分布标识 (0&1|0&2) == 0&(1|2) 递归提取项。

我在这里详细介绍了这个过程。这给出了仅使用 & 和 | 的解释，但可以对其进行修改以包括所有布尔运算符。

Answer 4

使用 Google 的第一次拍摄发现了这篇论文：

http://hopper.unco.edu/KARNAUGH/Algorithm.html

当然，这不涉及非布尔子表达式。但后一部分的一般形式确实很难，因为绝对没有算法来检查任意算术表达式是真、假还是其他。您所要求的内容深入到编译器优化领域。