ANTLR

Question

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

计算 3 个变量的表达式，每个变量取 true 和 false
因为 2^3 是 8，所以有 8 个组合
我评估给变量赋值，如 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 编译），我希望内部循环每个布尔操作采用 1-2 条机器指令，仅涉及寄存器或单个缓存行，外加 2 条循环. 对于 20 个变量，大约 42 条机器指令，甚至比我在第一段中的粗略估计还要好。

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

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

ANTLR - 布尔可满足性

ANTLR - Boolean satisfiabilty

java

boolean

logic

satisfiability