Accepted answer

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".

Related Articles