GATE CS 2014 Set 3 Q38 — Undecidability

The decision problem $2 ext{CNFSAT}$ can be solved in polynomial time using an implication graph representation:

1. For each clause $(u \vee v)$ in the formula, we rewrite it as two equivalent implication constraints: $(\neg u \implies v)$ and $(\neg v \implies u)$.
2. We construct a directed implication graph $G = (V, E)$ where the vertices $V$ represent the variables and their negations, and the directed edges $E$ represent these implications.
3. The formula is unsatisfiable if and only if there exists some variable $x$ such that there is a path from $x$ to $\neg x$ and a path from $\neg x$ to $x$ in $G$ (i.e., they belong to the same Strongly Connected Component).

Since finding strongly connected components and checking reachability in a directed graph can be done in linear time $O(|V| + |E|)$ using depth-first search (DFS), $2 ext{CNFSAT}$ is solvable in polynomial time by reduction to directed graph reachability.