score:2

I am concerned that this is overly complicated. Is there a better way?

The short answer is "No, there isn't" 1

The long answer: The "overly complicated" captures the essence of the problem: it is NP-hard. Here is a short informal proof relying upon the fact that the satisfiability problem is NP-complete:

• Suppose that you have two Boolean formulas, `A` and `B`
• You need to test if `A` implies `B`, or equivalently `¬A | B` for all assignments of variables upon which `A` and `B` depend. In other words, you need a proof that `F = ¬A | B` is a tautology.
• Suppose that the tautology test can be performed in polynomial time
• Consider `¬F`, the inverse of `F`. `F` is satisfiable if and only if `¬F` is not a tautology
• Use the hypothetical polynomial algorithm to test `¬F` for being a tautology
• The answer to "is `F` satisfiable" is the inverse of the answer to "is `¬F` a tautology"
• Therefore, an existence of a polynomial tautology checker would imply that the satisfiability problem is in `P`, and that `P=NP`.

Of course the fact that the problem is NP-hard does not mean that there would be no solutions for practical cases: in fact, your approach with the conversion to a canonical form may produce OK results in many real-world situations. However, an absence of a known "good" algorithm often discourages active development of practical solutions2.

1 With the obligatory "unless `P=NP`" disclaimer.

2 Unless a "reasonably good" solution would do, which may very well be the case for your problem, if you allow for "false negatives".