Untitled

#include <iostream>
#include <fstream>
#include <vector>
#include <algorithm>
#include <iomanip>
#include <cstdlib>
using namespace std;
// global variable
struct variable{
    int postimes; // positive variable's amount
    int negtimes; // negative variable's amount
};
int amount = 0; // variables amount
int clause = 0; // clauses amount

// deal with the clause that only has one element
void unit_propagation(vector<int> &temp_ans, vector <vector<int>> &temp_data)
{
    while (1) {

        //initialize key
        int key = 0;
        int negkey = 0;

        // find the operand for the unit propagation
        for (int i = 0; i < temp_data.size(); i++)
        {

            if (temp_data[i].size() == 1) // size==1 means only has one element
            {
                key = temp_data[i][0]; // assign the key as operand
                temp_ans.push_back(key); // save the answer into temperate answer
                negkey = -key; // assign a negkey as negtive operand
                break;
            }
        }

        // after size detect and key did not change
        if (key == 0)
            return;

        // find the correspond key
        for (int i = 0; i < temp_data.size(); i++)
            {
            for (int j = 0; j < temp_data[i].size(); j++)
            {
                if (temp_data[i][j] == key) // find the key and erase that row
                {
                    temp_data.erase(temp_data.begin() + i);
                    i = -1; // make it can check all row
                    break;
                }

                if (temp_data[i][j] == negkey) // find the -key and erase the element
                {
                    temp_data[i].erase(temp_data[i].begin() + j);
                    j = -1; // make it can check all element
                }
            }
        }
    }
    return;
}

// deal with all clause only has one variable state
void pure_literal_assign(vector<int> &temp_ans, vector <vector<int>> &temp_data)
{
    bool findpure = true; // find pure assign operand
    typedef struct variable Variables;
    Variables variables[amount + 1]; // in order to count the amount of variable

    while (findpure)
        {

        //initial
        for (int i = 0; i < amount + 1; i++)
        {
            variables[i].negtimes = 0;
            variables[i].postimes = 0;
        }

        findpure = false;

        //weight of variables
        for (int i = 0; i < temp_data.size(); i++)
        {
            for (int j = 0; j < temp_data[i].size(); j++)
            {
                if (temp_data[i][j] > 0) // temp_data is positve
                    variables[temp_data[i][j]].postimes++; // appear times++

                if (temp_data[i][j] < 0) // temp_data is negtive
                    variables[-(temp_data[i][j])].negtimes++; // appear times++
            }
        }


        for (int i = 1; i <= amount; i++)
        {
            if (variables[i].postimes == 0 && variables[i].negtimes != 0) // elements only appear one state(neg)
            {
                temp_ans.push_back(-i); // assign answer and save in temperate answer vector
                findpure = true; // whether find the pure literal assign operand

                // find the pure operand and erase that row
                for (int j = 0; j < temp_data.size(); j++)
                    {
                    for (int k = 0; k < temp_data[j].size(); k++)
                    {
                        if (temp_data[j][k] == -i)
                        {
                            temp_data.erase(temp_data.begin() + j);
                            j = -1;
                            break;
                        }
                    }

                }
            }

            if (variables[i].postimes != 0 && variables[i].negtimes == 0)// elements only appear one state(pos)
            {
                findpure = true;
                temp_ans.push_back(i);// assign answer and save in temperate answer vector

                // find the pure operand and erase that row
                for (int j = 0; j < temp_data.size(); j++)
                    {
                    for (int k = 0; k < temp_data[j].size(); k++)
                    {
                        if (temp_data[j][k] == i)
                        {
                            temp_data.erase(temp_data.begin() + j);
                            j = -1;
                            break;
                        }
                    }
                }
            }
        }
    }


}

