2-SAT Implementation

#include <iostream>
#include <vector>
#include <algorithm>

using namespace std;

int n;
vector<vector<int>> adj, adjt;
vector<bool> vis;
vector<int> L, comp;

void dfs1(int u)
{
    vis[u] = true;
    for(int v : adj[u])
    {
        if(!vis[v])
            dfs1(v);
    }
    L.push_back(u);
}

void dfs2(int u, int c)
{
    comp[u] = c;
    for(int v : adjt[u])
    {
        if(comp[v] == -1)
            dfs2(v, c);
    }
}

bool solve_2SAT()
{
    L.clear();
    vis.assign(2*n, false);
    adjt.assign(2*n, vector<int>(0));
    for(int i=0;i<2*n;i++)
    {
        for(int j:adj[i])
            adjt[j].push_back(i);
    }

    for(int i = 0; i < 2*n; i++)
    {
        if(!vis[i])
            dfs1(i);
    }

    reverse(L.begin(),L.end());
    comp.assign(2*n, -1);
    int curComp = 0;

    for(int i=0;i<2*n;i++)
    {
        if( comp[L[i]] == -1 )
            dfs2(L[i], curComp++);
    }

    for(int i=0;i<n;i++)
    {
        if(comp[i] == comp[n+i])
            return false;
    }
    return true;
}

int main()
{
    // ( a v !b ) n ( !a v b ) n ( !a v !b ) n ( a v !c )

    // 3 variables
    n = 3;
    // graph with 2*n nodes
    // one for each variable and one for each negation
    adj.assign(2*n, vector<int>(0));

    // !a -> !b
    adj[ n+0 ].push_back(n+1);
    // b -> a
    adj[ 1 ].push_back(0);

    // a -> b
    adj[ 0 ].push_back(1);
    // !b -> !a
    adj[ n+1 ].push_back(n+0);

    // a -> !b
    adj[ 0 ].push_back(n+1);
    // b -> !a
    adj[ 1 ].push_back(n+0);

    // !a -> !c
    adj[ n+0 ].push_back(n+2);
    // c -> a
    adj[ 2 ].push_back(0);

    cout << (solve_2SAT()?"Satisfiable":"Not Satisfiable") << '\n';
}