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>>, int), pure(vector<vector<int>>);
bool dpll(vector<vector<int>>);
int dlis(vector<vector<int>>), isunit(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)!=-1)
    {
        unit_propagate(clause, isunit(clause));
        cout <<"unitdone" << endl;
    }
    pure(clause);
    if(clause.empty())
    {
        return true;
    }
    for(int a=0; a<clause.size(); a++)
    {
        if(clause[a].empty())
        {
            return false;
        }
    }
    vector<vector<int>> fclause =clause;
    vector<int> temp ={dlis(clause)};
    clause.push_back(temp);
    temp={-dlis(clause)};
    fclause.push_back(temp);

    return (dpll(clause)||dpll(fclause));
}

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

void unit_propagate(vector<vector<int>> clause, int i)
{
    int unitLiteral = clause[i][0];

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

    int b=0;
    while(b<clause.size())
    {
        for(int c=0; c<clause[b].size(); c++)
        {
            if(clause[b][c] == unitLiteral)
            {
                clause.erase(clause.begin()+b);
            }
            else if(clause[b][c] == -unitLiteral)
            {
                clause[b].erase(clause[b].begin()+c);
            }
        }
        b++;
    }
}



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);
                }
            }
        }
    }
}

int 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];
        }
    }
    return large;
}