Lesson 294
2-SAT
Implication Graph + SCC
1:00How to decide 2-CNF satisfiability in linear time using an implication graph and strongly connected components.
By the end, you can
- Explain what a 2-CNF formula is and state its goal.
- Convert any two-literal clause into its equivalent pair of implications.
- Build the implication graph for a given 2-SAT instance.
- State the satisfiability theorem in terms of SCCs and explain why sharing an SCC is a contradiction.
- Apply the assignment-recovery rule (literal in the topologically later SCC is true).
- Identify the UNSAT condition by inspecting SCC membership for each variable.
- Compare 2-SAT (polynomial) with 3-SAT (NP-complete) and explain why adding one more literal per clause makes the problem hard.
Up next in String Algorithms, Advanced DP & Competitive Techniques
