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;
                    ans[deleteliteral]=judge;
                    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]--;
            }
        }
    }
}
bool 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);
                        }
                    }
                }
            }
        }
    }
    for (int i=1; i<=clausenum; i++){
        if(clause[i][0]==0){
            if(literalnum[i]==0){
                return 0;
                break;
            }
        }
        if(i == clausenum)
            return 1;
    }
}
bool 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);
            }
        }
    }
    for (int i=1; i<=clausenum; i++){
        if(clause[i][0]==0){
            if(literalnum[i]==0){
                return 0;
                break;
            }
        }
        if(i == clausenum)
            return 1;
    }
}
int 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 (i==variablenum)
            return i;
    }
}
bool dpll(int value, int deleteliteral, vector<vector<int>> clause, vector<int> plusliteral, vector<int> minusliteral, vector<int> literalnum, int clausenum, int variablenum, vector<int> ans)
{
    if(deleteliteral!=0){
        deleting(value, deleteliteral,clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
    }
    bool clauseanswer=0, wronganswer=1;
    wronganswer = unit(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
    if (wronganswer==0)
        return 0;
    wronganswer = pure(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);
    if (wronganswer==0)
        return 0;
    deleteliteral = 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;
    }
    for (int i=1; i<=clausenum; i++){
        if(clause[i][0]==0){
            if(literalnum[i]==0){
                wronganswer=0;
                break;
            }
        }
        if(i == clausenum)
            return 1;
    }
    if (wronganswer == 0)
        return 0;
    else
        return dpll(0, deleteliteral, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans) || dpll(1, deleteliteral, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans);

}
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;

    ofstream outputfile(argv[2], ios::out);

    if (dpll(0, 0, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans)==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 if(dpll(0, 0, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans)==0){
        outputfile << "s UNSATISFIABLE";
    }
    return 0;
}