Untitled

#include <iostream>
#include <fstream>
#include <vector>

using namespace std;
void deleting(int judge,int deleteliteral, vector<vector<int>> &clause, vector<int> &plusliteral, vector<int> &minusliteral, vector<int> &literalnum, int clausenum, int variablenum, vector<int> &ans)
{
    cout << "delete" << endl;
    for(int i=1; i<=clausenum; i++){
        if(clause[i][0]==0){
            if(clause[i][deleteliteral]!=2){
                if(clause[i][deleteliteral]==judge){
                    clause[i][0]=1;
                    literalnum[i]=0;
                    for(int k=1; k<=variablenum; k++){
                        if(clause[i][k]==0)
                            minusliteral[k]--;
                        else if(clause[i][k]==1)
                            plusliteral[k]--;
                    }
                }
                else
                    literalnum[i]--;
            }
        }
    }
}
void unit(vector<vector<int>> &clause, vector<int> &plusliteral, vector<int> &minusliteral, vector<int> &literalnum, int clausenum, int variablenum, vector<int> &ans)
{
    cout << "unit" << endl;
    for (int i=1; i<=clausenum; i++){
        if(clause[i][0]==0){
            if(literalnum[i]==1){
                for(int j=1; j<=variablenum; j++){
                    if(clause[i][j]==1){
                        ans[j]=1;
                        deleting(1, j, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
                    }
                    else if(clause[i][j]==0){
                        ans[j]=0;
                        deleting(0, j,clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
                    }
                }
            }
        }
    }
}
void pure(vector<vector<int>> &clause, vector<int> &plusliteral, vector<int> &minusliteral, vector<int> &literalnum, int clausenum, int variablenum, vector<int> &ans)
{
    cout << "pure"<<endl;
    for(int i=1; i<=variablenum; i++){
        if(plusliteral[i]>0 && minusliteral[i]==0){
            if(ans[i]==2){
                ans[i]=1;
                deleting(1, i, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
            }
        }
        else if(plusliteral[i]==0 && minusliteral[i]>0){
            if(ans[i]==2){
                ans[i]=0;
                deleting(0, i, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
            }
        }
    }
}
bool dlis(vector<vector<int>> &clause, vector<int> &plusliteral, vector<int> &minusliteral, vector<int> &literalnum, int clausenum, int variablenum, vector<int> &ans)
{
    cout << "dlis"<<endl;
    int most=0, mostliteral=0;

    for(int i=1; i<=variablenum; i++){
        if(plusliteral[i]>most){
            most = plusliteral[i];
            mostliteral = i;
        }
        if(minusliteral[i]>most){
            most = minusliteral[i];
            mostliteral = i;
        }
    }
    cout << mostliteral<<endl;
    cout << ans[mostliteral]<< endl;
    if(mostliteral!=0){
        if(mostliteral>0){
            if(ans[mostliteral]==2){
                ans[mostliteral]=1;
                deleting(1, mostliteral, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
            }
        }
        else{
            if(ans[-mostliteral]==2){
                ans[-mostliteral]=0;
                deleting(0, mostliteral, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
            }
        }
        return 1;
    }
    else
        return 0;
}
bool dpll(vector<vector<int>> &clause, vector<int> &plusliteral, vector<int> &minusliteral, vector<int> &literalnum, int clausenum, int variablenum, vector<int> &ans)
{
    cout << "dpll"<<endl;
    bool endfunction, clauseanswer;
    unit(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
    pure(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
    endfunction = dlis(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);

    for (int i=1; i<=clausenum; i++){
        if(clause[i][0]==0){
            clauseanswer=0;
            break;
        }
        if(i==clausenum)
            clauseanswer=1;
    }
    if(clauseanswer==1)
        return 1;
    else if(clauseanswer==0 && endfunction==1)
        dpll(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
    else
        return 0;
}
int main()
{
    char p;
    string cnf;
    string file;
    int inputnum, variablenum, clausenum, counter=1;

    cin >> file;
    ifstream inputfile(file, ios::in);
    inputfile >> p >> cnf >> variablenum >> clausenum;

    vector <vector<int>>clause(clausenum+1, vector<int>(variablenum+1));

    for (int i=0; i<=clausenum; i++){
        for (int j=0; j<=variablenum; j++){
            clause[i][j]=2;
        }
    }

    for (int i=0; i<=clausenum; i++)
        clause[i][0]=0;

    //this array caculate the number of literal in each clauses
    vector <int>literalnum(clausenum+1);
    for (int i=0; i<=clausenum; i++)
        literalnum[i]=0;

    vector <int>plusliteral(variablenum+1);
    vector <int>minusliteral(variablenum+1);
    for (int i=0; i<=variablenum; i++){
        plusliteral[i]=0;
        minusliteral[i]=0;
    }

    //store file into array
    while (inputfile >> inputnum){
        for (int i=1; i<=variablenum; i++){
            if (inputnum==i){
                clause[counter][i]=1;
                literalnum[counter]++;
                plusliteral[i]++;
            }
            else if(inputnum==-i){
                clause[counter][i]=0;
                minusliteral[i]++;
                literalnum[counter]++;
            }
        }
        if (inputnum==0)
            counter ++;
        if (counter > clausenum)
            break;
    }

    //set ans array
    vector <int>ans(variablenum+1);
    for(int i=0; i<=variablenum; i++)
        ans[i]=2;

    bool answerchoice;
    answerchoice = dpll(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);

    if (answerchoice==0){
        cout << "s UNSATISFIABLE";
    }
    else if (answerchoice==1){
        cout << "s SATISFIABLE"<<endl;
        for(int i=1; i<=variablenum; i++){
            cout << "v “ "<<i<< " ” -> ";
            if(ans[i]==0)
                cout << "False"<<endl;
            else
                cout << "True"<< endl;
        }
        cout << "Done";
    }


    return 0;
}