I think the competing approach to exhaustive (and possibly exhausting) creation of truth tables would be to reduce all your expressions to a canonical form and compare those. For example, rewrite everything into conjunctive normal form with some rule about the ordering of symbols (eg alphabetical order within terms) and terms (eg alphabetical by first symbol in term). This of course, requires that symbol A in one expression is the same as symbol A in another.
How easy it is to write (or grab from the net) a C or C++ function for rewriting your expressions into CNF I don t know. However, there s been a lot of AI work done in C and C++ so you ll probably find something when you Google.
I m also a little unsure about the comparative computational complexity of this approach and the truth-table approach. I strongly suspect that it s the same.
Whether you use truth tables or a canonical representation you can of course keep down the work to be done by splitting your input forms into groups based on the number of different symbols that they contain.
EDIT: On reading the other answers, in particular the suggestion to generate all truth tables and compare them, I think that @Iulian has severely underestimated the number of possible truth tables.
Suppose that we settle on RPN to write the expressions, this will avoid having to deal with brackets, and that there are 10 symbols, which means 9 (binary) operators. There will be 10! different orderings of the symbols, and 2^9 different orderings of the operators. There will therefore be 10! x 2^9 == 1,857,945,600 rows in the truth table for this expression. This does include some duplicates, any expression containing only and and or for instance will be the same regardless of the order of symbols. But I m not sure I can figure this any further ...
Or am I making a big mistake ?