I am interested in the conversion of  $\sum_{i=1}^n x_i = y$ to 3-CNF.  Here $x_i$ is a binary 0/1 variable and $y$ is some positive integer. There are a number of practical methods for doing this, some of which are in this answer.  What is known about the minimum possible size however? Define a function $f(n,y)$ as the minimum size of a logical formula which is equivalent to the question: does $\sum_{i=1}^n x_i = y$? What is known about  $f(n,y)$?   Is the exact value of $f(n,y)$ known for small values $n$ and $y$?EDIT Kaveh has formalized my intended question in the final part of his answer. From there we learn that finding any lower bound might be hard. I am still interested to know what the best upper bounds are, especially for small problem sizes.
Lower bounds for formulae sizes for addition
cc.complexity theory;lo.logic;lower bounds;boolean functions