At most two literals per clause
A literal is a variable or its negation. The formula (p∨q)∧(¬p∨r)∧(¬r∨q) requires three clauses to hold together; the number 2 limits clause width rather than the total number of variables. A unit condition p can be represented as p∨p.
A clause a∨b is equivalent to the pair of implications ¬a→b and ¬b→a. Construct two vertices per variable, one positive and one negative, and add these directed edges. A path then records consequences that any satisfying assignment must respect.
References: [1]
Contradictions within a component
If p and ¬p lie in one strongly connected component, each reaches the other. Choosing either literal as true forces its opposite to be true as well. A path in just one direction is insufficient for this contradiction; mere connection between opposite literals is not the criterion.
Conversely, when opposite literals always occupy different components, their condensation graph admits a consistent assignment. Process unassigned components in reverse topological order, making a selected component true and its dual false. This preserves implications and establishes sufficiency, rather than only a necessary test.
References: [1]
Why the restricted form matters
For n variables and m clauses of width at most two, the graph has 2n vertices and at most 2m edges. Linear-time SCC computation gives an overall O(n+m) bound for explicit input, including graph construction and assignment. An encoding from another problem may have its own size cost.
Allowing width three already includes NP-complete 3-SAT. The implication-graph criterion therefore cannot be applied to arbitrary clauses, nor may a three-way alternative simply be replaced by arbitrary pairs. Efficient solvability depends on preserving the restricted constraint form.