main.cpp

#include <bits/stdc++.h>
#include <fstream>
#include <cstdlib>

using namespace std;


void remove_v(vector<vector<int>>& clauses,vector<int>& assignment){

    int literal=assignment.back();
    int cl=clauses.size();
    for(int i=1;i<=cl;i++){
        for(int j=0;j<clauses[i].size();j++){
            if(clauses[i][j]==literal){
                clauses.erase(clauses.begin()+i);
                i--;
                j=0;
            }
            else if(clauses[i][j]==-literal){
                clauses[i].erase(clauses[i].begin()+j);
            }
        }
    }
    return;
}
int check(vector<vector<int>>& clauses){
    int checker=clauses.size();
    for(int i=1;i<=checker;i++){
        if(clauses[i].size()==0)
            return 1;
    }
    return 0;
}

void unit_prop(vector<vector<int>>& clauses,vector<int> assignment) {
    int up_h = 1;
    int cl=clauses.size();
    while (up_h) {
        up_h = 0;
        for (int i = 1; i <= cl; i++) {
            if (clauses[i].size() == 1) {
                up_h = 1;
                assignment.push_back(clauses[i][0]);
                clauses.erase(clauses.begin()+i);
                remove_v(clauses, assignment);
                break;
            }
        }
    }
}


void pure_literal(vector<vector<int>>& clauses ,vector<int> assignment,int vnum) {

        vector<pair<int, int>> checker(vnum+1, {0,0});
        int cl=clauses.size();

        for(int i=1; i <= cl; i++){
            for(int j=0;j < clauses[i].size();j++){
                int num = clauses[i][j];
                if (num < 0){
                    checker[-1*num].second = 1;
                }
                else{
                    checker[num].first = 1;
                }
            }
        }

        for(int i=1; i<=vnum; i++)
        {
            if(checker[i].first == 1 && checker[i].second == 0 ){
                assignment.push_back(i);
                remove_v(clauses,assignment);
            }
            else if (checker[i].first == 0 && checker[i].second == 1){
                assignment.push_back(-i);
                remove_v(clauses,assignment);
            }
        }

}

int DLIS(vector<vector<int>>& clauses, int vnum) {
    int maxv = -1, selectv = -1, literals, variable;
    int count_arr1[vnum + 1] = {0};
    int count_arr2[vnum + 1] = {0};
    int cl=clauses.size();

    for (int i = 1; i <= cl; i++) {
        for(int j=0;j<clauses[i].size();j++) {
            literals = clauses[i][j];
            variable = abs(literals);
            if(literals > 0)
                count_arr1[variable]++;
            else
                count_arr2[variable]++;
        }
    }

    for (int i = 1; i <= vnum; i++) {
        if (count_arr1[i] + count_arr2[i] > maxv ) {
            maxv = count_arr1[i] + count_arr2[i];
            selectv = i;
        }
    }
    if(count_arr1[selectv] >= count_arr2[selectv])
        return selectv;
    else
        return -1 * selectv;
}

bool DPLL( vector<vector<int>>& clauses,vector<int> assignment,int next, const int vnum) {

    assignment.push_back(next);
    remove_v(clauses,assignment);
    unit_prop(clauses, assignment);
    pure_literal(clauses, assignment , vnum );

    if(clauses.size()==0){
        return true;
    }

    if(check(clauses)==1){
        return false;
    }
    int newone = DLIS(clauses,vnum);
    return DPLL(clauses, assignment,newone, vnum) || DPLL(clauses,assignment,-1*newone,vnum);

}
void print_ans(vector<int> &assignment, int vnum){
    int size = assignment.size();
    vector<int> solution(vnum+1,1);
    for(int i=0;i<size;i++)
    {
        int val = assignment[i];
        if(val<0)
        {
            solution[val*-1]=-1;
        }
    }
    for(int i=1;i<=vnum;i++)
    {
        cout<<solution[i]<<endl;
    }
    cout<<endl;
    return;
}


int main() {
    int vnum, cnum;

    string trash;

    string filename;
    cin >> filename;
    ifstream inputfile(filename, ios::in);


    inputfile>>trash;
    inputfile>>trash;
    inputfile>>vnum;
    inputfile>>cnum;

    vector<vector<int>> clauses;

    for(int i=0;i<cnum+1;i++){
        clauses.push_back(vector<int>(0));
    }

    for(int i=1 ; i<=cnum ; i++){
        int x;
        inputfile >> x;
        while(x != 0){
            clauses[i].push_back(x);
            inputfile >> x;
        }
    }

    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(clauses)==1){
        cout<<"s UNSATISFIABLE"<<endl;
        return 0;
    }

    int  newone= DLIS(clauses,vnum);
    bool ans =  DPLL(clauses, assignment,newone, vnum) || DPLL(clauses,assignment,-1*newone,vnum);
    if(ans){
        cout<<"s SATISFIABLE"<<endl;
        print_ans(assignment,vnum);
    }

    else
        cout<<"s UNSATISFIABLE"<<endl;

    return 0;
}