Tool to compare if two logical expressions are same!

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 1

Based on m previous comment, here is an example of a Python implementation to check in a brute-force manner that two conditions are equivalent. I just basically test all possible combinations for the logical values of the inputs. This results in $n 2^n$ operations. For example, it takes ~3s on my computer for $n=23$. It is of course much quicker for lower values of $n$, which might be the most frequently occuring situation.

import numpy as np

def exp1(x):
    return  (x[0,:] & (x[1,:] | x[8,:] | x[9,:]) &  \
                      (x[2,:] | x[3,:] | x[4,:]) &    \
                      (x[5,:] | x[6,:]) & x[7,:]) |   \
            (x[0,:] & (x[1,:] | x[8,:] | x[9,:]) &  \
                      (x[10,:] | x[11,:]) & x[7,:])
               
def exp2(x):
    return x[0,:] & (x[1,:] | x[8,:] | x[9,:]) &  x[7,:] & \
                     (((x[2,:] | x[3,:] | x[4,:]) &    \
                     (x[5,:] | x[6,:])) | x[10,:] | x[11,:])

# for other logical operations in Python:
#  https://numpy.org/doc/stable/reference/arrays.ndarray.html#arithmetic-matrix-multiplication-and-comparison-operations

def compareBoolConditions(exp1,exp2,n):
    ## 1 - generate all possible combinations
    # from itertools import product
    # comb = np.array(tuple(product(np.array([True, False]), repeat=n))).T
    ## 1 - 2nd solution
    comb = np.array(np.meshgrid( *[[True, False] for i in range(n)] ) , order='F').T.reshape(-1,n)
    ## 1 - 3rd solution
    # see https://stackoverflow.com/questions/1208118/using-numpy-to-build-an-array-of-all-combinations-of-two-arrays
    ## 2 - vectorized check
    if np.all( exp1(comb) == exp2(comb) ):
        print('equivalent conditions')
    else:
        print('conditions are not equivalent')

compareBoolConditions(exp1, exp2, 12)

I've found multiple solutions to generate the combinations, so depending on the size of your problem you may want to test and choose the faster one.

Answer 2

Here is not exactly a tool but a convenient way to compare logical expressions graphically. Use electric circuits to represent your Boolean expressions: each resistor can be open gate (F) or closed gate (T), resistors in parallel means OR, and resistors in series means AND. Then, inspecting the two circuits (top and bottom in the picture) corresponding to the two given logical expressions one can recognize that they are equivalent.

Answer 3

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