Reduce Vertex cover to SAT
Let's introduce a variable $x_i$ for every node $i$, representing the condition that the node is part of the vertex cover. Then for every edge $\{v,w\}$ we introduce the clause $x_v \lor x_w$.

We have the additional condition $x_1  + x_2 + \ldots \ +\ x_n \leq k$. We can combine an addition circuit  to compute the bits of the sum with a comparator circuit to enforce the inequality. The CNF of the resulting circuit has only polynomially many clauses.