main.cpp

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

/*void print_clauses(vector<set<int>> &clauses){
    int rows = clauses.size();
    cout<<"START"<<endl;
    for(int i=0;i<rows;i++)
    {
        for (auto it=clauses[i].begin(); it != clauses[i].end(); ++it)
        {
            cout<<*it<<" ";
        }
        cout<<endl;
    }
    cout<<"END"<<endl;
    return;
}*/

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 uph=1;
    while(uph==1){
        uph=0;
        int rows = clauses.size();
        for(int i=0;i<rows;i++){
            if(clauses[i].size()==1){
                uph=1;
                set<int>::iterator it = clauses[i].begin();
                assignment.push_back(*it);
                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];
    int cl = clauses.size();

       for(int i=0;i<=literals;i++){
        check_arr1[literals]=0;
        check_arr2[literals]=0;
        }
        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> &an, int literals){

    vector<int> store = an;
    an.resize(0);
    sort(store.begin(), store.end(), [](int a, int b){return abs(a) <= abs(b);});
    cout<<"start"<<endl;
    for(int i=0;i<store.size();i++){
            cout<<store[i]<<endl;
        }
    cout<<"end" <<endl;
    int counter= 0;
    for(int i=1; i<=literals; i++){
        int flag=0;
        for(int counter=1;counter<=literals;counter++){
            if(i==abs(store[counter])){
                flag=1;
                an.push_back(store[counter]);
            }
        }
        if(flag==0){
            an.push_back(i);
        }
    }
    for(int i=0;i<an.size();i++){
            cout<<an[i]<<endl;
        }
}

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

    sort_ans(an,literals);


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

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

    vector<pair<int, int>> cnt(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[num].first ++;
            }
            else if(num<0){
                cnt[-num].second ++ ;
            }
        }
    }

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


    if (cnt[maxv].first >= cnt[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);
    //print_clauses(clauses);
    unit_prop(clauses,assignment);
    //print_clauses(clauses);
    pure_literal(clauses,assignment,vnum);
    //print_clauses(clauses);
    if(clauses.size()==0){
        for(int i=0;i<assignment.size();i++){
            cout<<assignment[i]<<endl;
        }
        cout<<"s SATISFIABLE"<<endl;
        print_ans(assignment,vnum);
        return true;
    }
    if(check_empty_clause(clauses)){
        cout<<"s UNSATISFIABLE"<<endl;
        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;
    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;
        }
    }
    //print_clauses(clauses);

    vector<int> assignment;

    int  new_p = DLIS(clauses,vnum);
    if(!DPLL(clauses, assignment,new_p, vnum)){
        assignment.pop_back();
        DPLL(clauses,assignment,-new_p,vnum);
    }


    return 0;
}