<p>The paper <a href="https://www.it.uu.se/research/group/astra/ModRef10/papers/Alan%20M.%20Frisch%20and%20Paul%20A.%20Giannoros.%20SAT%20Encodings%20of%20the%20At-Most-k%20Constraint%20-%20ModRef%202010.pdf" rel="noreferrer">SAT Encodings of the At-Most-
k
Constraint</a>, by Alan M. Frisch and Paul A. Giannaros compares five different encodings of the at-most-k constraint, both theoretically and by running experiments.</p>

<p>Their conclusion is that the naive binomial encoding is almost always sub-optimal, while the four more advanced encodings they consider each perform better in some cases and worse in others, with the sequential counter encoding mentioned in the comments generally adding the fewest clauses.</p>

CC BY-SA 3.0
2017-03-20T22:49:29.753Z
2017-03-20T22:49:29.753Z
Mangara
<p>There are many ways.  See <a href="https://cs.stackexchange.com/q/13188/755">Encoding 1-out-of-n constraint for SAT solvers</a> for a compendium of several ways and for a useful reference with more information.</p>

<p>From a practical perspective, the different schemes have different tradeoffs.  If you are trying to encode a $k$-out-of-$N$ constraint in something you are feeding to a SAT solver, you can try each of the different candidate encodings to see which makes the SAT solver run faster; they can have a significant impact on the efficiency of the SAT solver.</p>

CC BY-SA 3.0
2014-06-04T01:18:48.063Z
2014-06-04T01:18:48.063Z
2017-04-13T12:48:30.830Z
D.W.
<p>Is there a way to express the condition that exactly $k$ of $N$ boolean variables are active without writing a disjunction of $N$-choose-$k$ terms, i.e., all possible configurations of the $N$ variables where exactly $k$ are active? Is the same true for specifying that at least $K$ of the $N$ boolean variables are active?</p>

<p>I'm aware that this is a problem dealt with in theoretical computer science but I couldn't find any references. </p>

CC BY-SA 3.0
2014-06-03T15:53:01.873Z
Essentially you're looking at $N$ bits and trying to decide if they add up to $k$, so you only need a series of adder circuits that add up the bits plus a comparison circuit to check whether the final sum equals $k$.  Converting the circuits to CNF by the usual means produces $O(N)$ clauses.
Kyle Jones
CC BY-SA 3.0
2014-06-03T16:13:57.400Z
Thank you. I think I can take it from there. What about the more that $k$ active case? You could implement a disjunction of comparisons, but there should be a more succinct solution.
rnegrinho
CC BY-SA 3.0
2014-06-03T16:28:40.980Z
Same situation except the comparison circuit checks for greater than rather than equivalence.  Start with the MSB end of the two numbers to be compared and move right until you find bits that aren't equal.  The number with the 1 bit is obviously greater than the number with the 0 bit.
Kyle Jones
CC BY-SA 3.0
2017-03-20T22:52:23.243Z
[This answer](http://cs.stackexchange.com/a/6522/13065) is also relevant.
Mangara
<reference-request><sat>
SAT formula specifying that exactly $k$ of $N$ boolean variables are active using less than $N$-choose-$k$ terms
rnegrinho
# SAT formula specifying that exactly $k$ of $N$ boolean variables are active using less than $N$-choose-$k$ terms

(Asked by: username_0 on 2014-06-03)

Is there a way to express the condition that exactly $k$ of $N$ boolean variables are active without writing a disjunction of $N$-choose-$k$ terms, i.e., all possible configurations of the $N$ variables where exactly $k$ are active? Is the same true for specifying that at least $K$ of the $N$ boolean variables are active?

I'm aware that this is a problem dealt with in theoretical computer science but I couldn't find any references.

**Tags:** reference-request, sat

> **Comments:**
> **username_1**: Essentially you're looking at $N$ bits and trying to decide if they add up to $k$, so you only need a series of adder circuits that add up the bits plus a comparison circuit to check whether the final sum equals $k$.  Converting the circuits to CNF by the usual means produces $O(N)$ clauses.  
> **username_0**: Thank you. I think I can take it from there. What about the more that $k$ active case? You could implement a disjunction of comparisons, but there should be a more succinct solution.  
> **username_1**: Same situation except the comparison circuit checks for greater than rather than equivalence.  Start with the MSB end of the two numbers to be compared and move right until you find bits that aren't equal.  The number with the 1 bit is obviously greater than the number with the 0 bit.  
> **username_2**: [This answer](http://cs.stackexchange.com/a/6522/13065) is also relevant.  

---

## 2 answers

### Answer by username_3 on 2014-06-04. Score: 7 | Accepted answer

There are many ways. See [Encoding 1-out-of-n constraint for SAT solvers](https://cs.stackexchange.com/q/13188/755) for a compendium of several ways and for a useful reference with more information.

From a practical perspective, the different schemes have different tradeoffs. If you are trying to encode a $k$-out-of-$N$ constraint in something you are feeding to a SAT solver, you can try each of the different candidate encodings to see which makes the SAT solver run faster; they can have a significant impact on the efficiency of the SAT solver.


---

### Answer by username_2 on 2017-03-20. Score: 7

The paper [SAT Encodings of the At-Most-
k
Constraint](https://www.it.uu.se/research/group/astra/ModRef10/papers/Alan%20M.%20Frisch%20and%20Paul%20A.%20Giannoros.%20SAT%20Encodings%20of%20the%20At-Most-k%20Constraint%20-%20ModRef%202010.pdf), by Alan M. Frisch and Paul A. Giannaros compares five different encodings of the at-most-k constraint, both theoretically and by running experiments.

Their conclusion is that the naive binomial encoding is almost always sub-optimal, while the four more advanced encodings they consider each perform better in some cases and worse in others, with the sequential counter encoding mentioned in the comments generally adding the fewest clauses.


---

