-SAT (Boolean satisfiability with two literals per clause) problems use SCC detection to check if a solution exists. Build an implication graph where each variable has two nodes: and (not ).
For each clause, add implication edges. If and end up in the same SCC, no satisfying assignment exists. If they are in different SCCs, a solution exists.
Assign truth values based on the topological order of SCCs in the condensation graph. You will see this technique in detail in the next section.