4
$\begingroup$

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.

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ 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. $\endgroup$
    – Kyle Jones
    Jun 3, 2014 at 15:53
  • $\begingroup$ 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. $\endgroup$
    – rnegrinho
    Jun 3, 2014 at 16:13
  • 1
    $\begingroup$ 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. $\endgroup$
    – Kyle Jones
    Jun 3, 2014 at 16:28
  • 2
    $\begingroup$ This answer is also relevant. $\endgroup$
    – Mangara
    Mar 20, 2017 at 22:52

2 Answers 2

Reset to default
7
$\begingroup$

There are many ways. See Encoding 1-out-of-n constraint for SAT solvers 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.

Improve this answer
$\endgroup$
6
$\begingroup$

The paper SAT Encodings of the At-Most- k Constraint, 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.

Improve this answer
$\endgroup$

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.