# Convert $\sum x_i = y$ to 3-sat

I have a simple looking question. What is the most efficient conversion of $\sum_{i=1}^n x_i = y$ to 3-sat? Here $x_i$ is either $1$ or $0$ and $y$ is some positive integer.

Can you do better than making a SATISFIABILITY instance with $\binom{n}{y}$ clauses, each of which is the conjunction of $y$ positive literals and $n-y$ negative literals and then just feeding the whole thing into the Tseitin transform?

• Have you tried anything? Efficient in what sense?
– Juho
Commented Sep 27, 2013 at 13:59
• @Juho A naive method would make $\binom{n}{y}$ clauses with $y$ positive literals and $n-y$ negative literals each I was thinking. This is rather large as a function of $n$.
– Simd
Commented Sep 27, 2013 at 14:02
• The sizes I gave are before the conversion into 3-sat of course which will presumably expand things again.
– Simd
Commented Sep 27, 2013 at 14:11
• A closely related question has been posted on CSTheory.
– D.W.
Commented Oct 2, 2013 at 2:15

## 2 Answers

Many better techniques for enforcing cardinality constraints are described in this answer. For the special case $y=1$, see also Encoding 1-out-of-n constraint for SAT solvers. Read those links; they suggest more efficient conversions, though I'm not aware of any reason to expect that they are necessarily optimal, so they don't answer your question about the most efficient conversion.

• Thank you. The " Encoding 1-out-of-n constraint" link looks very useful for that problem. I am still working through the other interesting links but I am not sure they fully answer my question.
– Simd
Commented Sep 29, 2013 at 14:42

Hint: Use a circuit for computing $\sum_{i=1}^n x_i$. Don't forget you're allowed to add variables!

• Would you mind expanding this answer a bit please?
– Simd
Commented Sep 27, 2013 at 18:03
• Well, it's your exercise. You can look up the proof of Cook's theorem (along with the reduction from SAT to 3SAT), which explains how to convert a circuit to a SAT instance. Commented Sep 27, 2013 at 21:16