2-SAT via SCC, in depth: why component order is the assignment, an iterative solver, contradiction cycles and forced literals

The implication graph and its symmetry

Give each variable x two literal nodes, x and ¬x, for 2n nodes in all. A clause (u ∨ v) says that at least one literal is true, which is the same as saying ¬u → v and ¬v → u. Add both edges for every clause. The graph is skew-symmetric: whenever u → v is an edge, so is ¬v → ¬u. That symmetry is what makes every argument below work, so it is worth keeping the encoding that guarantees it: store literal x as 2*x and ¬x as 2*x + 1, so negation is l ^ 1 and the contrapositive edge is never forgotten.

Implication is transitive, so a path u ⇒ v also forces v whenever u is true. Two facts follow at once. If x and ¬x lie in the same SCC, then x ⇒ ¬x and ¬x ⇒ x, so neither value survives and the formula is unsatisfiable. Less obviously, when every literal sits in a different component from its complement, the formula is satisfiable, and the topological order of the components hands you a model. The next section proves that claim, because the proof is also the clearest way to remember which direction the rule runs.

Why component order is the assignment

Contract each SCC to one node to get the condensation, a DAG, and fix a topological order pos(·) so every edge goes from a smaller position to a larger or equal one. Set x true exactly when pos(x) is greater than pos(¬x), that is, when x's component is closer to the sinks.

Suppose some clause is violated. Then there is an edge u → v with u true and v false. Translate each fact into positions: u true means pos(¬u) < pos(u); v false means pos(v) < pos(¬v); the edge u → v gives pos(u) ≤ pos(v); and its skew-symmetric partner ¬v → ¬u gives pos(¬v) ≤ pos(¬u). Chain them: pos(u) ≤ pos(v) < pos(¬v) ≤ pos(¬u) < pos(u). A position strictly smaller than itself is impossible, so no clause is violated. The proof never used anything except the edge, its contrapositive and the order, which is why the algorithm is correct for any valid topological order of the condensation.

The intuition behind choosing the later component is that implications only push truth downstream. Choosing a literal near the sinks commits you to very little, because little is reachable from it; choosing one near the sources would force everything reachable from it, possibly including its own negation.

Tarjan or Kosaraju: which way the ids point

You never sort the condensation explicitly. Both standard SCC algorithms emit components in a topological order as a side effect, but they emit it in opposite directions, and mixing them up inverts every value. The inverted assignment is still wrong even when it happens to pass a test on a symmetric formula, which is how this bug survives code review.

Tarjan finishes a component only after every component reachable from it has been finished and numbered, so reachable components get smaller ids. Kosaraju's first pass records finish times; the second pass walks the transposed graph in decreasing finish time, and the node with the latest finish lies in a source component of the original graph, so ids grow downstream. Write the rule next to the SCC call with a comment saying which algorithm you used, and keep a randomized brute-force test that would catch an inversion.

An iterative solver with a contradiction cycle

Here the SCC pass is Tarjan written with an explicit work stack, so a long implication chain cannot overflow Python's recursion limit, which is about a thousand frames by default and is easy to exceed with a few thousand variables. It returns either an assignment or the component array, and a second method turns an unsatisfiable verdict into an explicit cycle through x and ¬x. The code was checked against an exhaustive search over 3,000 random formulas of up to six variables.

def lit(var, positive=True):
    return 2 * var + (0 if positive else 1)

def neg(l):
    return l ^ 1


class TwoSat:
    def __init__(self, n_vars):
        self.n = n_vars
        self.adj = [[] for _ in range(2 * n_vars)]

    def add_clause(self, a, b):            # (a OR b)
        self.adj[neg(a)].append(b)          # not a  ->  b
        self.adj[neg(b)].append(a)          # not b  ->  a

    def _tarjan(self):
        N = 2 * self.n
        index, low, comp = [-1] * N, [0] * N, [-1] * N
        on_stack = [False] * N
        stack, counter, n_comp = [], 0, 0
        for root in range(N):
            if index[root] != -1:
                continue
            work = [(root, 0)]               # (node, next edge position)
            while work:
                v, i = work[-1]
                if i == 0:                   # first visit
                    index[v] = low[v] = counter
                    counter += 1
                    stack.append(v)
                    on_stack[v] = True
                if i < len(self.adj[v]):
                    work[-1] = (v, i + 1)
                    w = self.adj[v][i]
                    if index[w] == -1:
                        work.append((w, 0))
                    elif on_stack[w]:
                        low[v] = min(low[v], index[w])
                    continue
                work.pop()                   # v is finished
                if work:
                    u = work[-1][0]
                    low[u] = min(low[u], low[v])
                if low[v] == index[v]:       # v roots a component
                    while True:
                        w = stack.pop()
                        on_stack[w] = False
                        comp[w] = n_comp
                        if w == v:
                            break
                    n_comp += 1
        return comp

    def solve(self):
        comp = self._tarjan()
        assignment = []
        for v in range(self.n):
            t, f = comp[lit(v)], comp[lit(v, False)]
            if t == f:
                return None, comp
            # Tarjan numbers components in reverse topological order,
            # so the smaller id is the one further downstream.
            assignment.append(t < f)
        return assignment, comp

    def contradiction_cycle(self, v):
        """Literal path v -> ... -> not v -> ... -> v, proving unsatisfiability."""
        def path(src, dst):
            prev, queue = {src: None}, [src]
            for x in queue:
                if x == dst:
                    break
                for y in self.adj[x]:
                    if y not in prev:
                        prev[y] = x
                        queue.append(y)
            out, x = [], dst
            while x is not None:
                out.append(x)
                x = prev[x]
            return out[::-1]
        there = path(lit(v), lit(v, False))
        back = path(lit(v, False), lit(v))
        return there + back[1:]

