I am looking for a general formula/algorithm for the construction of boolean expression of $n$ variables which is true iff the sum of all variables is equal to $k$.
I don't understand the second part of this post.
Something like this in mathematical notation.
Such an expression is often called cardinality constraint.
An overview paper of Carsten Sinz can be found here.
To construct such an expression (or circuit), you basically need a counter/adder and a binary comparator. The comparator compares the sum against the specified constraint(s) and returns true or false respectively.
The counter can be designed in many different styles. There are serial, parallel or mixed counters. The style is chosen according to the requirements. There is a trade-off between gate level depth and number of gates (= Boolean operations).
