Here are systematic ways to express constraints like "pick at least k" or "pick at most k" in CNF. Let your set of choices be $S = \{x_1, x_2, \dots, x_n\}$.

1. Pick at least $k$ from a set of $n$ options

To ensure at least $k$ items are chosen, you must prevent the case where you pick too few. This means that out of any group of $n-k+1$ items, at least one must be chosen.

• Clause Size: Each clause will have $n-k+1$ literals.
• Number of Clauses: $\binom{n}{n-k+1}$
• Example: Pick at least 2 from $\{a, b, c\}$. ($n=3, k=2$)
  • Out of any group of $n-k+1 = 3-2+1 = 2$ items, at least one must be chosen.
  • The clauses are: $(a \lor b) \land (a \lor c) \land (b \lor c)$.

2. Pick at most $k$ from a set of $n$ options

To ensure at most $k$ items are chosen, you must prevent the case where you pick too many. This is equivalent to saying you cannot pick at least $k+1$ items. This means that out of any group of $k+1$ items, at least one must not be chosen (i.e., must be false).

• Clause Size: Each clause will have $k+1$ negated literals.
• Number of Clauses: $\binom{n}{k+1}$
• Example: Pick at most 2 from $\{a, b, c, d\}$. ($n=4, k=2$)
  • Out of any group of $k+1 = 3$ items, at least one must be false.
  • The clauses are: $(\neg a \lor \neg b \lor \neg c) \land (\neg a \lor \neg b \lor \neg d) \land (\neg a \lor \neg c \lor \neg d) \land (\neg b \lor \neg c \lor \neg d)$.

3. Pick exactly $k$ from a set of $n$ options

To get exactly $k$, you simply combine the previous two constraints with an AND: (Pick at least $k$) $\land$ (Pick at most $k$)

Enhancement

if you want to pick at least k items from a set of size n:

• write down n symbols
• draw a circle around the first k
• draw a box that starts from the last symbol, and excloses exactly one circled symbol
• the size of your box gives the size of each of your clauses

Changelog

8/8/25, 4:17 AM

View All Changelog

• 2aa48-web-deploy(Auto): Update base URL for web-pages branchon 8/8/25

Copyright

Copyright Ownership:WARREN Y.F. LONG

License under:Attribution-NonCommercial-NoDerivatives 4.0 International (CC-BY-NC-ND-4.0)