6
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • $\begingroup$ Have you tried anything? Efficient in what sense? $\endgroup$
    – Juho
    Sep 27, 2013 at 13:59
  • $\begingroup$ @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$. $\endgroup$
    – Simd
    Sep 27, 2013 at 14:02
  • $\begingroup$ The sizes I gave are before the conversion into 3-sat of course which will presumably expand things again. $\endgroup$
    – Simd
    Sep 27, 2013 at 14:11
  • $\begingroup$ A closely related question has been posted on CSTheory. $\endgroup$
    – D.W. ♦
    Oct 2, 2013 at 2:15

2 Answers 2

Reset to default
8
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Simd
    Sep 29, 2013 at 14:42
4
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • $\begingroup$ Would you mind expanding this answer a bit please? $\endgroup$
    – Simd
    Sep 27, 2013 at 18:03
  • 2
    $\begingroup$ 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. $\endgroup$
    – Yuval Filmus
    Sep 27, 2013 at 21:16

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.