<p>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$.</p>

<p>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 $$</p>

<p>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.</p>

<hr>

<p>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$.</p>

<hr>

<p>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.</p>

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

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2013-09-30T13:43:58.237Z
Thank you. Could you explain why your lower bound is exponential but the linked answers seem to claim  polynomial size solutions in $y$ please?
Simd
CC BY-SA 3.0
2013-09-30T16:53:11.187Z
@Lembik, well, the linked answer states that the formula is **not** polynomial size. There are simply no polynomial size CNFs for majority function and we have a well-known exponential CNF size lower-bound for majority. ps: keep in mind that the linked question is about reductions to satisfiability and as I wrote if we only care about equisatisfiability then we have CNFs of size 1.
Kaveh
CC BY-SA 3.0
2013-09-30T17:21:10.213Z
Just to finish this line off.. what do they refer to when they say "Some links to papers on more space-efficient cardinality constraint translations which are polynomial size in k"?
Simd
CC BY-SA 3.0
2013-09-30T17:29:42.810Z
Thanks. I am definitely not interested in this version of the problem where you are converting a sum with all the $x_i$ variables already set to $1$ or $0$ to 3-cnf. The variables $x_i$ should appear in the 3-cnf translation uninstantiated and this 3-cnf formula should be true exactly when any $y$ of them is set to True and the rest are set to False. I am sorry if this hasn't been clear.
Simd
CC BY-SA 3.0
2013-09-30T19:24:18.833Z
@Lembik, I haven't read the papers. You should ask the author. My guess would be: they come up with some polynomial size CNF which is satisfiable iff the original equation holds. One way to do is to add additional variables like in the reduction of SAT to 3CNF-SAT. In other words, there is a polynomial size CNF $\varphi(\vec{x}, \vec{y}, \vec{w})$ such that the equation holds for given $\vec{x}$ and $\vec{y}$ iff $\exists \vec{w} \ \varphi(\vec{x}, \vec{y}, \vec{w})$.
Kaveh
CC BY-SA 3.0
2013-10-02T04:24:59.820Z
@Kaveh, sorry to hear that you felt this was an unfair comment: it wasn't my intent to make you feel besieged or unappreciated.  I was trying to seek greater clarity.  As you say, the author of the question is unclear on this.  I have proposed an edit to try to make this clearer in your answer, in hopes that this will be more constructive than commenting; feel free to see if you think it is an improvement or not.  Also, after you review it, can I persuade you to take a second look at the last sentence of your answer and edit it?  I'm having trouble understanding what it is saying.
D.W.
CC BY-SA 3.0
2013-10-02T05:16:08.087Z
@D.W., I removed that sentence. I thought that the OP might be some one who is using SAT-solvers and is trying to optimize the size for that purpose. I was pointing out that, as far as I know, optimizing the size does not give CNFs which are easier to solve.
Kaveh
CC BY-SA 3.0
2013-10-02T08:12:06.047Z
@Kaveh  Thank you for the edited answer which is addressing the question I meant to ask. You are exactly right I am trying to use SAT-solvers and as a result became interested in what theory was known about this problem, and in particular lower bounds.
Simd
CC BY-SA 3.0
2013-10-06T14:25:44.360Z
@Kaveh would like to confirm that in SAT additional variables are being used. then the problem can be included in linear size. also, these encodings ensure arc consistency.
Mikolas
CC BY-SA 3.0
2013-09-30T04:06:38.670Z
2013-10-02T05:10:15.307Z
2013-10-02T05:10:15.307Z
Kaveh
<p>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 <a href="https://cs.stackexchange.com/a/6522/755">answer</a>.  What is known about the minimum possible size however? </p>

<p>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$?</p>

<p><strong>EDIT</strong> 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.</p>

