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个变量分别为true和false的表达式
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程序的野蛮言论而进行了编辑，从而导致了答案:

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的JITted)编译后，我希望innner循环每个布尔操作将接收1-2条机器指令，仅触摸寄存器或单个cachec行，并为该循环加上2条指令. 对于20个变量来说，这大约是42条机器指令，甚至比我在第一段中的粗略估计还要好.

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)转换为并行线程，但是如果只需要print语句，那么我就看不到实用程序的实际意义了.

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屋！