2-SAT Implication Graph

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.

Experiment with the native controls

Open the interactive 2-SAT Implication Graph module.

1. Look at the default Variable count (2) and Clauses (1 2, -1 2, 1 -2).
2. Click Step to reveal the first clause's implications. The graph updates to show the new directed edges between the literals.
3. 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.
4. 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.
5. Click Reset to clear the graph state.
6. 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.