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

如果您首先生成真值表（相当简单），这将简化为经过充分研究的 circuit minimization problem,。

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)

映射到下面的真值表 I。但是，从您的示例中，我们知道（不是 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 插入 Logic Friday 并使用其求解器生成最小化 (CNF) 表达式：

A && (B || C)

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

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

Answer 4

我建议你建立一个决策树。

您的每个条件都将数字空间分为两个部分。例如c > 1 将空间划分为(-Infinity, 1] 和[1, +Infinity) 部分。如果您有 c 的另一个条件，例如 c>0，那么您有额外的分割点 0，最后您会得到 3 个部分：(-Infinity, 0]、[0,1] 和 [1, +Infinity)。

因此，每个树级别都将包含适当的分支：

c<0
   b<0
      a<0
      a>0  
   b>0
      a<0
      a>0  
0<c<1
   b<0
      a<0
      a>0  
   b>0
      a<0
      a>0  
c>1
   b<0
      a<0
      a>0  
   b>0
      a<0
      a>0  

现在您应该只保留表达式中存在的路径。这将是您的优化。不确定它是否 100% 有效，但它在某种程度上是有效的。

你的情况是

c<0
   b<0: false
   b>0
      a<0: true
      a>0: false  
0<c<1
   b<0
      a<0: true
      a>0: false  
   b>0
      a<0: true
      a>0: false  
c>1
   b<0
      a<0: true
      a>0: false  
   b>0
      a<0: true
      a>0: false  

为了提高优化，您可以将子树比较和联合等效子树合并到一个中

c<0
   b<0: false
   b>0
      a<0: true
      a>0: false  
c>0
   a<0: true
   a>0: false  

最后，当您收到您的值时，只需跟踪树并检查您的决定。如果您遇到死胡同（已删除路径），则结果为false。否则你会追踪到退出，结果将是true。

Answer 5

您也许可以从 BDD 库中获得所需的内容。 BDD 并没有在最后给你一个 C++ 表达式，但它们给你一个图表，你可以从中构造一个 C++ 表达式。

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

Answer 6

简化该表达式的最佳工具是编译器的优化器。

据我所知，没有 c++ 库会为您重写这样的表达式（尽管从技术上讲，使用表达式模板编写一个表达式是可能的）。

我建议查看由您的编译器生成的经过高度优化的汇编代码。它可能会给你一个提示。静态分析工具提供了另一种选择。