Untitled

#include <bits/stdc++.h>

using namespace std;

vector < vector<int> > clauses;
unordered_map<int,int> l_freq;
unordered_map<int,bool> l_assign;

void input_file(), reset(vector<vector<int>>), unit_propagate(vector<vector<int>>), pure(vector<vector<int>>), dlis(vector<vector<int>>);
bool isunit(vector<vector<int>>), dpll(vector<vector<int>>);

int main(int argc, char *argv[])
{
    input_file();

    if(dpll(clauses))
    {
        cout << "s SATISFIABLE";
        for(auto f: l_assign)
        {
            cout << "v \" " << f.first << " \" -> " << f.second;
        }
        cout << "Done";
    }
    else
    {
        cout << "s UNSATISFIABLE";
        return 0;
    }

    /*for(int a=0; a<clauses.size(); a++)
    {
        for(int b=0; b<clauses[a].size(); b++)
        {
            cout << clauses[a][b] << " ";
        }
        cout << endl;
    }*/
}

void input_file()
{
    ifstream file("testcase1.cnf");
    //ifstream file(argv[1]);
    vector<int> temp;

    string line, t;
    getline(file, line);
    stringstream ss(line);

    int n;
    ss >> t;
    ss >> t;
    ss >> n;
    ss >> n;

    for(int a=0; a<n; a++)
    {
        getline(file, line);
        stringstream ss(line);
        int l;

        while(ss>>l && l!=0)
        {
            temp.push_back(l);
        }

        clauses.push_back(temp);
        temp.clear();
    }
}

void reset(vector < vector<int> > clause)
{
    for(int a=0; a<clause.size(); a++)
    {
        for(int b=0; b<clause[a].size(); b++)
        {
            l_assign[abs(clause[a][b])]==true;
        }
    }
}

bool dpll(vector < vector<int> > clause)
{
    reset(clause);

    for(int a=0; a<clause.size(); a++)
    {
        for(int b=0; b<clause[a].size(); b++)
        {
            l_freq[clause[a][b]]++;
        }
    }

    while(isunit(clause))
    {
        unit_propagate(clause);
    }
    pure(clause);

    if(clause.empty())
    {
        return true;
    }

    for(int a=0; a<clause.size(); a++)
    {
        if(clause[a].empty())
        {
            return false;
        }
    }

    dlis(clause);
}

bool isunit(vector < vector<int> > clause)
{
    for(int a=0; a<clause.size(); a++)
    {
        if(clause[a].size()==1)
        {
            return true;
        }
    }
    return false;
}

void unit_propagate(vector < vector<int> > clause)
{
    for(int a=0; a<clause.size(); a++)
    {
        if(clause[a].size()==1)
        {
            if(clause[a][0]<0)
            {
                l_assign[0-clause[a][0]]=false;
            }

            for(int b=0; b<clause.size(); b++)
            {
                auto i= find(clause[b].begin(), clause[b].end(), clause[a][0]);
                auto ni= find(clause[b].begin(), clause[b].end(), 0-clause[a][0]);

                if(i!= clause[b].end())
                {
                    clause.erase(clause.begin()+b);
                }

                if(ni!= clause[b].end())
                {
                    clause[b].erase(ni);
                }
            }
            clause.erase(clause.begin()+a);
        }
    }
}

void pure(vector < vector<int> > clause)
{
    for(auto f: l_freq)
    {
        if(f.second+l_freq[0-(f.first)]==1)
        {
            for(int a=0; a<clause.size(); a++)
            {
                auto it=find(clause[a].begin(), clause[a].end(), f.first);
                if(it!=clause[a].end())
                {
                    if(f.first<0)
                    {
                        l_assign[abs(f.first)]=false;
                    }
                    clause.erase(clause.begin()+a);
                }
            }
        }
    }
}

void dlis(vector < vector<int> > clause)
{
    int large=0, fr=0;

    for(auto f: l_freq)
    {
        if(l_freq[f.first]+ l_freq[0-f.first] > fr)
        {
            if(l_freq[f.first] >= l_freq[0-f.first])
            {
                large=f.first;
            }
            else
            {
                large=0-f.first;
            }
            fr=l_freq[f.first]+ l_freq[0-f.first];
        }
    }

    if(large<0)
    {
        l_assign[abs(large)]=false;
    }

    int b=0;
    while(b<clause.size())
    {
        //cout << 1;
        auto i= find(clause[b].begin(), clause[b].end(), large);
        //cout << 2;
        auto ni= find(clause[b].begin(), clause[b].end(), 0-large);
        //cout << 3;
        if(i!= clause[b].end())
        {
            clause.erase(clause.begin()+b);
        }
        //cout << 4;
        if(ni!= clause[b].end())
        {
            clause[b].erase(ni);
        }
        //cout << 5;
        b++;
    }

    for(int a=0; a<clauses.size(); a++)
    {
        for(int b=0; b<clauses[a].size(); b++)
        {
            cout << clauses[a][b] << " ";
        }
        cout << endl;
    }

    dpll(clause);
}