2-SAT

class TwoSAT {
    constructor(n) {
        this.n = n; // number of variables
        this.adj = Array.from({length: 2*n}, () => []);
        this.radj = Array.from({length: 2*n}, () => []);
    }

    // Add clause (x ∨ y) where literals: variable i = i, negation = i+n
    addClause(x, y) {
        // ¬x → y and ¬y → x
        const negX = x < this.n ? x + this.n : x - this.n;
        const negY = y < this.n ? y + this.n : y - this.n;
        this.adj[negX].push(y);  this.radj[y].push(negX);
        this.adj[negY].push(x);  this.radj[x].push(negY);
    }

    solve() {
        const n2 = 2 * this.n;
        const order = [], visited = new Array(n2).fill(false);
        const dfs1 = (v) => {
            visited[v] = true;
            for (const u of this.adj[v]) if (!visited[u]) dfs1(u);
            order.push(v);
        };
        for (let i = 0; i < n2; i++) if (!visited[i]) dfs1(i);
        const comp = new Array(n2).fill(-1);
        let numComp = 0;
        const dfs2 = (v, c) => {
            comp[v] = c;
            for (const u of this.radj[v]) if (comp[u] === -1) dfs2(u, c);
        };
        for (let i = n2 - 1; i >= 0; i--) {
            if (comp[order[i]] === -1) dfs2(order[i], numComp++);
        }
        // Check satisfiability and extract assignment
        const vals = new Array(this.n);
        for (let i = 0; i < this.n; i++) {
            if (comp[i] === comp[i + this.n]) return null; // unsatisfiable
            vals[i] = comp[i] > comp[i + this.n]; // higher comp = later in topo = TRUE
        }
        return vals;
    }
}

// Usage:
// const sat = new TwoSAT(n);
// sat.addClause(x, y)  -- (var_x OR var_y)
// sat.addClause(x, x+n) -- forces var_x to be TRUE (x OR NOT x is tautology, but: x AND ¬¬x = x)
// For "var x must be true": addClause(x, x) if using literal encoding
// const result = sat.solve(); // null = unsat, array = assignment