ANTLR - логическое удовлетворение

Question

У меня есть синтаксический анализатор выражений ANTLR, который может оценивать выражения формы ( A & ( B | C)), используя сгенерированный посетитель. A, B и C могут принимать любое из 2 значений true или же false, Однако передо мной стоит задача найти все комбинации A, B и C, для которых это выражение верно. Я попытался решить эту проблему следующим способом.

1. Оцените выражение для 3 переменных, принимающих true и false каждая
2. Это касается 8 комбинаций, так как 2 ^ 3 равно 8
3. Я оцениваю предоставление значений, таких как 000, 001, 010 ....... 111, переменным и оцениваю с помощью посетителя

Несмотря на то, что это работает, этот метод становится интенсивнее вычислений по мере увеличения числа переменных. Следовательно, для выражения с 20 переменными требуется 1048576 вычислений. Как я могу оптимизировать эту сложность, чтобы получить все истинные выражения? Я надеюсь, что это подпадает под булеву проблему

Answer 1

Оно делает. Если вы ограничены 20-30 переменными, вы можете просто перебрать все комбинации. Если на одну попытку требуется 100 нс (это 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;

Скомпилированный (или даже JITted Java), я ожидал бы, что внутренний цикл будет принимать 1-2 машинных инструкции на логическую операцию, касаясь только регистров или одной строки кэша, плюс 2 для цикла. Для 20 переменных это около 42 машинных инструкций, даже лучше, чем моя грубая оценка в первом абзаце.

Если кто-то настаивает, он может преобразовать внешние циклы (3 или 4) в параллельные потоки, но если вам нужны только операторы print, я не понимаю, как это будет иметь значение с точки зрения полезности.

Если у вас много этих формул, легко написать генератор кода, который будет генерировать это из любого представления формулы (например, дерева разбора ANTLR).