Detection of redundant boolean constraints

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.

The simplification you're describing is called subsumption. It's a standard technique and some SAT solvers (e.g. minisat) will apply it along with other simplification techniques as a preprocessing step before attacking the SAT problem itself. In particular, subsumption and equivalent variable substitution together, applied to the generated CNF formula, are enough to do the common subformula elimination you described in the question. That's because each circuit transformation yields an output variable, and output variables derived from the same circuit can be efficiently identified and reduced to references to a single variable. After that normal subsumption rules applied to clauses will eliminate the common subformulas.

If you're using a solver that doesn't do this preprocessing, then you can do the rough equivalent of it during conversion to CNF. First you'll need to apply duplicate circuit suppression while you're doing the Tseitin tranformation. As you're doing the transformation to CNF, memoize each circuit you've converted. If you encounter the circuit again, skip the circuit conversion and use the same output variable that you used for the memoized circuit. Once you've converted everything to clauses, do normal clause subsumption, i.e. check each clause A against every other longer B clause to see if A's literals are a subset of B's. If so, then A subsumes B and clause B can be discarded from the formula.

StackExchange Computer Science Q#28845, answer score: 3