CODEWITHSUNDEEP
python
MaxB
MaxB

Reputation: 458

Comparing large boolean expressions for equivalence

I am trying to simplify and compare very large boolean expressions for equivalence. I've traditionally used simplify_logic from sympy to simplify an expression and then compare the two strings for equivalence. This only works well if the expressions contain 8 or less elements. If I am trying to compare two expressions that have 15+ elements each it just hangs (because the time it takes increases exponentially). Are there any Python packages or other roundabout ways to try and accomplish this?

Update with random example

Exp1 = 'A|B&(C|D|E)&F|H|I|J|(K&L&M)|K'

Exp2 = 'A&B&C&(D|E|F|J|K|L)&M&K&O&P'

Exp1 == Exp2 ----> False

These are obviously not the same, but an example of some runaway expressions that I might encounter. For sanitys sake each element is only 1 letter long when my ACTUAL case each expression is a mix of 10 numbers/letters each.

Upvotes: 1

Views: 368

Answers (1)

kaya3
kaya3

Reputation: 51102

Testing equivalence of Boolean expressions is as computationally complex as solving the Boolean satisfiability problem.

To reduce in one direction, a formula is satisfiable if and only if it is not equivalent to the formula False. In the other direction, two formulae A and B are equivalent if and only if (A and not B) or (not A and B) is not satisfiable.

This problem is NP-complete, so there is no known solution that works efficiently for large formulae in the worst case. However, "large" is relative; says Wikipedia:

Since the SAT problem is NP-complete, only algorithms with exponential worst-case complexity are known for it. In spite of this, efficient and scalable algorithms for SAT were developed during the 2000s and have contributed to dramatic advances in our ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints (i.e. clauses).

So your problem, with only dozens of clauses and hundreds of variables, should be quite feasible. Wikipedia suggests some algorithms:

There are two classes of high-performance algorithms for solving instances of SAT in practice: the conflict-driven clause learning algorithm, which can be viewed as a modern variant of the DPLL algorithm (well known implementations include Chaff and GRASP) and stochastic local search algorithms, such as WalkSAT.

Upvotes: 4

Related Questions