CODEWITHSUNDEEP
javaboolean-logic
JoniJnm
JoniJnm

Reputation: 722

How to check if two boolean expressions are equivalent

How can I know if two boolean expresions are equivalent?

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

I think I should...

  1. Parse the expresion storing it in some structure data
  2. Reduce the expresion in OR groups
  3. Check if the two expresions have the same groups

For example, with the step two I get:

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)

Now I have to know if have the same groups. One way can be getting the hash of each group:

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")

So:

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

I can do the md5 of each group, sort, and the expr hash is the md5 of all hashs.

But the problem is... How can I reduce the exprs? Is there any algorithm? The expressions use only AND and OR operators.

Upvotes: 1

Views: 4091

Answers (1)

Stephen C
Stephen C

Reputation: 718758

Is there any algorithm?

Theoretical answer:

  • The problem your are trying to solve is the Boolean Satisfiability Problem also known as SAT.

  • It is NP-complete.

  • THAT MEANS, that there are no known algorithms1 that always find a solution for a SAT problem in polynomial time; i.e. no algorithm that whose worst case is O(N^C) or better, where C is a constant and N is the number of variables in the SAT problem.

  • There is an obvious solution that is O(2^N) ... brute-force search of the solution space. Better algorithms exist; see the Wikipedia article but they are all exponential in the worst-case.

Practical solutions:

  • For really small N, brute force may give acceptable performance.

  • Use an existing SAT solver, bearing in mind that the theory says that it has exponential behavior in the worst case.

  • Avoid problems with large N ... or code your application so that the solver is "time boxed"; i.e. it gives up if it can't get a solution in a prescribed time.

1 - If it is ever proven that P == NP, then better algorithms may emerge for this and other NP-complete problems.

Upvotes: 5

Related Questions