Reduce the following problem to SAT
It looks like you are trying to compute a hypergraph transversal of size $k$. That is, $\{T_1,\dots,T_m\}$ is your hypergraph, and $S$ is your transversal. A standard translation is to express the clauses as you have, and then translate the length restriction into a cardinality constraint.

So use your existing encoding, i.e., $\bigwedge_{1 \le j \le m} \bigvee_{i \in T_j} x_i$ and then add clauses encoding $\sum_{1 \le i \le n} x_i \le k$.

$\sum_{1 \le i \le n} x_i \le k$ is a cardinality constraint. There are various different cardinality constraint translations into SAT.

The simplest but rather large cardinality constraint translation is just $\bigwedge_{X \subseteq \{1,\dots,n\}, |X| = k+1} \bigvee_{i \in X} \neg x_i$. In this way each disjunction represents the constraint $\neg \bigwedge_{i \in X} x_i$ - for all subsets $X$ of $\{1,\dots,n\}$ of size k+1. That is, we ensure that there is no way that more than k variables can be set. Note that this is not polynomial size in $k$

Some links to papers on more space-efficient cardinality constraint translations which are polynomial size in $k$:


Translating Pseudo-Boolean Constraints into SAT - Niklas Eén and Niklas Sörensson, JSAT vol 2 (2006), pg 1-26 (a good survey).
Efficient CNF encoding of Boolean cardinality constraints - Olivier Bailleux and Yacine Boufkhad, Proceedings of Principles and Practice of Constraint Programming 2003, LNCS vol 2833, pg 108-122 (a nice, fairly easy to implement translation).
Towards an Optimal CNF Encoding of Boolean Cardinality Constraints - Carsten Sinz - Proceedings of Principles and Practice of Constraint Programming 2005, LNCS 3709, pg 827-831.
Towards Robust CNF Encodings of Cardinality Constraints - Joao Marques-Silva and Inês Lynce, Proceedings of Principles and Practice of Constraint Programming 2007, LNCS 4741, pg 483-497.


If you are actually interested in solving such problems, perhaps it is better to formulate them as pseudo-boolean problems (see wiki article on pseudo-boolean problems) and use pseudo-boolean solvers (see pseudo-boolean competition). That way the cardinality constraints are just pseudo-boolean constraints and are part of the language - hopefully the pseudo-boolean solver then handles them directly and therefore more efficiently.