2sat problem use SCC

2sat.cpp

#include <iostream>
#include <fstream>
#include <vector>
#include <string>
#include <sstream>
#include <random>
#include <assert.h>
#include <algorithm>
#include <ctime>
#include <utility>
#include <stack>
#include <unordered_map>
using namespace std;

class Node{
public:
    Node(int idd=0 ,int ss=-1,int ff=-1):isVisited(false),id(idd),s(ss),f(ff)	{}
    int id;
    int s;
    int f;
    bool isVisited;
    vector<int> adj;
    int operator[](size_t index)
    {
        assert(index< adj.size());
        return adj[index];
    }
};
typedef vector< Node > Graph;
int size=0;
// read from file with adjacency list representation of undirected graph
void getFromtxt(char *name, Graph &graph)
{
    std::clock_t c_start = std::clock();
    cout<<"Begin to read file!"<<endl;
    ifstream input;
    input.open(name);//read from a txt file
    if(input.is_open())
    {
        int s,t,ns,nt;
        input>>size;
        cout<<"size:"<<size<<endl;
        graph.push_back( Node());// graph index begin with 1 not 0
        graph.resize(size*2+1);
        while (input>> s >> t)
        {
            if(s<0){ns=-s;s=size-s;}
            else {ns=size+s;}
            if(t<0){nt=-t;t=size-t;}
            else {nt=size+t;}
            graph[ns].adj.push_back(t);
            graph[nt].adj.push_back(s);
        }
        std::clock_t c_end = std::clock();
        cout<<"Read file finished!"<<endl;
        std::cout << "CPU time used: "
              << 1000.0 * (c_end-c_start) / CLOCKS_PER_SEC
              << " ms\n";
    }
    else cout<<"Cannot open "<<name<<endl;
}

bool cmp(pair<int,int> &a, pair<int,int> &b)
    {
        return a.first<b.first;
    }
class SCC{
public:
    void compute(Graph &graph)
    {
        std::clock_t c_start = std::clock();
        //prepare data
        _graph.swap(graph);
        getReverseGraph(_graph);
        leader.resize(_graph.size());
        finished.resize(_graph.size());
        //first pass dfs compute finished
        dfsloop(_graphrev);
        getOrder();
        //second pass search graph node in the decreased order of their finished score compute by the first pass
        dfsloop(_graph,2);
        getSCCs();
        std::clock_t c_end = std::clock();
        std::cout << "Total time used: "
              << 1000.0 * (c_end-c_start) / CLOCKS_PER_SEC
              << " ms\n";
    }
    void dfsloop(Graph &graph,int pass=1)
    {
        std::clock_t c_start = std::clock();
        total=0;
        start=-1;
        if(pass==1)//first pass
        {
            cout<<"first pass"<<endl;
            int node=graph.size();
            while(--node>0)
            {
                if(!graph[node].isVisited)
                {
                    start=node;
                    dfs(graph,node);
                }
            }

        }
        else //second pass
        {
            cout<<"second pass"<<endl;
            int node=finished.size();
            while(--node>0)
            {
                if(!graph[finished[node].second].isVisited)
                {
                    start=finished[node].second;
                    dfs(graph,finished[node].second);
                }
            }
        }
   }

    void dfs(Graph &graph,int node)
    {
        graph[node].isVisited=true;
        graph[node].s=start;
        for(int i=0;i<graph[node].adj.size();++i)
            if(!graph[graph[node][i]].isVisited)
                dfs(graph,graph[node][i]);
        ++total;
        graph[node].f=total;//finished time
   }

    void getReverseGraph(Graph &graph)
    {
       _graphrev.resize(graph.size());
        for(int i=1;i<graph.size();++i)
        {
            for(int j=0;j<graph[i].adj.size();++j)
                _graphrev[graph[i][j]].adj.push_back(i);
        }
   }
    void getOrder()
    {
        if(finished.size()<_graphrev.size())
            finished.resize(_graphrev.size());

        for(int i=1;i<_graphrev.size();++i)
        {
            finished[i]=std::make_pair<int,int>(_graphrev[i].f,i);
        }

        sort(finished.begin(),finished.end(), cmp);

    }

    void getSCCs()
    {
       bool satify=true;
        for(int i=1;i<=size;i++){
            if(_graph[i].s==_graph[i+size].s){
                satify=false;
                break;
            }
        }
        if(satify)cout<<"Satify"<<endl;
        else cout<<"Unsatify"<<endl;
   }
private:
    Graph _graph;
    Graph _graphrev;
    // leader and finished are extra variables
    vector<int> leader;
    vector<std::pair<int,int> > finished;
    int start;//start of dfs
    int total;//total visited
    vector<int> sccNums;
};

int main(int argv,char **argc)
{
    Graph graph;
    getFromtxt("2sat6.txt",graph);
    SCC scc;
    if(graph.size()>2)
        scc.compute(graph);
    return 0;
}