Untitled

#include <iostream>
#include <fstream>
#include<string>
#include<cstdlib>
#include<cmath>
using namespace std;


enum TYPE
{
    UNASSIGNED = 0,
    NOPRIME = 1,
    PRIME = 2,
    DONTCARE = 3
};

void update_input(TYPE **input, bool *phi, int variable, bool decision, int num_v, int num_c){

    for(int i=0;i<num_c;++i){
        if(!phi[i]){
            if(input[variable][i] == NOPRIME){
                if(decision){
                    phi[i] = true;
                    for(int j=0;j<num_v;++j)
                    {
                        input[j][i]=UNASSIGNED;
                    }
                }
                else{
                    input[variable][i] = UNASSIGNED;
                }
            }
            else if(input[variable][i] == PRIME){
                if(decision){
                    input[variable][i] = UNASSIGNED;
                }
                else{
                    phi[i] = true;
                    for(int j=0;j<num_v;++j)
                    {
                        input[j][i]=UNASSIGNED;
                    }
                }
            }
        }
    }
}

//Unit propagation
void unit_propagation(TYPE **input,bool *phi,bool*answer1,bool*answer2, int num_v,int  num_c)
{
    int count,variable,clause;
    for(int i=0;i<num_c;i++)
    {
        if(!phi[i])
        {
            count = 0;
            for(int j=0;j<num_v;j++)
            {
                if(input[j][i] != UNASSIGNED)
                {
                    count++;
                    variable = j;
                    clause = i;
                }
                if(count == 2)
                {
                    break;
                }

            }
            if(count == 1)
            {
                //assign value to input[variable]
                answer1[variable] = true;
                if(input[variable][clause] == NOPRIME)
                {
                    answer2[variable] = true;
                    update_input(input,phi,variable,true,num_v,num_c);
                }
                else
                {
                    answer2[variable] = false;
                    update_input(input,phi,variable,false,num_v,num_c);
                }
                unit_propagation(input, phi, answer1,answer2, num_v, num_c);
                return;
            }
        }

    }
}

//Pure Literal Assign
void pure_literal_assign(TYPE **input,int variable_num,bool *phi,bool *answer1,bool *answer2,int clause_num)
{
    bool noprime;
    bool prime;
    for(int i=0;i<variable_num;i++)
    {
        if(!answer1[i])
        {
            noprime = prime = true;
            for(int j=0;j<clause_num;j++)
            {
                if(input[i][j] == NOPRIME){
                    prime = false;
                }
                else if(input[i][j] == PRIME){
                    noprime = false;
                }
                if(!(noprime || prime)){
                    continue;
                }
                if(j == clause_num-1){
                    answer1[i]=true;
                    if(prime&&noprime)
                    {
                        ;
                    }
                    else if(prime){
                        answer2[i]=false;
                        update_input(input,phi,i,false,variable_num,clause_num);
                    }
                    else if(noprime){
                        answer2[i]=true;
                        update_input(input,phi,i,true,variable_num,clause_num);
                    }
                    pure_literal_assign(input,variable_num,phi,answer1,answer2,clause_num);
                    return;
                }
            }
        }
    }
}

bool phi_is_empty(bool *phi, int num_c)
{
    for(int i=0;i<num_c;++i)
    {
        if(!phi[i])
        {
            return false;
        }
    }
    return true;
}

bool containing_empty_clause(TYPE **input,bool *phi, int num_v, int num_c)
{
    bool lala;
    for(int i=0;i<num_c;++i){
        if(!phi[i]){
            lala = true;
            for(int j=0;j<num_v;++j){
                if(input[j][i] != UNASSIGNED){
                    lala = false;
                    break;
                }
            }
            if(lala){
                return true;
            }
        }
    }
    return false;
}

int choose_a_literal(bool*answer1, int num_v)
{
    for(int i=0;i<num_v;++i)
    {
        if(!answer1[i])
        {
            return i+1;
        }
    }
    return 0;
}

