A Boolean cardinality constraint $$\sum_{j=0}^{n-1}x_j=k,$$ where $x_j$’s are Boolean variables, and $k$ is a non-negative integer.

How to express the Boolean cardinality constraint to CNF formulas?

  • $\begingroup$ Any idea of $n$ and $k$ ? For some values ($k=0$, $k=n$) that's a single line. In general, one option is to build a tree of adders. $\endgroup$
    – fgrieu
    Sep 16, 2023 at 14:01
  • $\begingroup$ carstensinz.de/papers/CP-2005.pdf $\endgroup$
    – kelalaka
    Sep 16, 2023 at 19:01


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.