I'm trying to solve a constraint programming problem using a SAT solver. I have set of constraints in the form of propositional logic statements, which are converted to CNF using Tseitin transformation. From the nature of my problem I know that there are redundant constraints. For example, I have a rule: $$AND\:(OR\: (x1,x2),\: OR\: (x3,x4)) \,\,\,\,\,\,(1)$$
and another: $$AND\:(OR\: (x1,x2),\: OR\: (x3,x4), \:OR\:(x5,x6))\,\,\,\,\,\, (2)$$ where $x_i$ are inputs. Both constraints have in common subnodes, for example $OR (x1,x2)$. Due to this I know that there is no point in having both constraints - if the first one becomes FALSE, then the second equals FALSE too. So the second one is redundant. This example is the easiest. One more, closer to what might be found in my formula: $$AND\:(x1,\:x2,\: OR \:(AND \:(x3,x4), \:AND\:(x5,x6)))\,\,\,\,\,\,(3)$$ and the second one: $$AND\:(x3,x4)\,\,\,\,\,\,(4)$$ In this case, I can simplify the first one to the form of: $$AND\:(x1,\:x2,\:AND\:(x5,x6))\,\,\,\,\,\,(5)$$ due to (4).
I prefer to have a lot of small rules (by a lot I mean $10^3$ or $10^4$, which in CNF become $10^5-10^6$ of clauses). The rules are not complicated - 10 ANDs and ORs and 20-30 inputs per rule at most, but they are usually much simpler.
Is there an efficient way to remove such redundancy from a formula? Is it possible with CNF formulation or I should use some other representation of the formula (BDD, for example)? Any help and directions will be useful.