Untitled

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


void unit_propagation(vector<int>&temp_ans,vector <vector<int>>&temp_data)
{
    while(1)
    {
        int key=0;
        int negkey=0;
        for(int i=0;i<temp_data.size();i++)
        {
            if(temp_data[i].size()==1)
            {
                key=temp_data[i][0];
                temp_ans.push_back(key);
                negkey=-key;
                break;
            }
        }

        if(key==0)
            return;

        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)
                {
                    temp_data.erase(temp_data.begin() + i);
                    i=-1;
                    break;
                }

                if(temp_data[i][j]==negkey)
                {
                    temp_data[i].erase(temp_data[i].begin() + j);
                    j=-1;
                }
            }
        }
    }

    return;
}


void pure_literal_assign(vector<int>&temp_ans,vector <vector<int>>&temp_data)
{
   bool findpure=true;
   typedef struct variable Variables;
   Variables variables[amount+1];
    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)
                        variables[temp_data[i][j]].postimes++;
                    if(temp_data[i][j]<0)
                        variables[-(temp_data[i][j])].negtimes++;
            }
        }

        for(int i=1;i<=amount;i++)
        {
            if(variables[i].postimes==0&&variables[i].negtimes!=0)
            {
                temp_ans.push_back(-i);
                findpure=true;
                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)
            {
                findpure=true;
                temp_ans.push_back(i);
                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;
                        }
                    }
               }
            }
        }
    }


}

int DLIS(vector <vector<int>>temp_data)
{
    int maxamount=-1;
    int maxvariable=0;
    int pos_neg;
    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;
        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++;
                    if(temp_data[i][j]<0)
                        variables[-(temp_data[i][j])].negtimes++;
            }
        }

        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;
        else
            return maxvariable;
}

bool DPLL(vector<vector<int>>temp_data,vector <int>temp_ans,int maxvariable,vector <int> &final_ans)
{
    vector<int>v;
    v.push_back(maxvariable);
    temp_data.push_back(v);
    unit_propagation(temp_ans,temp_data);
    pure_literal_assign(temp_ans,temp_data);
    maxvariable=DLIS(temp_data);

    if(temp_data.empty())
    {
        for(int i=0;i<amount;i++)
        {
            final_ans=temp_ans;
            return true;
        }
    }

    else if(temp_data.size()!=0)
    {
        for(int i=0;i<temp_data.size();i++)
                if(temp_data[i].size()==0)
                    return false;
    }
    return DPLL(temp_data,temp_ans,maxvariable,final_ans)||DPLL(temp_data,temp_ans,-maxvariable,final_ans);
}

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

    if(!infile)
        cerr << "File can not be opened.";

    infile >> unuse;
    infile >> unuse;

    infile >> amount;
    infile >> clause;
    vector<vector<int>> temp_data(clause);
    int tempvariable;

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