2-SAT Implication Graph

From clauses to graphs

The 2-Satisfiability (2-SAT) problem asks whether there exists an assignment of truth values to a set of variables such that a formula in Conjunctive Normal Form (CNF) with exactly two literals per clause evaluates to true. We can solve this efficiently by reducing it to a graph reachability problem using implications.

Every clause (A OR B) can be rewritten logically as two equivalent implications:(NOT A ➔ B) and (NOT B ➔ A). If we create a directed graph where every literal (each variable and its negation) is a vertex, and these implications form directed edges, we can determine satisfiability by examining the Strongly Connected Components (SCCs) of this implication graph.

Worked example: Detecting a contradiction

Consider a formula with one variable (n=1) and two clauses: (1 OR 1) and (-1 OR -1).

First, we trace the deterministic SCC algorithm over the graph:

Expand (1 OR 1) to the implication -1 ➔ 1.
Expand (-1 OR -1) to the implication 1 ➔ -1.
Run DFS on the implication graph: node 1 visits -1. Exit order: -1, then 1.
Run DFS on the transpose graph: root 1 visits -1, forming the first component C0.

Component C0 = { 1, -1 }

We build a directed graph with vertices for 1 and -1. The edges are -1 ➔ 1 and 1 ➔ -1.

Because there is a path from 1 to -1 and a path from -1 to 1, they are mutually reachable. In graph theory terms, they belong to the same Strongly Connected Component (SCC). Logically, this means that assuming 1 is true implies -1 is true, and vice versa. This is a direct contradiction!

Conclusion: Since a variable and its negation share an SCC, the formula is UNSATISFIABLE (UNSAT). If no such variable existed, it would be SATISFIABLE (SAT).

Experiment with the native controls

Open the interactive 2-SAT Implication Graph module.

Look at the default Variable count (2) and Clauses (1 2, -1 2, 1 -2).
Click Step to reveal the first clause's implications. The graph updates to show the new directed edges between the literals.
Click Step repeatedly until the terminal trace is reached. One Step reveals each clause’s implication pair; the next and final Step computes the SCC certificate and colors the nodes.
Observe the Status output. It will show SAT, and Conflicts will be None, because no variable x shares an SCC color with its negation -x.
Click Reset to clear the graph state.
Change the Variable count to 1 and Clauses to 1 1 and -1 -1. Click Finish to immediately process the graph. Observe the status changes to UNSAT and the conflicting variable is listed.

Assumptions, boundaries and costs

This visualization models exact deterministic reachability for a small number of variables (up to 4) to ensure readability of the graph and its components.

No General SAT Solving: This deterministic polynomial-time algorithm only works for 2-SAT. 3-SAT (and above) is NP-complete, and this implication graph reduction does not apply.
Strict Formatting: Inputs are strictly parsed as two non-zero integers per line. Blank input is the empty conjunction (SAT); malformed nonblank lines are rejected. Duplicate literals like 1 1 are perfectly valid.
No Assignment Extraction: The module correctly identifies if a satisfying assignment exists (SAT) but does not extract or promise to display a specific satisfying assignment.

References

The formulation of the 2-Satisfiability problem as a deterministic graph traversal allows for an elegant reduction from logic to connected components.

2-SAT Deterministic (UPenn CIS 1210): Details the formal reduction of 2-CNF formulas to implication graphs and the correctness of checking SCCs.

2-SAT Implication Graph