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)
{
    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;
                    minusliteral[deleteliteral]=0;
                    plusliteral[deleteliteral]=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)
{
    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){
                        if(ans[j]==2){
                            ans[j]=1;
                            deleting(1, j, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
                        }
                    }
                    else if(clause[i][j]==0){
                        if(ans[j]==2){
                            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)
{
    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)
{
    int most=0, mostliteral=0;

    for(int i=1; i<=variablenum; i++){
        if(plusliteral[i]+minusliteral[i]>most){
            if(ans[i]==2){
                most = plusliteral[i]+minusliteral[i];
                mostliteral = i;
            }
        }
    }
    if(mostliteral!=0){
        if(plusliteral[mostliteral]>minusliteral[mostliteral]){
            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;
}
void dpll(vector<vector<int>> clause, vector<int> plusliteral, vector<int> minusliteral, vector<int> literalnum, int clausenum, int variablenum, vector<int> ans, char *argv)
{
    bool endfunction=0, clauseanswer=0;
    unit(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);

    for (int i=1; i<=clauseanswer; i++){
        if(literalnum[i]==0)
            clause[i][0]=1;
    }
    for (int i=1; i<=clausenum; i++){
        if(clause[i][0]==0){
            clauseanswer=0;
            break;
        }
        if(i==clausenum)
            clauseanswer=1;
    }
    if(clauseanswer==0)
        pure(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);

    for (int i=1; i<=clauseanswer; i++){
        if(literalnum[i]==0)
            clause[i][0]=1;
    }
    for (int i=1; i<=clausenum; i++){
        if(clause[i][0]==0){
            clauseanswer=0;
            break;
        }
        if(i==clausenum)
            clauseanswer=1;
    }
    if (clauseanswer==0)
        endfunction = dlis(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);

    for (int i=1; i<=clauseanswer; i++){
        if(literalnum[i]==0)
            clause[i][0]=1;
    }
    for (int i=1; i<=clausenum; i++){
        if(clause[i][0]==0){
            clauseanswer=0;
            break;
        }
        if(i==clausenum)
            clauseanswer=1;
    }
    if(clauseanswer==0 && endfunction==1)
        dpll(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans, argv);

    else {
        ofstream outputfile(argv, ios::out);

        if(clauseanswer==1){
            outputfile << "s SATISFIABLE"<<endl;
            for(int i=1; i<=variablenum; i++){
                outputfile << "v “ "<<i<< " ” -> ";
                if(ans[i]==0)
                    outputfile << "False"<<endl;
                else
                    outputfile << "True"<< endl;
            }
            outputfile << "Done";
        }
        else
            outputfile << "s UNSATISFIABLE";
    }
}
int main(int argc, char *argv[])
{
    char p;
    string cnf;
    int inputnum, variablenum, clausenum, counter=1;

    ifstream inputfile(argv[1], 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;

    dpll(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans, argv[2]);
    return 0;
}