Reduce Set problem to SAT
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.