5
$\begingroup$

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.

Improve this question
$\endgroup$
8
  • $\begingroup$ 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? $\endgroup$
    – Kaveh
    Sep 29, 2013 at 20:04
  • $\begingroup$ The equation is satisfiable iff $n<y$. The formula I mentioned is equisatisfiable with the equation. You probably mean equivalent? $\endgroup$
    – Kaveh
    Sep 29, 2013 at 20:19
  • $\begingroup$ "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. $\endgroup$
    – Kaveh
    Sep 29, 2013 at 20:20
  • $\begingroup$ @Kaveh Ah.. I misunderstood "whenever" to refer to values of the variables. Thanks. Fixed. $\endgroup$
    – Simd
    Sep 29, 2013 at 20:22
  • 1
    $\begingroup$ A related question has been posted on CS.SE, though the answers there don't answer this question. $\endgroup$
    – D.W.
    Oct 2, 2013 at 2:17

1 Answer 1

Reset to default
2
$\begingroup$

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.

Improve this answer
$\endgroup$
9
  • $\begingroup$ Thank you. Could you explain why your lower bound is exponential but the linked answers seem to claim polynomial size solutions in $y$ please? $\endgroup$
    – Simd
    Sep 30, 2013 at 13:43
  • $\begingroup$ @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. $\endgroup$
    – Kaveh
    Sep 30, 2013 at 16:53
  • $\begingroup$ 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"? $\endgroup$
    – Simd
    Sep 30, 2013 at 17:21
  • 1
    $\begingroup$ @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})$. $\endgroup$
    – Kaveh
    Sep 30, 2013 at 19:24
  • 1
    $\begingroup$ @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. $\endgroup$
    – Mikolas
    Oct 6, 2013 at 14:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.