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)
{
    ans[deleteliteral]=judge;
    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]--;
                            clause[i][k]=2;
                        }
                        else if(clause[i][k]==1){
                            plusliteral[k]--;
                            clause[i][k]=2;
                        }
                    }
                }
                else
                    literalnum[i]--;
            }
        }
        minusliteral[deleteliteral]=0;
        plusliteral[deleteliteral]=0;
    }
}
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;
            }
        }
    }
    return mostliteral;
}
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, char *argv)
{

    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){
            ofstream outputfile(argv, ios::out);

            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";
            return 1;
        }
    }
    if (wronganswer == 0)
        return 0;
    else
        return dpll(0, deleteliteral, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans, argv) || dpll(1, deleteliteral, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans, argv);
}
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;

    if(dpll(0, 0, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans, argv[2])==0){
        ofstream outputfile(argv[2], ios::out);

        outputfile << "s UNSATISFIABLE";
    }
    return 0;
}