main.cpp

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


int check_empty_clause(vector<set<int>> &clauses){
    int rows = clauses.size();
    for(int i=0;i<rows;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--;
        }
        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();
                clauses.erase(clauses.begin()+i);
                assignment.push_back(*it);
                remove_new_p(clauses,assignment);
                break;
            }
        }
    }
    return;
}

void pure_literal(vector<set<int>> &clauses, vector<int> &assignment, int literals){
    vector<int> check(literals+1, 0);
    int curr_rows = clauses.size();
    for(int i=0;i<curr_rows;i++)
    {
        for (auto it=clauses[i].begin(); it != clauses[i].end(); ++it)
        {
            int val = *it;
            if(val<0){
                if(check[-1*val]==1)
                    check[-1*val]=2;
                else if(check[-1*val]==0)
                    check[-1*val]=-1;
                else if(check[-1*val]==2)
                    check[-1*val]=2;
            }
            else{
                if(check[val]==-1)
                    check[val]=2;
                else if(check[val]==0)
                    check[val]=1;
                else if(check[val]==2)
                    check[val]=2;
            }
        }
    }
    for(int i=1;i<=literals;i++)
    {
        if(check[i]==1 || check[i]==-1){
            assignment.push_back(check[i]*i);
            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(), [](int a, int b){return abs(a) < abs(b);});
    int counter= 0;
    for(int i=1; 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){
    int size = assignment.size();

    sort_ans(assignment,literals);

    vector<int> solution(literals+1,1);
    for(int i=1;i<=literals;i++){
        cout<< "v \" " << i << " \" -> "<<(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 -1 * maxv;
    }
}


bool DPLL_algo(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_algo(clauses, assignment,newp, vnum) || DPLL_algo(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;

    unit_prop(clauses,assignment);
    pure_literal(clauses,assignment,vnum);
    if(clauses.size()==0){
        print_ans(assignment,vnum);
        cout<<"s SATISFIABLE"<<endl;
        return 0;
    }
    if(check_empty_clause(clauses)==1){
        cout<<"s UNSATISFIABLE"<<endl;
        return 0;
    }
    int  new_p = DLIS(clauses,vnum);
    bool answer =  DPLL_algo(clauses, assignment,new_p, vnum) || DPLL_algo(clauses,assignment,-1*new_p,vnum);
    if(answer){
        print_ans(assignment,vnum);
        cout<<"s SATISFIABLE"<<endl;
    }
    else
        cout<<"s UNSATISFIABLE"<<endl;
    return 0;
}