//use a recurtion function
bool DPLL(TYPE **input, bool *answer1, bool *answer2, bool *phi, int num_v, int num_c, int literal)
{

    TYPE** input_1 = new TYPE*[num_v];
    bool* answer1_1 = new bool[num_v];
    bool* phi_1 = new bool[num_c];
    for(int i = 0; i < num_v; ++i)
    {
        input_1[i] = new TYPE[num_c];
    }
    for(int i=0;i<num_v;++i)
    {
        for(int j=0;j<num_c;++j)
        {
            input_1[i][j] = input[i][j];
        }
        answer1_1[i] = answer1[i];
    }
    for(int i=0;i<num_c;++i){
        phi_1[i] = phi[i];
    }

    if(literal != 0)
    {
        int y = abs(literal) - 1;
        answer1[y] = true;
        answer2[y] = (literal > 0);
        update_input(input, phi, y, (literal > 0), num_v, num_c);
    }

    unit_propagation(input, phi, answer1, answer2, num_v, num_c);
    pure_literal_assign(input, num_v, phi, answer1, answer2, num_c);

    if(phi_is_empty(phi, num_c))
    {
        for(int i = 0; i < num_v; ++i)
        {
            delete[] input_1[i];
        }
        delete[] input_1;
        delete[] answer1_1;
        delete[] phi_1;

        return true;
    }
    if(containing_empty_clause(input, phi, num_v, num_c))
    {
        for(int i=0;i<num_v;++i)
        {
            for(int j=0;j<num_c;++j)
            {
                input[i][j] = input_1[i][j];
            }
            answer1[i] = answer1_1[i];
        }
        for(int i=0;i<num_c;++i){
            phi[i] = phi_1[i];
        }
        for(int i = 0; i < num_v; ++i)
        {
            delete[] input_1[i];
        }
        delete[] input_1;
        delete[] answer1_1;
        delete[] phi_1;

        return false;
    }

    int lit = choose_a_literal(answer1, num_v);
    if(!(DPLL(input, answer1, answer2, phi, num_v, num_c, lit) || DPLL(input, answer1, answer2, phi, num_v, num_c, -lit)))
    {
        for(int i=0;i<num_v;++i)
        {
            for(int j=0;j<num_c;++j)
            {
                input[i][j] = input_1[i][j];
            }
            answer1[i] = answer1_1[i];
        }
        for(int i=0;i<num_c;++i){
            phi[i] = phi_1[i];
        }
        for(int i = 0; i < num_v; ++i)
        {
            delete[] input_1[i];
        }
        delete[] input_1;
        delete[] answer1_1;
        delete[] phi_1;

        return false;
    }

    for(int i = 0; i < num_v; ++i)
    {
        delete[] input_1[i];
    }
    delete[] input_1;
    delete[] answer1_1;
    delete[] phi_1;

    return true;
}

void input_file(char *argv,TYPE **input,bool *phi,bool *answer1,bool *answer2,int num_of_clause,int num_of_variable,istream &infile)
{

    int x,y;
    for(int i=0;i<num_of_clause;++i)
    {
        cin >> x;
        while(x != 0)
        {
            y= abs(x)-1;
            if(input[y][i] == UNASSIGNED)
            {
             input[y][i] = (x > 0 ? NOPRIME : PRIME);
            }
            else if(input[y][i] == NOPRIME)
            {
                if(x < 0)
                {
                 input[y][i] = DONTCARE;
                }
            }
            else if(input[y][i] == PRIME)
            {
                if(x > 0)
                {
                 input[y][i] = DONTCARE;
                }
            }
            cin >> x;
        }
    }
}

void output_file(char *argv,bool *answer1, bool *answer2,int num_of_variable,bool result)
{
   ofstream outfile(argv,ios::out);
   if(result)
   {
        cout<<"s SATISFIABLE"<<endl;
        for(int i=0;i<num_of_variable;i++)
        {
         cout<<"v \" "<<i+1<<" \" -> "<<(answer2[i] ? "True":"False")<<endl;
        }
        cout<<"Done";
        return;

   }
   else
   {
       cout<<"s UNSATISFIABLE";
       return;
   }
}

int main(int agrc,char*argv[])
{

    ifstream infile(argv[1],ios::in);
    int num_of_variable,num_of_clause ;
    string trash;
    infile>>trash>>trash;
    infile>>num_of_variable;
    infile>>num_of_clause;
    bool result;
    TYPE** input = new TYPE*[num_of_variable];
    for (int i = 0; i < num_of_variable; ++i)
    {
        input[i] = new TYPE[num_of_clause]{UNASSIGNED};
    }

    bool phi[num_of_clause];
    for(int i=0;i<num_of_clause;++i){
        phi[i] = false;
    }
    bool answer1[num_of_variable];                 //check if assigned value
    bool answer2[num_of_variable];                 //the real value
    for(int i=0;i<num_of_variable;++i){
        answer1[i] = false;
        answer2[i] = false;
    }

    input_file(argv[1],input,phi,answer1,answer2,num_of_clause,num_of_variable,infile);                   /////////////////////////////////////////////////////////////

    for(int i=0;i<num_of_clause;++i){
        for(int j=0;j<num_of_variable;++j){
            if(input[j][i] == DONTCARE){
                phi[i] = true;
                 for(int j=0;j<num_of_variable;++j)
                    {
                        input[j][i]=UNASSIGNED;
                    }
                break;
            }
        }
    }

    result=DPLL(input, answer1, answer2, phi, num_of_variable, num_of_clause, 0);
    output_file(argv[2],answer1,answer2,num_of_variable,result);                                   ///////////////////////////////////////////////////////

    for(int i = 0; i < num_of_variable; ++i)
    {
        delete[] input[i];
    }
    delete[] input;
}