ANTLR - 布尔satisfiabilty

Question

我有ANTLR表达式分析器，其可以评估的形式的表达式|使用所生成的访问者（A &（B C））。 A，B和C可以采用2值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秒内运行。这比你快。

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

EDIT由于OP此言约试图去平行于加快Java程序，野蛮势力答案：

我不知道你是怎么表现你的布尔公式。对于蛮力，你不想解释一个公式树或做其他很慢的事情。

一个关键技巧是让布尔公式快速的评价。对于大多数编程语言，你应该能够编写公式，以测试在用手该语言的天然表达，把它包装ñ嵌套循环和编译整个事情，例如，

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），我希望innner循环每布尔操作需要1-2条机器指令，只接触寄存器或单个cachec行，加上2个循环。 对于大约42条机器指令的20个变量，甚至比我在第一段中的粗略估计还要好。

如果一个坚持，一个可以转换的最外层循环（3或4）转换成并行线程，但是如果你想要的是打印语句我不明白如何将实际在实用性方面关系。

如果有许多这些公式，很容易编写的代码发生器，从你具有式（例如，ANTLR解析树）的任何表示产生这种。