# Reducing Dominant Set Problem to SAT

I am trying to solve a problem and I am really struggling, I would appreciate any help.

Given a graph $$G$$ and an integer $$k$$ , recognize whether $$G$$ contains dominating set $$X$$ with no more than $$k$$ vertices. And that is by finding a propositional formula $$\phi_{G,k}$$ that is only satisfiable if and only if there exists a dominating set with no more than k vertices, so basically reducing it to SAT-Problem.

What I have so far is this boolean formula:

$$\phi=\bigwedge\limits_{i\in V} \bigvee\limits_{j\in V:(i,j)\in E} x_i \vee x_j$$

So basically defining a variable $$x_i$$ that is set to true when when vertix $$v_i$$ is in the dominating Set $$X$$, so all the formula says that it is satisfiable when for each node in $$G$$ it is true that either the vertex itself is in $$X$$ or one of the adjacent vertices is. Which is basically a Weighted Satisfiability Problem so its satisfiable with at most $$k$$ variables set to true.

My issue is now that I couldn’t come up with a boolean formula $$\phi_{G,k}$$ that not only uses Graph $$G$$ as input but also integer $$k$$. So my question is now how can I modify this formula so it features $$k$$ , or possibly come up with a new one if it cannot be modified?