main.cpp

#include<bits/stdc++.h>
#include <fstream>
using namespace std;

struct myclass {
    bool operator() (int a, int b) { return abs(a)< abs(b); }
} sorting;

int check_empty_clause(vector<set<int>> &clauses){
    int cl = clauses.size();
    for(int i=0;i<cl;i++)
    {
        if(clauses[i].size()==0)
            return 1;
    }
    return 0;
}

void remove_new_p(vector<set<int>>&clauses, vector<int> &assignment){
    int new_p = assignment.back();
    for(int i=0;i<clauses.size();i++)
    {
        if(clauses[i].find(new_p) != clauses[i].end()){
            clauses.erase(clauses.begin()+i);
            i-=1;
        }
        else if(clauses[i].find(-1*new_p)!=clauses[i].end()){
            clauses[i].erase(clauses[i].find(-1*new_p));
        }
    }
    return;
}

void unit_prop(vector<set<int>> &clauses,vector<int> &assignment){
    int flag=1;
    while(flag==1){
        flag=0;
        int rows = clauses.size();
        for(int i=0;i<rows;i++){
            if(clauses[i].size()==1){
                flag=1;
                set<int>::iterator it = clauses[i].begin();
                assignment.push_back(*it);
                clauses.erase(clauses.begin());
                remove_new_p(clauses,assignment);
                break;
            }
        }
    }
    return;
}


void pure_literal(vector<set<int>> &clauses, vector<int> &assignment, int literals){
    int check_arr1[literals+1];
    int check_arr2[literals+1];
    for(int i=0;i<=literals;i++){
        check_arr1[literals]=0;
        check_arr2[literals]=0;
    }

    int cl = clauses.size();
        for(int i=0;i<cl;i++)
        {
            for (auto pl=clauses[i].begin(); pl != clauses[i].end(); pl++)
            {
                int val = *pl;
                if(val>0){
                    check_arr1[-val]=1;
                }
                else if(val<0){
                    check_arr2[val]=-1;
                }
            }
        }

        for(int i=1;i<=literals;i++)
        {
            if(check_arr1[i]==1 &&check_arr2[i]==0){
                assignment.push_back(check_arr1[i]*1);
                remove_new_p(clauses,assignment);
            }
            else if(check_arr2[i]==-1&&check_arr1[i]==0){
                assignment.push_back(check_arr2[i]*(-1));
                remove_new_p(clauses,assignment);
            }
        }


    return;
}

void sort_ans(vector<int> &assignment, int literals){

    vector<int> store = assignment;
    assignment.resize(0);

    sort(store.begin(), store.end(), sorting);
    int counter= 0;
    for(int i=0; i<literals; i++){
        if (abs(store[counter]) == i){
            assignment.push_back(store[counter]);
            counter++;
        }
        else{
            assignment.push_back(i);
        }
    }
}

void print_ans(vector<int> &assignment, int literals){

    sort_ans(assignment,literals);

    for(int i=0;i<literals;i++){
        cout<< "v \" " << i+1 << " \" -> "<<(assignment[i]>0?"True":"False")<<endl;
    }
    cout<<"Done";
    return;
}

int DLIS(vector<set<int>> &clauses, int vnum){

    vector<pair<int, int>> cnt_literal(vnum + 1, {0, 0});
    int clause_cnt = clauses.size();
    for(int i=0; i<clause_cnt; i++){
        for(set<int> ::iterator it = clauses[i].begin(); it != clauses[i].end(); ++it){
            int num = *it;
            if (num < 0){
                cnt_literal[-1 * num].second += 1;
            }
            else{
                cnt_literal[num].first += 1;
            }
        }
    }

    int maxnum = -1;
    int maxv;
    for(int i=1; i<cnt_literal.size(); i++){
        if (maxnum < (cnt_literal[i].first + cnt_literal[i].second)){
            maxnum = cnt_literal[i].first + cnt_literal[i].second;
            maxv = i;
        }
    }


    if (cnt_literal[maxv].first >= cnt_literal[maxv].second){
        return maxv;
    }
    else {
        return -maxv;
    }
}


bool DPLL(vector<set<int>>clauses,vector<int> assignment,int new_p, int vnum){

    assignment.push_back(new_p);
    remove_new_p(clauses,assignment);
    unit_prop(clauses,assignment);
    pure_literal(clauses,assignment,vnum);
    if(clauses.size()==0){
        print_ans(assignment,vnum);
        return true;
    }
    if(check_empty_clause(clauses)==1){
        return false;
    }
    int  newp = DLIS(clauses,vnum);
    return DPLL(clauses, assignment,newp, vnum) || DPLL(clauses,assignment,-1*newp,vnum);
}



int main()
{
    string trash;
    string file;
    cout<<"Enter name of file: "<<endl;
    cin>>file;
    ifstream inputfile(file,ios::in);

    inputfile>>trash;
    inputfile>>trash;

    int cnum;
    int vnum;

    inputfile>> vnum;
    inputfile>>cnum;

    vector<set<int>> clauses(cnum);
    int num;
    for(int i=0;i<cnum;i++)
    {
        inputfile>>num;
        while(num!=0)
        {
            clauses[i].insert(num);
            inputfile>>num;
        }
    }
    vector<int> assignment;


    int  new_p = DLIS(clauses,vnum);
    bool answer =  DPLL(clauses, assignment,new_p, vnum) || DPLL(clauses,assignment,-new_p,vnum);
    if(answer){
        print_ans(assignment,vnum);
        cout<<"s SATISFIABLE"<<endl;
    }
    else
        cout<<"s UNSATISFIABLE"<<endl;
    return 0;
}