Lower bounds for formulae sizes for addition 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.
Counting the number of 1s in a given binary string is $\mathsf{TC^0}$-complete and cannot be decided using any polynomial-size CNF. In fact you need exponentially large CNFs to decide them. So if you want $y$ to be part of the input then the size is going to be exponential in $n$.

If $y$ is fixed, then there are CNF's with $O({n \choose y})$ gates: check if any $y$bits of $x$ are 1: 
$$\exists I \in {n \choose y} \ \forall j \in I. \ x_{j} \land \forall j\notin I. \ \lnot x_j $$

For $y = \frac{n}{2}$ this gives an exponential-size CNF. I haven't checked it but I think the proof for parity not in $\mathsf{AC^0}$ can be adopted to prove an exponential size lower-bound for this function.



As I wrote before, in case we are interested in satisfiability and a reduction to 3CNF-SAT then the size is constant as we can decide in polynomial-time if the equality holds or not and depending on the answer return $\top$ or $\bot$.



Another question is to look for a CNF $\varphi(\vec{x}, \vec{y}, \vec{w})$ such that for all $\vec{a}$ and $\vec{b}$, $\Sigma_{1 \leq i \leq n} a_i = b$ holds iff $\varphi(\vec{a}, \vec{b}, \vec{w})$ is satisfiable, i.e. $\exists \vec{w} \ \varphi(\vec{a}, \vec{b}, \vec{w})$ holds. The lower-bound does not apply to such formula, in fact for any langauge $L \in \mathsf{NP}$ there is a polynomial-size CNF $\varphi(\vec{x},\vec{w})$ s.t.

$$ x \in L \Leftrightarrow \exists \vec{w} \ \varphi(\vec{x},\vec{w}).$$

I don't know what is the best known CNF size for 
$\Sigma_{1 \leq i \leq n} x_i = y$ in this sense.
I don't think there is any good lower-bound for the following reason:
the reduction from circuit-SAT to 3CNF-SAT is very efficient: linear number of new variables, linear increase in size.
Any lower-bound would also give a similar lower-bound on the circuit size for deciding the equation and in general we don't have good circuit size lower-bounds.

An obvious upper-bound can be obtained from the same idea: the equation can be decided using two Threshold and one And, so this has a constant size $\mathsf{TC^0}$ circuit. The upper-bound follows from reducing evaluation of a $\mathsf{TC^0}$ circuit to 3CNF-SAT.