//count the occurrence of variable and return a most weighted variable
int DLIS(vector <vector<int>>temp_data)
{
    int maxamount = -1; // most weighted variable's amount
    int maxvariable = 0; // most weighted variable 
    int pos_neg; // positive or negetive
    typedef struct variable Variables;
    Variables variables[amount + 1];
    
    
    for (int i = 0; i < amount + 1; i++)
    {
        variables[i].negtimes = 0;
        variables[i].postimes = 0;
    }

    //bool findpure = false;
    
     //weight of variables
    for (int i = 0; i < temp_data.size(); i++)
        {
        for (int j = 0; j < temp_data[i].size(); j++)
        {
            if (temp_data[i][j] > 0)
                variables[temp_data[i][j]].postimes++;// temp_data is positve

            if (temp_data[i][j] < 0)
                variables[-(temp_data[i][j])].negtimes++;// temp_data is negative
        }
    }
    
    // find the max amount variable 
    for (int i = 0; i <= amount; i++)
        {
        if (variables[i].negtimes > maxamount)
        {
            maxamount = variables[i].negtimes;
            maxvariable = i;
            pos_neg = -1;
        }

        if (variables[i].postimes > maxamount)
        {
            maxamount = variables[i].postimes;
            maxvariable = i;
            pos_neg = 1;
        }
    }

    if (pos_neg == -1)
        return -maxvariable; // negative
    else
        return maxvariable; // positive
}

// use recursion to run the upper function
bool DPLL(vector<vector<int>>temp_data, vector <int>temp_ans, int maxvariable, vector <int> &final_ans)
{
    //add a clause that only include maxvariable
    vector<int>v;
    v.push_back(maxvariable);
    temp_data.push_back(v);
    
    // run the upper function to simplify the clauses
    unit_propagation(temp_ans, temp_data);
    pure_literal_assign(temp_ans, temp_data);
    maxvariable = DLIS(temp_data);

    // temperate data is empty means that it has solution
    if (temp_data.empty()) {
        for (int i = 0; i < amount; i++) {
            final_ans = temp_ans;
            return true;
        }
    }

    // temperate clause is empty means that it has solution
    else if (temp_data.size() != 0) {
        for (int i = 0; i < temp_data.size(); i++)
            if (temp_data[i].size() == 0)
                return false;
    }
    
    // it did not satisfy because run the recursion
    return DPLL(temp_data, temp_ans, maxvariable, final_ans) ||
            DPLL(temp_data, temp_ans, -maxvariable, final_ans);
}

int main(int argc, char *argv[]) {
    
    // variable definition
    string inputfile = "in.txt";
    string outputfile = "out.txt";
    string unuse;
    ifstream infile(argv[1], ios::in);
    ofstream outfile(argv[2], ios::out);

    // ignore p and cnf
    infile >> unuse;
    infile >> unuse;

    // save variable amount and clause amount
    infile >> amount;
    infile >> clause;

    vector<vector<int>> temp_data(clause); // declare a temperature vector to save data
    int tempvariable;//use to push_back data

    //
    for (int i = 0; i < clause; i++) {
        infile >> tempvariable;

        while (tempvariable != 0) {
            temp_data[i].push_back(tempvariable);
            infile >> tempvariable;
        }
    }

    vector<int> temp_ans;
    vector<int> final_ans;
    int maxvariable;
    bool output;

    maxvariable = DLIS(temp_data);
    output = DPLL(temp_data, temp_ans, maxvariable, final_ans) ||
             DPLL(temp_data, temp_ans, -maxvariable, final_ans);

    if (output == true)
    {
        outfile << "s SATISFIABLE" << endl;
        bool finded;//whether finded value;

        for (int i = 1; i <= amount; i++) {
            finded = false;
            outfile << "v \" " << i << " \" -> " ;

            for (int j = 0; j < final_ans.size(); j++) {
                if (final_ans[j] == i) {
                    outfile << "True" << endl;
                    finded = true;
                } else if (final_ans[j] == -i) {
                    outfile << "False" << endl;
                    finded = true;
                }
            }

            if (finded == false)
                outfile << "True" << endl;
        }

        outfile << "Done" << endl;
    }
    else if (output == false)
        outfile << "s UNSATISFIABLE" << endl;


    return 0;
}