3
$\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.

$\endgroup$
  • 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 '14 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 '14 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 '14 at 16:28
  • 1
    $\begingroup$ This answer is also relevant. $\endgroup$ – Mangara Mar 20 '17 at 22:52
6
$\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.

$\endgroup$
4
$\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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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