CNF Construction
About 393 wordsAbout 1 min
2025-07-29
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={x1,x2,…,xn}.
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: (n−k+1n)
- 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∨b)∧(a∨c)∧(b∨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: (k+1n)
- 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: (¬a∨¬b∨¬c)∧(¬a∨¬b∨¬d)∧(¬a∨¬c∨¬d)∧(¬b∨¬c∨¬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) ∧ (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
2b7ff
-web-deploy(Auto): Update base URL for web-pages branchon
Copyright
Copyright Ownership:WARREN Y.F. LONG
License under:Attribution-NonCommercial-NoDerivatives 4.0 International (CC-BY-NC-ND-4.0)