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:

Reductions

Turing Reduction to Graph-Reachability Problem

See Krom Formula

2-SAT

Given a 2-CNF formula , construct its implication graph .

For each variable in , ask whether there is a path from to and a path from to in .

If this happens for some , 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 is decided by repeated calls to graph reachability.