Lesson 2

Theorem. The \(2\)-satisfiability problem can be solved in linear (in the size of the input formula) time.

Proof. Consider the 2-clause \((l_{1} \lor l_{2})\). This clause forbids literals \(l_{1}\) and \(l_{2}\) from being zero simultaneously. In other words, if \(l_{1}=0\), then \(l_{2}=1\), and if \(l_{2}=0\), then \(l_{1}=1\). Thus, the clause \((p \lor q)\) has the same truth table as the implications \(\overline{l_1}\Rightarrow l_{2}\) and \(\overline{l_2}\Rightarrow l_{1}\).

All such implications can be represented in the implication graph of the formula:

• for each variable \(x\) we create vertices \(x\) and \(\overline x\);


• for each 2-clause \((l_{1} \lor l_{2})\) we draw directed edges \(\overline{l_1}\to l_{2}\) and \(\overline{l_2}\to l_{1}\);


• for each 1-clause \((l)\) we draw an edge \(\overline{l}\to l\).

For example, for the formula \[(\overline x \lor y) \land (\overline y \lor z) \land (x \lor \overline z) \land (z \lor y)\] the implication graph looks like this:

Our goal is to assign values to the variables so that none of the implications are violated. For the graph above the assignment \(x=1,y=1,z=1\) satisfies all implications, while \(x=0,y=0,z=0\) violates the implications \(\overline{z}\to y\) and \(\overline{y}\to z\), which correspond to the clause \((z \lor y)\).

The resulting graph is skew-symmetric: if there is an edge \(l_{1} \to l_{2}\), then also an edge \(\overline{l_2}\to \overline{l_1}\). This property extends to paths: if there is a path from \(l_{1}\) to \(l_{2}\), then also from \(\overline{l_2}\) to \(\overline{l_1}\). Furthermore, if some assignment satisfies the formula and there is a path from \(l_{1}\) to \(l_{2}\), then it cannot happen that \(l_{1}=1\) and \(l_{2}=0\). Indeed, along this path the first vertex is one and the last is zero, which contradicts the implication.

Now consider the strongly connected components of the implication graph. In any such component there is a path from any vertex to any other. Thus, all vertices in one component must be assigned the same value. In particular, if a variable and its negation are in the same component, the formula is unsatisfiable. If this does not happen, the formula is satisfiable! We prove this algorithmically: using the strongly connected components we construct a satisfying assignment.

To construct a satisfying assignment (when no component contains both \(x\) and \(\overline{x}\)), consider a topological sort \(C_{1}, \dotsc, C_{k}\) of the graph of components. Thus, there are no edges from \(C_{j}\) to \(C_{i}\) when \(i<j\). We iterate over components in reverse order: \(C_{k}, C_{k-1},\dotsc, C_{1}\). If the variables of \(C_{i}\) have not yet been assigned, assign them all one and their negations zero.

It remains to see why the resulting assignment does not violate any implication. Indeed, when we assign a literal to 1, all literals reachable from it have already been assigned one (since we process components in reverse order). Similarly, when we assign a literal to 0, all literals from which it is reachable have already been assigned zero (by skew-symmetry).

The algorithm runs in linear time, since both the graph construction and the computation of strongly connected components and their topological sort are linear.◼