Sign in to watch this lesson
Advanced - Graphs Ā· 4:37
2-SAT
2-SAT asks for true/false values that satisfy a conjunction of clauses with two literals each. Every clause (a or b) becomes the implications not a => b and not b => a on a graph with a vertex per literal; the formula is unsatisfiable exactly when some variable shares a strongly connected component with its negation. Otherwise, with components in topological order, set x true iff its component comes later than not x's, all in O(n + m).
You will learn
- Turn every two-literal clause into its pair of contrapositive implications on a 2n-vertex graph
- Decide satisfiability by checking whether any x shares a strongly connected component with not x
- Build an assignment from a topological numbering of the components, and flip the comparison when using Tarjan
- Encode common constraints (forcing a value, equal, different) as clauses, and explain why 3-literal clauses break the method