Pattern recognition:
- Boolean variables: each topping is either included or not
- Constraints: "at least one of these two" = disjunction
- Two preferences per person = exactly 2 literals per clause
This is textbook 2-SAT.
Translation:
- "I want x" = literal x
- "I don't want x" = literal ¬x
- "At least one of a or b" = clause (a∨b)
Build the implication graph and check satisfiability.