Reduce Set problem to SAT

Question

So the problem is, given some set $M = \{x_1,x_2,\ldots,x_n\}$ and a set of subsets $S = \{S_1, S_2, \ldots, S_m\}$ where $S_i \subseteq M$. We want to find some set $X \subseteq M$ such that $|X| \le k$ and $X \cap S_i \neq \emptyset$ for all $S_i \in S$.

My solution, I would take some set $M = \{x_1,x_2,x_3,x_4\}$ and suppose $S_1 = \{x_1,x_2\}$, $S_2 = \{x_2,x_3\}$, $S_3 = \{x_4\}$. I would then transform this to a SAT instance to get:

$\phi = (x_1 \vee x_2) \wedge (x_2 \vee x_3) \wedge (x_4)$

Clearly if $\phi$ is satisfiable then there exists some $X \subseteq M$ however this does not guarantee that $|X| \le k$.

So my question is, how can I reduce this problem further so that $|X| \le k$ in polynomial time?

EDIT

I realized there may be an easier way to reduce this to the set-cover problem but need confirmation that my idea is correct.

Will post a new question containing this.

Answer 1

The final constraint you need to encode is that $k$ or fewer variables in the set ${x_1, x_2, ..., x_n}$ is set true. There is a good reference question that outlines several methods for encoding a 1-out-of-$n$ constraint. Those methods can be extended to fit your constraint. Using a chain of adder circuits plus a comparison circuit seems the most straightforward method to me.