What is the state of the art in efficient boolean function operations?
The obvious method is to use BDDs.

Given a BDD for two boolean functions $f,g$, you can form a BDD for $f \land g$, $f \lor g$, $\neg f$, $f \implies g$, $f \oplus g$ (xor), and many other binary operations on them.  Also, given BDDs for $f,g$, you can test whether $f$ and $g$ are the same boolean function.

The worst-case behavior is that their size might grow to be exponential in $n$, the number of boolean variables, but empirically, the size often remains manageable in many real-world applications, e.g., when there is suitable structure in the underlying boolean functions.  In the model-checking world, designs with 50-200 boolean variables are routinely handled using BDDs.

It's also possible to manipulate boolean expressions in symbolic form, and then use SAT solvers or SMT solvers to test for equivalence.  This is another plausible alternative.

My advice is: try BDDs first, then if they don't scale well enough for your needs, you can try SAT-based solutions.  If that still doesn't work, come back to ask for more suggestions (providing more details about your specific setting and what you've tried).