2-SAT

O(n + m)

Satisfiability of clauses with two literals each, via the implication graph: clause (a or b) becomes edges ¬a→b and ¬b→a, then a variable and its negation must land in different SCCs. Needs the SCC (Kosaraju) template pasted above this; its topological component ids make the assignment rule a one-liner.

// use it on

CSES: Giant Pizza ↗

Each family member gives a clause of two topping literals. Feasibility plus an assignment is exactly what solve() returns.

// the code

// requires the SCC (Kosaraju) template
struct TwoSat {
    int n;
    SCC scc;
    TwoSat(int n) : n(n), scc(2 * n) {}  // literal x -> node 2x, !x -> 2x+1
    // add clause (a or b); pass (var, isPositive) for each literal
    void add_clause(int a, bool va, int b, bool vb) {
        scc.add_edge(2 * a + (va ? 1 : 0), 2 * b + (vb ? 0 : 1));  // !a -> b
        scc.add_edge(2 * b + (vb ? 1 : 0), 2 * a + (va ? 0 : 1));  // !b -> a
    }
    // returns an assignment, or {} if unsatisfiable
    vector<bool> solve() {
        scc.run();
        vector<bool> res(n);
        for (int x = 0; x < n; x++) {
            if (scc.comp[2 * x] == scc.comp[2 * x + 1]) return {};
            res[x] = scc.comp[2 * x] > scc.comp[2 * x + 1];
        }
        return res;
    }
};

// more dags & satisfiability

Topological Sort (Kahn)