ANTLR - 布尔可满足性

Question

我有一个 ANTLR 表达式解析器，它可以使用生成的访问者评估 ( A & ( B | C ) ) 形式的表达式。 A 、 B 和 C 可以采用 true 或 false 两个值中的任何一个。然而，我面临着找到表达式为真的 A、B 和 C 的所有组合的挑战。我尝试通过以下方法解决。

1. 计算 3 个变量的表达式，每个变量取真假
2. 这是 8 种组合，因为 2 ^ 3 是 8
3. 我评估将 000、001、010 ...... 111 等值赋予变量并使用访问者进行评估

虽然这种方法可行，但随着变量数量的增加，这种方法会变得计算密集。因此，对于具有 20 个变量的表达式，需要进行 1048576 次计算。我怎样才能优化这种复杂性，以便获得所有真实的表达方式？我希望这属于Boolean satisfiabilty problem

Answer 1

确实如此。如果您仅限于 20-30 个变量，您可以简单地强制尝试所有组合。如果每次尝试需要 100ns（即 500 条机器指令），它将在大约 100 秒内运行。那比你快。

如果你想解决比这更大的方程，你需要构建一个真正的约束求解器。

编辑由于 OP 关于尝试并行加速一个蛮力回答的 Java 程序的评论：

我不知道您如何表示布尔公式。对于蛮力，您不想解释公式树或执行其他缓慢的操作。

一个关键的技巧是使布尔公式的评估快速。对于大多数编程语言，您应该能够手动编写公式以测试该语言中的本机表达式，将其包装 N 个嵌套循环并编译整个内容，例如，

A=false;
do {
     B=false;
     do {
          C= false;
          do { 
               if (A & (B | C) ) { printf (" %b %b %b\n",A,B,C);
               C=~C;
             } until C==false;
          B=~B;
        } until B==false;
     A=~A;
   } until A==false;

编译（甚至由 Java 进行 JIT），我希望内部循环每个布尔运算需要 1-2 个机器指令，仅涉及寄存器或单个缓存行，加上 2 个循环。 20 个变量大约是 42 条机器指令，甚至比我在第一段中的粗略估计还要好。

如果有人坚持，可以将最外层的循环（3 或 4 个）转换为并行线程，但如果你想要的只是打印语句，我看不出这在实用性方面有什么实际意义。

如果您有许多这样的公式，则很容易编写代码生成器来根据您对公式的任何表示（例如，ANTLR 解析树）生成它。