Lesson : Recognize -SAT when you see constraints of the form "at least one of two conditions must hold." that is the OR pattern. Lesson : Model carefully. Map problem entities (toppings, courses, nodes) to boolean variables and constraints (customer wishes, conflicts) to clauses.
Lesson : Trust the algorithm. The SCC-based satisfiability check is complete and correct. If it says unsatisfiable, no solution exists. If it says satisfiable, the constructed assignment works.