Pattern: 2-SAT

Use $2$-SAT when:

• You have boolean variables
• Each constraint involves exactly $2$ literals
• Constraints are disjunctions (OR)

Form: $(x \lor y) \land (\neg x \lor z) \land.$

Recognize it: "Either A or B must happen." "If A, then not B." These translate to $2$-SAT clauses.

Solution: Build implication graph, find SCCs. Satisfiable if no variable and its negation are in the same SCC.