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
andB
- You need to test if
A
impliesB
, or equivalently¬A | B
for all assignments of variables upon whichA
andB
depend. In other words, you need a proof thatF = ¬A | B
is a tautology. - Suppose that the tautology test can be performed in polynomial time
- Consider
¬F
, the inverse ofF
.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 thatP=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".