satisfiability – Reduction of K-Vertex-Cover to SAT: How to define the constraint?

Overall, one would naturally think that with n different nodes, and for x(1) for example representing node 1, it would be like:

x(1)+x(2)+x(3)…+x(n) <= k

This would mean that for every possible solution of k-vertex-cover, the maximum amount of literals being true has to be lower or equal to k.
So much for understanding.

The problem however is, that a logic formula is needed for description of the constraint and logic doesn’t have addition or comparison.

My only idea up to now is that I could use the logic formula of Adders and Comparators to simulate an addition and a comparison in logic, but that only works out for some solutions. I need a general logic formula.
Does anyone have another idea or maybe a simpler method which could be used in general?

The reduction has to be done in polynomial time.