ANTLR - 布尔可满足性 [英] ANTLR - Boolean satisfiabilty

问题描述

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

I have a ANTLR expression parser which can evaluate expressions of the form ( A & ( B | C ) ) using the generated visitor. A , B and C can take any of the 2 values true or false. However I am faced with a challenge of finding all combinations of A,B and C for which the expression is true. I tried to solve this by the following method.

1. 评估 3 个变量的表达式，每个变量取真假
2. 这有 8 种组合，因为 2 ^ 3 是 8
3. 我评估给变量提供 000、001、010 ....... 111 之类的值并使用访问者评估

虽然这种方法有效，但随着变量数量的增加，这种方法变得计算密集.因此，对于具有 20 个变量的表达式，需要 1048576 次计算.如何优化这种复杂性，以便获得所有真实的表达?我希望这属于布尔可满足性问题

Though this works this method becomes compute intensive as the number of variables increases. Hence for an expression with 20 variables 1048576 computations are required. How can I optimise this complexity so that I get all the true expressions ? I hope this falls under Boolean satisfiabilty problem

推荐答案

确实如此.如果您仅限于 20-30 个变量，您可以简单地对所有组合进行暴力试验.如果每次尝试需要 100ns(即 500 条机器指令)，它将在大约 100 秒内运行.这比你还快.

It does. If you are liimted to 20-30 variables, you can simply brute force a trial of all the combinations. If it takes 100ns per try (that's 500 machine instructions), it will run in about 100 seconds. That's faster than you.

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

If you want to solve much bigger equations than that, you need to build a real constraint solver.

由于 OP 关于尝试并行加速 Java 程序而进行的 OP 评论而进行编辑，该程序会暴力破解答案:

EDIT due to OP remark about trying to go parallel to speed up a Java program that brute forces the answer:

我不知道你如何表示你的布尔公式.对于蛮力，您不想解释公式树或做其他缓慢的事情.

I don't know how you represent your boolean formula. For brute force, you don't want to interpret a formula tree or do something else which is slow.

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

A key trick is to make evaluation of the boolean formula fast. For most programming languages, you should be able to code the formula to test as an native expression in that language by hand, wrap it N nested loops and compile the whole thing, e.g.,

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 条机器指令，仅涉及寄存器或单个 cachec 行，加上 2 条用于循环.对于大约 42 条机器指令的 20 个变量，甚至比我在第一段中粗略估计的还要好.

Compiled (or even JITted by Java), I'd expect the innner loop to take 1-2 machine instructions per boolean operation, touching only registers or a single cachec line, plus 2 for the loop. For 20 variables thats around 42 machine instructions, even better than my rough estimate in the first paragraph.

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

If one insists, one could convert the outermost loops (3 or 4) into parallel threads, but if all you want are the print statements I don't see how that will actually matter in terms of utility.

如果您有许多这样的公式，那么很容易编写一个代码生成器，根据您对公式的任何表示(例如，ANTLR 分析树)来生成它.

If you have many of these formulas, it is easy to write a code generator to produce this from whatever representation you have of the formula (e.g., ANTLR parse tree).

这篇关于ANTLR - 布尔可满足性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！