Complexity of minimising polynomial formula size
You can reduce the co-NP-Complete TAUTOLOGY problem (given a Boolean formula, is it a tautology?) to the problem of minimizing formula size (since a formula is a tautology iff it's equivalent to TRUE). Moreover, TAUTOLOGY for 3DNFs (analogously to SAT for 3CNFs) is co-NP-Complete.