CC BY-SA 3.0
2013-09-29T20:04:59.980Z
It is one: $\bot$ if $n<y$ and $\top$ otherwise. In essence because it is polynomial time decidable whether the conditions are satisfiable or not, you can solve the satisfiability problem and output $\bot$ or $\top$ depending on the answer. (This holds even if you restrict the reduction to $\mathsf{AC^0}$ as comparison between binary numbers is decidable in $\mathsf{AC^0}$). Does this answer your question or are you looking for something else?
Kaveh
CC BY-SA 3.0
2013-09-29T20:19:00.827Z
The equation is satisfiable iff $n<y$. The formula I mentioned is equisatisfiable with the equation. You probably mean equivalent?
Kaveh
CC BY-SA 3.0
2013-09-29T20:20:54.287Z
"two formulae are equisatisfiable if the first formula is satisfiable whenever the second is and vice versa", so you mean equivalent not equisatisfiable. ps: I removed 3-SAT since it is not needed and is probably confusing for readers.
Kaveh
CC BY-SA 3.0
2013-09-29T20:22:17.903Z
@Kaveh Ah.. I misunderstood "whenever" to refer to values of the variables. Thanks. Fixed.
Simd
CC BY-SA 3.0
2013-09-29T20:27:23.110Z
I wonder if this would be interesting to theoreticians since it's polynomial. BTW the solutions listed in the linked answer are not only trying to be small but also arc-consistent.
Mikolas
CC BY-SA 3.0
2013-09-29T20:53:08.497Z
@Mikolas, it can be, e.g. see [this question](http://cstheory.stackexchange.com/questions/12172).
Kaveh
CC BY-SA 3.0
2013-10-02T02:17:40.287Z
A related question has been [posted on CS.SE](http://cs.stackexchange.com/q/14640/755), though the answers there don't answer this question.
D.W.
CC BY-SA 3.0
2013-10-02T04:22:34.637Z
@D.W., check the [revisions](http://cstheory.stackexchange.com/posts/19194/revisions).
Kaveh
<cc.complexity-theory><lo.logic><lower-bounds><boolean-functions>
Lower bounds for formulae sizes for addition
Simd
# Lower bounds for formulae sizes for addition

(Asked by: username_0 on 2013-09-29)

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](https://cs.stackexchange.com/a/6522/755). 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.

**Tags:** cc.complexity-theory, lo.logic, lower-bounds, boolean-functions
> **Comments:**
> **username_1**: It is one: $\bot$ if $n<y$ and $\top$ otherwise. In essence because it is polynomial time decidable whether the conditions are satisfiable or not, you can solve the satisfiability problem and output $\bot$ or $\top$ depending on the answer. (This holds even if you restrict the reduction to $\mathsf{AC^0}$ as comparison between binary numbers is decidable in $\mathsf{AC^0}$). Does this answer your question or are you looking for something else?  
> **username_1**: The equation is satisfiable iff $n<y$. The formula I mentioned is equisatisfiable with the equation. You probably mean equivalent?  
> **username_1**: "two formulae are equisatisfiable if the first formula is satisfiable whenever the second is and vice versa", so you mean equivalent not equisatisfiable. ps: I removed 3-SAT since it is not needed and is probably confusing for readers.  
> **username_0**: @Kaveh Ah.. I misunderstood "whenever" to refer to values of the variables. Thanks. Fixed.  
> **username_2**: I wonder if this would be interesting to theoreticians since it's polynomial. BTW the solutions listed in the linked answer are not only trying to be small but also arc-consistent.  
> **username_1**: @Mikolas, it can be, e.g. see [this question](http://cstheory.stackexchange.com/questions/12172).  
> **username_3**: A related question has been [posted on CS.SE](http://cs.stackexchange.com/q/14640/755), though the answers there don't answer this question.  
> **username_1**: @D.W., check the [revisions](http://cstheory.stackexchange.com/posts/19194/revisions).  

---

## 1 answers

### Answer by username_1 on 2013-09-30. Score: 2

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.

> **Comments:**
> **username_0**: Thank you. Could you explain why your lower bound is exponential but the linked answers seem to claim  polynomial size solutions in $y$ please?  
> **username_1**: @Lembik, well, the linked answer states that the formula is **not** polynomial size. There are simply no polynomial size CNFs for majority function and we have a well-known exponential CNF size lower-bound for majority. ps: keep in mind that the linked question is about reductions to satisfiability and as I wrote if we only care about equisatisfiability then we have CNFs of size 1.  
> **username_0**: Just to finish this line off.. what do they refer to when they say "Some links to papers on more space-efficient cardinality constraint translations which are polynomial size in k"?  
> **username_0**: Thanks. I am definitely not interested in this version of the problem where you are converting a sum with all the $x_i$ variables already set to $1$ or $0$ to 3-cnf. The variables $x_i$ should appear in the 3-cnf translation uninstantiated and this 3-cnf formula should be true exactly when any $y$ of them is set to True and the rest are set to False. I am sorry if this hasn't been clear.  
> **username_1**: @Lembik, I haven't read the papers. You should ask the author. My guess would be: they come up with some polynomial size CNF which is satisfiable iff the original equation holds. One way to do is to add additional variables like in the reduction of SAT to 3CNF-SAT. In other words, there is a polynomial size CNF $\varphi(\vec{x}, \vec{y}, \vec{w})$ such that the equation holds for given $\vec{x}$ and $\vec{y}$ iff $\exists \vec{w} \ \varphi(\vec{x}, \vec{y}, \vec{w})$.  
> **username_3**: @Kaveh, sorry to hear that you felt this was an unfair comment: it wasn't my intent to make you feel besieged or unappreciated.  I was trying to seek greater clarity.  As you say, the author of the question is unclear on this.  I have proposed an edit to try to make this clearer in your answer, in hopes that this will be more constructive than commenting; feel free to see if you think it is an improvement or not.  Also, after you review it, can I persuade you to take a second look at the last sentence of your answer and edit it?  I'm having trouble understanding what it is saying.  
> **username_1**: @D.W., I removed that sentence. I thought that the OP might be some one who is using SAT-solvers and is trying to optimize the size for that purpose. I was pointing out that, as far as I know, optimizing the size does not give CNFs which are easier to solve.  
> **username_0**: @Kaveh  Thank you for the edited answer which is addressing the question I meant to ask. You are exactly right I am trying to use SAT-solvers and as a result became interested in what theory was known about this problem, and in particular lower bounds.  
> **username_2**: @Kaveh would like to confirm that in SAT additional variables are being used. then the problem can be included in linear size. also, these encodings ensure arc consistency.  

---

