Consider the decision problem \(2CNFSAT\) defined as follows: \(\left\{ \phi…
2014
Consider the decision problem \(2CNFSAT\) defined as follows:
\(\left\{ \phi \mid \phi \text{ is a satisfiable propositional formula in CNF with at most two literals per clause}\right\}\)
For example, \(\phi = (x1 \vee x2) \wedge (x1 \vee \bar{x3}) \wedge (x2 \vee x4)\) is a Boolean formula and it is in \(2CNFSAT\).
The decision problem \(2CNFSAT\) is
- A.
NP-Complete.
- B.
solvable in polynomial time by reduction to directed graph reachability.
- C.
solvable in constant time since any input instance is satisfiable.
- D.
NP-hard, but not NP-complete.
Attempted by 49 students.
Show answer & explanation
Correct answer: B
Answer: The problem is solvable in polynomial time (indeed linear time) by reducing to a directed implication graph and analyzing strongly connected components.
Build the implication graph:
For each clause (a ∨ b), add directed edges (¬a → b) and (¬b → a). Each literal (variable or its negation) is a node.
Find strongly connected components (SCCs) of the directed graph using Kosaraju or Tarjan.
Decide satisfiability:
If any variable and its negation are in the same SCC, the formula is unsatisfiable (there are paths both ways leading to a contradiction).
Otherwise the formula is satisfiable. To construct a satisfying assignment, collapse SCCs to form a DAG, process components in reverse topological order, and assign each variable a truth value consistent with implications (assign false to a component before assigning true to its negation's component).
Complexity: Building the graph and computing SCCs can be done in O(n + m) time, where n is the number of variables (times two for literals) and m is the number of clauses. Thus 2-CNF-SAT is solvable in linear time and therefore is in P.
Key insight: the logical constraints of a 2-CNF formula map directly to reachability constraints in a directed graph; consistency is checked by SCC membership.
A video solution is available for this question — log in and enroll to watch it.