Note that the parent's low-link is updated only after the child is popped, mirroring the line after the recursive call in the textbook version.

Worked example: three variables, then one clause too many

Take three variables and four clauses: (a ∨ b), (a ∨ ¬b), (¬a ∨ c), (¬b ∨ ¬c). The eight implication edges are ¬a→b, ¬b→a, ¬a→¬b, b→a, a→c, ¬c→¬a, b→¬c and c→¬b.

Tarjan starts at node a. From a it reaches c, from c it reaches ¬b, and ¬b points back to a, so {a, c, ¬b} closes as the first component and receives id 0. The next unvisited root is ¬a, which reaches b, which reaches ¬c, which points back to ¬a; its edges into a and ¬b lead to already-finished nodes. {¬a, b, ¬c} closes as id 1. Reading the rule with Tarjan ids: id(a)=0 < id(¬a)=1 so a is true; id(b)=1 is not smaller than id(¬b)=0 so b is false; id(c)=0 < id(¬c)=1 so c is true. Check the clauses: a satisfies the first two, c the third, ¬b the fourth.

Now add one clause, (¬a ∨ b), which contributes a→b and ¬b→¬a. The new edges connect the two components in both directions and everything collapses into one SCC, so a and ¬a share a component and the solver returns no assignment. contradiction_cycle(0) returns a → c → ¬b → ¬a → b → a. Read it aloud as the proof: if a is true then c (clause 3), then ¬b (clause 4), then ¬a (the new clause), a contradiction; if a is false then b (clause 1), then a (clause 2), another contradiction. Every arrow names a clause, so this cycle is exactly what a user who wrote conflicting constraints needs to see.

Beyond yes or no: what-if queries and forced literals

A yes-or-no answer is rarely the end. Configuration tools want to grey out options that are already decided, and planners want to know whether a choice is still open. Two facts, both following from transitivity, answer these with plain reachability on a satisfiable formula F.

• Can literal u be true? F ∧ u is satisfiable if and only if there is no path u ⇒ ¬u. Adding u is the clause (u ∨ u), which adds the edge ¬u → u; a contradiction needs a path from u back to ¬u, and that path would already exist in F.
• Is u forced? u is true in every model exactly when ¬u ⇒ u. Such literals form the backbone of the formula. Testing each literal with a breadth-first search costs O(n(n + m)); on the condensation with bitset reachability it is much cheaper in practice.

def reaches(solver, src, dst):
    seen, queue = {src}, [src]
    for x in queue:
        if x == dst:
            return True
        for y in solver.adj[x]:
            if y not in seen:
                seen.add(y)
                queue.append(y)
    return False

def can_be_true(solver, u):
    return not reaches(solver, u, neg(u))

def forced_literals(solver):
    return [l for l in range(2 * solver.n) if reaches(solver, neg(l), l)]

In the satisfiable worked example, forced_literals returns a, ¬b and c: the formula has exactly one model. Some questions do not stay easy. Counting the models of a 2-SAT formula is #P-complete, as Valiant showed in 1979, and maximising the number of satisfied clauses (MAX-2-SAT) is NP-hard. If a product requirement turns into either, reach for a different tool rather than stretching the SCC method.

Scaling it up

The algorithm is linear, so the constant factors are what you tune. For millions of clauses, replace lists of lists with a compressed sparse row layout: count out-degrees, prefix-sum them into an offsets array, then fill a flat targets array, which roughly halves memory and keeps edge scans sequential. Deduplicate clauses before building. Encodings such as at-most-one over k literals produce k(k-1)/2 clauses when written pairwise; prefix-variable encodings bring that down to O(k) clauses with extra variables, and on large groups that is the difference between seconds and minutes.

If clauses arrive incrementally, note that the SCC structure can merge but never split as clauses are added, so verdicts only move from satisfiable to unsatisfiable. A simple policy is to answer point queries with the reachability tests above and rebuild the full solution in batches. Every check you run as part of maintaining a topological order online applies here too, because the implication graph only gains edges, so its components can only merge.

Failure modes

• Inverted rule. Using the Kosaraju comparison with Tarjan ids, or the reverse. Symptom: assignments that violate clauses on asymmetric formulas. Fix: verify every returned model against the clause list before returning it; the check is linear and catches this class of bug permanently.
• Missing contrapositive. Adding only ¬u → v. The graph loses skew symmetry and the proof above no longer holds, so the solver can return a wrong verdict. Always add edges in one function that writes both.
• Unit clauses mishandled. A constraint that x must be true is the clause (x ∨ x), which yields the single edge ¬x → x. Do not drop it because it looks degenerate.
• Recursion overflow. A recursive SCC on a chain of 100,000 implications crashes in Python and can blow a thread stack elsewhere. Use the iterative form.
• Opaque failures. Returning only false when the formula is unsatisfiable. Users cannot fix what they cannot see; return the contradiction cycle mapped back to the clauses that produced each edge.

What to do next

1. Implement the solver with the 2*x / 2*x+1 literal encoding and a single add_clause that writes both edges.
2. Write a randomized test that compares the solver's verdict against exhaustive search for up to eight variables and checks every returned assignment against the clauses.
3. Decide which SCC algorithm you use and put the id comparison rule in a comment beside the call.
4. Store, for each edge, the index of the clause that produced it, so contradiction cycles can be reported as clause lists.
5. Add can_be_true and forced_literals if your users configure choices interactively.
6. Profile on your largest real instance; switch to compressed sparse rows and deduplicate clauses if building the graph dominates.