Giant Pizza - Implementation

Here is the $2$-SAT implementation for Giant Pizza:

function giantPizza(n, m, customers):
    // Build implication graph: nodes 0..n-1 are x_i, nodes n..2n-1 are NOT x_i
    adj = adjacency list of size 2n

    for each (sign1, topping1, sign2, topping2) in customers:
        a = topping1 if sign1 == '+' else topping1 + n
        b = topping2 if sign2 == '+' else topping2 + n
        notA = (a + n) mod (2n)
        notB = (b + n) mod (2n)

        // clause (a OR b) becomes edges: NOT a -> b, NOT b -> a
        adj[notA].append(b)
        adj[notB].append(a)

    sccId = tarjanSCC(adj)

    // Check satisfiability
    for i from 0 to n - 1:
        if sccId[i] == sccId[i + n]:
            print "IMPOSSIBLE"
            return

    // Construct solution: pick literal with higher SCC index
    result = empty string
    for i from 0 to n - 1:
        if sccId[i] > sccId[i + n]:
            result.append('+')
        else:
            result.append('-')

    print result

Time: $O(V + E)$. Space: $O(V)$.