An answer to this question on the Scientific Computing Stack Exchange.

Question

We have challenge in my current assignment where we need to modify/minimize an existing logical expression to another new logical expression. But the result should be the same.

For eg: the ask to convert

(1 AND (2 OR 9 OR 10) AND (3 OR 4 OR 5) AND (6 OR 7) AND 8) OR (1 AND (2 OR 9 OR 10) AND (11 OR 12) AND 8)

into

1 AND (2 OR 9 OR 10) AND 8 AND (((3 OR 4 OR 5) AND (6 OR 7)) OR 11 OR 12)

and see if both of them evaluate to same, across a various combinations of ( T or F) for each number.

I need to the same activity for almost 100+ expressions. hence i am looking for a tool to help expedite.

Answer

If I recall correctly, every formula has a unique canonical conjunctive normal form and for each possible truth table you could make from some set of variables there is a corresponding canonical CNF. It follows then, that if two expressions have the same CNF they are equivalent.

Therefore, if you can find a way of expressing your formula as a CNF (this is a fairly simple algorithm) and then a way of ordering the terms of the output appropriately, you can do a string equivalence check. This will solve many cases efficiently, though there are logical expressions whose CNF representation is exponentially larger than the input, so it's not a panacea.

A Python example:

import re
from sympy.logic.boolalg import to_cnf
#Your inputs
str1 = "(1 AND (2 OR 9 OR 10) AND (3 OR 4 OR 5) AND (6 OR 7) AND 8) OR (1 AND (2 OR 9 OR 10) AND (11 OR 12) AND 8)"
str2 = "1 AND (2 OR 9 OR 10) AND 8 AND (((3 OR 4 OR 5) AND (6 OR 7)) OR 11 OR 12)"
#Convert numbers to something we can use as a variable
str1 = re.sub(r"\b([0-9]+)\b", r"x\1", str1)
str2 = re.sub(r"\b([0-9]+)\b", r"x\1", str2)
#Convert logic to something SymPy will recognize
str1 = str1.replace("AND", "&").replace("OR", "|")
str2 = str2.replace("AND", "&").replace("OR", "|")
#Check equivalence
print("Equivalent?", str(to_cnf(str1))==str(to_cnf(str2)))