Two Choices Each — Solution & Editorial

Back to the Problem

2-SAT: build the implication graph (¬a → b and ¬b → a per clause); the formula is satisfiable iff no variable shares an SCC with its own negation.

Complexity: O(N + M)

Watch out: Each clause contributes TWO implications; forgetting the symmetric one silently accepts unsatisfiable formulas.