Learning notes on 2-SAT

Algorithm to solve 2-SAT

First decompose the implication graph into SCCs, and then if $x_i$ and $\neg x_i$ is in the same SCC, then the answer is impossible. Else it suffices to choose the variable that appears later in the topological order to be true.

Problems and Techniques

Enforcing one variable to be true: link
To do that, we can just add an edge from $\neg x_i$ to $x_i$

Enforcing at most one variable among several to be true
This can be done in $O(n)$. Order the nodes arbitrarily. Then we can build prefix nodes for each prefix part of the nodes and establish implication between those prefix nodes and the variables themselves.