CNF Encoding Patterns (At Least, At Most, Exactly)
Context: FIT2014_MOC · turning a counting condition into CNF mechanically · the reusable half of Encoding Problems in Propositional Logic Problem it solves: given options, write CNF for “pick at least / at most / exactly of them”.
Quick Revision
- 🎯 Trigger: any phrase reducible to “at least / at most / exactly from options” ➔ apply the clause-size formula, then enumerate combinations.
- ⚡ Key Constraint: the formula is on clause size, not clause count — for at least from , every clause has literals, and you write all of them.
📐 The master formula
- At least from ➔ literals per clause ; clauses = all combinations of size , i.e. clauses; literals unnegated.
- Sanity check ➔ at least gives : one clause with everything, . At least gives : singleton clauses .
- Visual trick ➔ write symbols, circle the first , draw a box from the last symbol back until it encloses exactly one circled symbol; the box size is the clause size.
🔧 Worked patterns
At least from ➔ , so all pairs:
At least from ➔ , so all triples:
At most from ➔ equivalent to “do not pick at least ” ⟹ use the same formula on the negated literals with : At most from ➔ , all clauses of negated literals:
Exactly from ➔ simply conjoin the two:
🔀 Common special cases
| Condition | CNF shape | Note |
|---|---|---|
| at least one of | one clause | already CNF |
| at most one of | pairwise for all | clauses |
| exactly one of | the workhorse | |
| rewrite implication | ||
| two clauses |
✍️ Practice
Practice 1: A mouse is on the clock, the floor, or the bread, and can be in only one place at once. Write this in CNF.
Reference solution exactly one of three options" with :
This is ”
- Key move: exactly one at least one (single clause) at most one (all pairwise negated pairs).
Practice 2: Write "at least two of " in CNF, and state the clause count before writing it.
Reference solution literals per clause; clauses:
- Key move: compute first, then mechanically enumerate every size- subset in alphabetical order so none is missed.
⚠️ Common Mistakes
- 💡 The formula sizes the clause, not the count ➔ is literals per clause; the number of clauses is then . Swapping these is the standard error.
- 💡 “At most” needs negated literals ➔ it is at least of the complements; forgetting to negate produces a formula asserting the opposite.
- 💡 A single big negated clause is wrong for “at most one” ➔ only forbids all three; “no more than one” needs pairwise clauses.
- 💡 Enumerate systematically ➔ write clauses in alphabetical order (new leading variable ⟹ new line) so no combination is skipped under time pressure.
🧠 Active Recall
For "at least of ", why does each clause have literals?
Answer
- Short answer: a clause of size says “not all of these are false”. If we omitted options, remain; forcing at least one of every such subset to be true makes it impossible to leave or fewer chosen.
- Why: Blocking the shortfall ➔ suppose only were picked; then some size- subset would be entirely unpicked, violating its clause. Requiring all such clauses therefore forces at least picks.