Как проверить, эквивалентны ли два булевых выражения

Question

Как узнать, эквивалентны ли два булевых выражения?

String expr1 = "(A or B) and C"; 
String expr2 = "C and (B or A)"; 
boolean equals = areExprsEquals(expr1, expr2); 

Я думаю, что я должен ...

1. Разбираем expresion хранения в некоторых данных о структуре
2. Снизить expresion в OR группы
3. Проверьте, если два имеют как выражения одинаковые группы

Например, с шага два я получаю:

Expr1 
(A or B) and C 
Converted to: 
(A and C) or (B and C) 

Expr2 
C and (B or A) 
Converted to: 
(C and B) or (C and A) 

Теперь я должен знать, имеют ли те же группы. Одним из способов может быть получение хэш каждой группы:

EXP1:

group 1: 
(A and C) 
Order: 
(A and C) 
Hash: 
md5("a&c") 

group 2: 
(B and C) 
Order: 
(B and C) 
Hash: 
md5("b&c") 

exp2:

group 1: 
(C and B) 
Order: 
(B and C) 
Hash: 
md5("b&c") 

group 2: 
(C and A) 
Order: 
(A and C) 
Hash: 
md5("a&c") 

Итак:

expr1: md5(sort(md5("a&c"), md5("b&c"))) 
expr2: md5(sort(md5("b&c"), md5("a&c"))) 

Я могу сделать md5 каждой группы , sort и expr hash - это md5 всех хешей.

Но проблема в том, что ... Как уменьшить exprs? Есть ли какой-нибудь алгоритм? В выражениях используются только операторы AND и OR.

Answer 1

Есть ли алгоритм?

Теоретический ответ:

• Проблема вашей пытаются решить это Boolean Satisfiability Problem также известный как SAT.

• Это NP-complete.

• ЭТО ЗНАЧИТ, что нет известных алгоритмов , которые всегда находят решение для задачи SAT в полиномиальное время; то есть нет алгоритма, в худшем случае которого O(N^C) или выше, где C является константой, а N - числом переменных в задаче SAT.

• Существует очевидное решение, которое представляет собой O(2^N) ... грубой поиск пространства решения. Существуют лучшие алгоритмы; см. the Wikipedia article, но они все экспоненциальны в худшем случае.

Практические решения:

• Для очень маленького N, грубая сила может дать приемлемую производительность.

• Используйте существующий SAT-решатель, имея в виду, что теория говорит о том, что она имеет экспоненциальное поведение в худшем случае.

• Избегайте проблем с большими N ... или закодируйте приложение так, чтобы решатель был «время в коробке»; то есть он отказывается, если он не может получить решение в установленное время.

---

^{1 - Если когда-либо доказано, что P == NP, то лучше алгоритмы могут возникнуть для этого и других NP-полных задач.}