ANTLR — логическая выполнимость

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

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

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


person ssdimmanuel    schedule 02.12.2016    source источник
comment
Это был близкий ответ, который все еще нуждается в исследовании с моей стороны. Я ждал, чтобы увидеть, будет ли больше ответов   -  person ssdimmanuel    schedule 04.12.2016


Ответы (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;

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

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

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

person Ira Baxter    schedule 02.12.2016
comment
Спасибо за ответ. Даже для 20 переменных я использовал многопоточную программу на Java, чтобы быстрее получать результаты. Существуют ли какие-либо библиотеки решения ограничений с открытым исходным кодом? - person ssdimmanuel; 03.12.2016
comment
Решатель ограничений с открытым исходным кодом: выглядит довольно многообещающе: gecode.org - person Ira Baxter; 03.12.2016
comment
Большое спасибо !! gecode кажется библиотекой C++. Одна из библиотек Java, с которой я столкнулся, это [SAT4j] (sat4j.org). Однако я новичок в этом и должен посмотреть, как я могу адаптировать их к своему Java-приложению. В документации говорится, что логическое выражение должно быть преобразовано в форму CNF перед использованием решателей SAT. Надеюсь, мне понадобится некоторое время, чтобы привыкнуть к используемым соглашениям. - person ssdimmanuel; 03.12.2016
comment
Поиск дал [Choco Solver]( choco-solver.org), который показался мне многообещающим. . Он использует целочисленные и логические ограничения. Но мои бизнес-правила также проверяют строки. Я застрял в том, как преобразовать мою бизнес-проблему в проблему ограничений. Любая помощь приветствуется - person ssdimmanuel; 16.12.2016
comment
Вопрос о том, как использовать решатель ограничений со строками, отличается от этого вопроса. Вы должны начать новый вопрос и убедиться, что вы предоставили больше деталей, чем проверяли строки. Если вы оставите здесь ссылку на этот вопрос, я обязательно ее посмотрю. - person Ira Baxter; 16.12.2016
comment
Я задал новый вопрос stackoverflow.com/questions/41198639/ - person ssdimmanuel; 17.12.2016