2-SAT

Deciding satisfiability of boolean formulas with two literals per clause in linear time via implication graphs.

The problem

A 2-SAT instance is a conjunction of clauses, each an OR of exactly two literals (a variable or its negation). Unlike general SAT, which is NP-complete, 2-SAT is solvable in linear time. The key is to rewrite each clause as two implications and analyze the resulting implication graph.

Implication graph

The clause (a OR b) is logically equivalent to (not a implies b) and (not b implies a). Building a directed graph with a vertex for each literal and its negation, and adding both implications per clause, captures the constraints. The formula is satisfiable if and only if no variable x and its negation lie in the same strongly connected component.

Assignment from SCC order

python

# comp[] from an SCC algorithm; components in reverse topological order
def solve(n, comp):
    for i in range(n):
        if comp[2*i] == comp[2*i+1]:
            return None            # x and not-x in same SCC -> UNSAT
    # variable is true if its positive literal's SCC comes later
    return [comp[2*i] > comp[2*i+1] for i in range(n)]

Why it works

If x and not-x share an SCC, each implies the other, forcing a contradiction. Otherwise, choosing for each variable the literal whose SCC appears later in reverse topological order yields a consistent assignment, because implications only point from earlier to later components. Computing SCCs takes O(V + E), so 2-SAT is linear.

Applications

• Scheduling with binary either-or constraints.
• Consistency of pairwise preferences and conflict resolution.
• Some geometric labeling and map-labeling feasibility tests.
• A model problem showing the boundary between tractable and NP-hard SAT.