2-Satisfiability Problem

computation

Definition

2-Satisfiability Problem

The 2-SAT problem is a specific form of the SAT where every clause consists of at most 2 literals.

Example: $(x_1\vee \neg x_2)\wedge (\neg x_1\vee x_3)\wedge (x_2\vee x_3)$

Reductions

Turing Reduction to Graph-Reachability Problem

2-SAT

Given a 2-CNF formula $\phi$, construct its implication graph $G_{\phi }$.

For each variable $x$ in $\phi$, ask whether there is a path from $x$ to $\neg x$ and a path from $\neg x$ to $x$ in $G_{\phi }$.

If this happens for some $x$, return false. Otherwise, return true.

procedure test2SAT:
  Input: propositional formula φ in 2-CNF
  Output: true if φ is satisfiable and false otherwise
 
  from φ construct Gφ
  for all variables x in φ do {
    if Gφ contains a path from x to ¬x
      and a path from ¬x to x then return false;
  }
  return true;

In this way, the satisfiability of $\phi$ is decided by repeated calls to graph reachability.