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?