2‐SAT (By Rami) - YessineJallouli/Competitive-Programming GitHub Wiki

#include <bits/stdc++.h>

// 0-indexed

using namespace std;
using vi = vector<int>;
using vvi = vector<vi>;
using vb = vector<bool>;

struct Sat2 {
    int n, d;
    vvi adj, rev;

    explicit Sat2(int _d) : n(2 * _d), adj(n), rev(n), d(_d)
    {
    }

    void topoSort(int r, vi &L, vb &vis)
    {
        if (!vis[r])
        {
            vis[r] = true;
            for (auto s: adj[r]) topoSort(s, L, vis);
            L.push_back(r);
        }
    }


    vi topoSort() {
        vb vis(n);
        vi L;
        for (int i = 0; i < n; i++) topoSort(i, L, vis);
        std::reverse(L.begin(), L.end());
        return L;
    }

    // Decomposition of strongly connected components
    struct SCDec {
        int components; // Number of components
        vi componentId; // A map that gives the id of the strongly connected component of a node
        vi topologicalOrder; // A topological order of the components
    };

    void assign(int u, vb &assigned,vi & cmpId,int id)
    {
        if (assigned[u]) return;
        cmpId[u]=id;
        assigned[u] = true;
        for (int v : rev[u]) assign(v,assigned,cmpId,id);
    }

    SCDec getSCComponents()
    {
        vi topoOrder = topoSort(),cmpId(n);
        vb hasId(n);
        int components=0;
        for (auto i :topoOrder) if (!hasId[i]) assign(i,hasId,cmpId,components++);
        return {components,cmpId, topoOrder};
    }

    // Get a solution, or an empty vector if not satisfiable (the most important one)
    vb satisfy()
    {
        vb vis(2 * d), sol(d), assigned(d);
        auto &&[components,cmpId, topoOrder] = getSCComponents();
        vi topoIndex(2*d);
        vb cmpAssigned(components);
        for (int i = 0; i < n; i += 2) {
            if (cmpId[i] == cmpId[i^1]) return {};
            sol[i / 2] = cmpId[i] > cmpId[i^1];
        }
        return sol;
    }

    // Connect two nodes in a graph
    void connect(int a, int b, bool r1, bool r2)
    {
        adj[2*a^r1].push_back(2*b^r2);
        rev[2*b^r2].push_back(2*a^r1);
    }

    // Add a 2-SAT clause.
    void addClause(int a, int b, bool r1, bool r2) {
        connect(a, b, !r1, r2);
        connect(b, a, !r2, r1);
    }

    // a ∨ b
    void addOr(int a, int b) {
        addClause(a, b, false, false);
    }

    // ⅂a ∨ ⅂b
    void addNand(int a, int b) {
        addClause(a, b, true, true);
    }

    // a => b. Equivalent to: ⅂a ∨ b
    void addImplication(int a, int b) {
        addClause(a, b, true, false);
    }

    // a <=> b. Equivalent to a => b and b => a
    void addEquivalence(int a, int b) {
        addImplication(a, b);
        addImplication(b, a);
    }

    // a ∨ b, but not a ∧ b
    void addExclusion(int a, int b) {
        addOr(a, b);
        addNand(a, b);
    }

    // Assume that a has value r.
    void addAssumption(int a, bool r) {
        addClause(a,a,r,r);
    }

    bool satisfiable() {
        return !satisfy().empty();
    }

};

int main()
{
    std::ios_base::sync_with_stdio(false);
    std::cin.tie(nullptr);
    string garbage1,garbage2;
    int n,m;
    cin >> garbage1 >> garbage2 >> n >> m;
    Sat2 S(n);
    for(int i=0;i<m;i++)
    {
        int a,b,trash;
        cin >> a >> b >> trash;
        bool r1 = a < 0,r2 = b < 0;
        a=abs(a)-1,b=abs(b)-1;
        S.addClause(a,b,r1,r2);
    }
    auto sol=S.satisfy();
    if(sol.empty())
        cout << "s UNSATISFIABLE\n";
    else
    {
        cout << "s SATISFIABLE\nv ";
        for(int i=0;i<n;i++)
        {
            int v = sol[i];
            cout << (2*v-1) * (i+1) << ' ';
        }
        cout << 0 << '\n';
    }
}