c ++线性公式简化库

Question

什么是最好的(在简单的使用和性能方面)C++/C++ 11库可以简化如下的公式？

(a < 0 && b > 0) || (a < 0 && c > 0) || (a < 0 && c > 1) 

到(例如)

a < 0 && (b > 0 || c > 0)

我认为解释一件事是非常重要的(因为我看到这个问题被误解了).

我不想简化C/C++表达式 - 我知道,编译器可以实现它.

我正在制作一个图形处理工具.在图形的边缘,有让关于其顶点某些情况下(比如顶点是a,b,c和这些条件都一样a<b,b>0等等-请注意,这些条件不表示为"弦",他们可以是任何功能或图书馆电话).在处理过程中,我正在收集表达式,在进一步的图形处理之前,我想简化它们.

条件和表达式将在运行时创建.

我希望能够向该库输入一些表达式,例如:

[...]
a = new Variable();
b = new Variable();
expr1 = lib.addExpr(a,0, lib.LESS);
expr2 = lib.addExpr(b,0, lib.MORE);
expr3 = lib.addExpr(expr1, expr2, lib.AND);
[...]
cout << lib.solve(exprn).getConditionsOf(a);

当然这个库可能会有更多漂亮的API.我把它写成方法调用只是为了展示我期望的底层机制 - 强调一点,我不需要源代码来源编译器,或者这个问题与源代码编译优化无关.

Answer 1

您正在寻找可以处理布尔逻辑的C++符号数学库.

以下是一些入门:

• SymbolicC++:用于C++的功能强大的通用符号数学库,但不是特别适用于布尔数学.
• BoolStuff:不是一个通用的符号数学库,非常注重布尔逻辑,但可能正是你想要的.
• Logic Friday:独立的数字电路分析工具和布尔逻辑简化器,带有C API.

Answer 2

如果你第一次生成真值表(相当简单),这就减少了电路最小化问题,这是一个很好的研究.

Answer 3

建议程序

代替专用库,我建议的解决问题的程序如下:

1. 为未简化的布尔表达式生成真值表.
2. 确定单变量比较表达式暗示同一变量的其他比较表达式的情况.如果您的用例具有完全代表性,那么这应该是直截了当的.
3. 将真值表输出标记为"不关心"(DNC),用于输入值违反含义的条目.
4. 使用真值表作为支持真值表和DNC的布尔表达式简化器的输入.正如Mahmoud Al-Qudsi所说,Logic Friday是一个很好的候选者,这就是我在下面的例子中使用的.

说明

假设您的给定用例完全代表问题空间,那么您可以使用任何支持真值表输入和"不关心"(DNC)函数输出规范的布尔表达式简化器.DNC之所以重要,是因为某些单变量比较表达式可能意味着同一变量的其他比较表达式.考虑以下单变量比较表达式到布尔变量映射:

A = (a < 0); B = (b > 0); C = (c > 0); D = (c > 1);

D暗示C或等效(不是D或C)始终为真.因此,在考虑示例表达式的输入时(替换我们新定义的布尔变量)

Output = (A && B) || (A && C) || (A && D)

当(不是D或C)为假时,我们不关心这个表达式的输入,也不关心这个表达式的输出,因为它永远不会发生.我们可以通过生成上述表达式的真值表来利用这一事实,并在(非D或C)为假的情况下将所需的输出标记为DNC.从该真值表中,您可以使用布尔表达式简化器来生成简化表达式.

例

让我们将该过程应用于您的示例,假设单变量比较表达式给出上面给出的布尔变量映射.特别是,我们有

Output = (A && B) || (A && C) || (A && D)

它映射到下面的真值表.但是,从你的例子中,我们知道(不是D或C)总是如此; 因此,我们可以将所有输出标记为(D而不是C)作为DNC,这导致下面的真值表II.

Truth Table I               Truth Table II
=============               ==============
A  B  C  D  Output          A  B  C  D  Output
0  0  0  0    0             0  0  0  0    0
0  0  0  1    0             0  0  0  1   DNC
0  0  1  0    0             0  0  1  0    0
0  0  1  1    0             0  0  1  1    0
0  1  0  0    0             0  1  0  0    0
0  1  0  1    0             0  1  0  1   DNC
0  1  1  0    0             0  1  1  0    0
0  1  1  1    0             0  1  1  1    0
1  0  0  0    0             1  0  0  0    0
1  0  0  1    1             1  0  0  1   DNC
1  0  1  0    1             1  0  1  0    1
1  0  1  1    1             1  0  1  1    1
1  1  0  0    1             1  1  0  0    1
1  1  0  1    1             1  1  0  1   DNC
1  1  1  0    1             1  1  1  0    1
1  1  1  1    1             1  1  1  1    1

将真值表II插入到星期五并使用其求解器产生最小化(CNF)表达式:

A && (B || C)

或等效地,从布尔变量映射回来,

a < 0 && (b > 0 || c > 0).

Answer 4

您也许可以从 BDD 库中获得您想要的东西。BDD 最后并没有给你一个 C++ 表达式，但它们给你一个图表，你可以从中构造一个 C++ 表达式。

我从未使用过它，但我听说 minibdd 很容易使用。请参阅http://www.cprover.org/miniBDD/