Untitled

#include <iostream>
#include <sstream>
#include <vector>
#include <algorithm>
#include <cstdlib>

using namespace std;

typedef struct pos_neg{
    int num_pos=0;
    int num_neg=0;
    bool tof;
};

bool DPLL(vector<vector<int>>, int, vector<vector<int>>&, vector<pos_neg>);
void UnitPropagation(vector<vector<int>>&, vector<pos_neg>&);
void PureLiteralElimination(vector<vector<int>>&, vector<pos_neg>&);
void remove_literal(vector<vector<int>>&, vector<pos_neg>&);
bool whether_have_variable(vector<vector<int>>&);
void print(vector<vector<int>>&);
int DLIS(vector<vector<int>>&);
int num_variable;

int main()
{
    string s1, s2, input;
    cin>>s1>>s2;

    while(s1!="p" || s2!="cnf"){
        s1=s2;
        cin>>s2;
    }

    int clause;
    cin>>num_variable>>clause;
    vector<int> info;
    vector<vector<int>>clauses;//原資料的複製，對他做改動
    vector<vector<int>>clause_c;//原資料
    vector<pos_neg>pn;//儲存已賦的值
    pn.resize(num_variable+1);

    while(getline(cin, input))
    {
        info.clear();
        istringstream iss(input);
        int variable;
        while(iss>>variable)
        {
            if(variable!=0)
                info.push_back(variable);
        }
        clause_c.push_back(info);
        if(input=="0")
           break;
    }

    clauses=clause_c;

    bool sat;

    UnitPropagation(clauses, pn);
    PureLiteralElimination(clauses, pn);

    if(clauses.empty())
    {
        sat=true;
        cout<<"kkk"<<endl;
    }
    if(whether_have_variable(clauses))
    {
        sat=false;
        cout<<"bbb"<<endl;
    }

    int chosen_main=DLIS(clauses);

    sat=DPLL(clauses, chosen_main, clause_c, pn)||DPLL(clauses, chosen_main*(-1), clause_c, pn);

    if(sat==true)
    {
        cout<<"s SATISFIABLE"<<endl;
        for(int i=1 ; i<num_variable+1; i++)
        {
            if(pn[i].tof==true)
                cout<<"v “ "<<i<<" ” -> True"<<endl;
            else if(pn[i].tof==false)
                cout<<"v “ "<<i<<" ” -> False"<<endl;
        }
        cout<<"DONE"<<endl;
    }

    else if(sat==false)
        cout<<"s UNSATISFIABLE"<<endl;

    //輸出測試
    for (int i = 0; i < clauses.size(); i++) {
        for (int j = 0; j < clauses[i].size(); j++)
            cout << clauses[i][j] << " ";
        cout << endl;
    }
    for (int i = 0; i < clause_c.size(); i++) {
        for (int j = 0; j < clause_c[i].size(); j++)
            cout << clause_c[i][j] << " ";
        cout << endl;
    }
    return 0;
}

//判斷clauses中是否為空，如clasuse中無任何元素return true，otherwise return false
bool whether_have_variable(vector<vector<int>>& clauses)
{
    for(int i=0; i<clauses.size(); i++)
    {
        if(clauses[i].size()==0)
            return true;
    }
    return false;
}

//DPLL algorithm
bool DPLL(vector<vector<int>>clauses, int chosen, vector<vector<int>>& clause_c, vector<pos_neg> pn)
{
    clauses.push_back({chosen});
    remove_literal(clauses, pn);
    UnitPropagation(clauses, pn);
    PureLiteralElimination(clauses, pn);

    if(clauses.empty())
    {
        cout<<"kkkkkk"<<endl;
        clause_c=clauses;
        return true;
    }
    if(whether_have_variable(clauses))
    {
        cout<<"aaaaaaa"<<endl;
        return false;
    }

    int chosen_DPLL=DLIS(clauses);
    print (clauses);
    return DPLL(clauses, chosen_DPLL, clause_c, pn)||DPLL(clauses, chosen_DPLL*(-1), clause_c, pn);
}

void print(vector<vector<int>>& clauses)
{
    for(int i=0; i<clauses.size(); i++)
    {
        for(int j=0; j<clauses[i].size(); j++)
            cout<<clauses[i][j]<<" ";
        cout<<endl;
    }
}

//刪除clauses or literal
void remove_literal(vector<vector<int>>& clauses, vector<pos_neg>& pn)
{
    int new_literal;
    if(clauses.size()>0)
    {
        new_literal=clauses[clauses.size()-1][0];
        cout<<new_literal<<"qqqqq"<<endl;
    }

    //刪除含new_literal的clause
    for(int i=0; i<clauses.size();i++)
    {
        int length1=clauses[i].size();
        for(int j=0; j<length1;)
        {
            if(clauses[i][j]==new_literal)
            {
                clauses.erase(clauses.begin()+i);
                i=-1;
                break;
            }
            else
                j++;
        }
    }

    //刪除相反unit literal
    for(int i=0; i<clauses.size();)
    {
        int length1=clauses[i].size();
        for(int j=0; j<length1;j++)
        {
            if(clauses[i][j]==-new_literal)
            {
                clauses[i].erase(clauses[i].begin()+j);
                j=-1;
                break;
            }

        }
        i++;
    }
}

void UnitPropagation(vector<vector<int>>& clauses, vector<pos_neg>& pn)
{
    while(true)
    {
        int unit=0;
        int length=clauses.size();

        //尋找unit
        for(int i=0; i<length; i++)
        {
            vector<int>&clauses_test=clauses[i];
            if(clauses_test.size()==1)
            {
               unit=clauses_test[0];
               break;
            }
        }

        //判斷是否為空括號
        if(unit==0)
            break;

        clauses.push_back({unit});

        if(unit>0)
            pn[unit].tof=true;
        else if(unit<0)
            pn[-unit].tof=false;

        remove_literal(clauses, pn);
        print(clauses);
    }
}

void PureLiteralElimination(vector<vector<int>>&clauses, vector<pos_neg>&pn)
{
    int length=clauses.size();
    int counter=0;
    while(1)
    {
        for(int i=0; i<num_variable+1; i++)
        {
            pn[i].num_neg=0;
            pn[i].num_pos=0;
        }
        //計算變數正負各出現次數
        for(int i=0; i<clauses.size(); i++)
        {
            for(int j=0; j<clauses[i].size(); j++)
            {
                if(clauses[i][j]>0)
                    pn[clauses[i][j]].num_pos++;
                else if(clauses[i][j]<0)
                    pn[-clauses[i][j]].num_neg++;
            }
        }
        /*for(int i=0; i<clauses.size()+1; i++)
        {
            cout<<pn[i].num_neg<<"   "<<pn[i].num_pos<<endl;
        }*/
        int pure_literal=0;
        int length=clauses.size();

        //尋找pure literal
        for(int i=1; i<num_variable+1; i++)
        {
            if( (pn[i].num_neg==0 && pn[i].num_pos!=0) || (pn[i].num_neg!=0 && pn[i].num_pos==0) )
            {
                if(pn[i].num_neg==0)
                {
                    counter++;
                    pure_literal=i;
                    break;
                }
                if(pn[i].num_pos==0)
                {
                    pure_literal=-i;
                    break;
                }
            }
        }

        if(pure_literal==0)
            break;

        clauses.push_back({pure_literal});

        if(pure_literal>0)
            pn[pure_literal].tof=true;

        else if(pure_literal<0)
            pn[-pure_literal].tof=false;

        remove_literal(clauses, pn);
        print (clauses);
    }
}

int DLIS(vector<vector<int>>&clauses)
{
    int maximum=0;
    pos_neg pn[num_variable+1];
    int pon=0;
    int maximum_variable;
    for(int i=0; i<num_variable+1; i++)
    {
        pn[i].num_neg=0;
        pn[i].num_pos=0;
    }

    //計算變數正負各出現次數
    for(int i=0; i<clauses.size(); i++)
    {
        for(int j=0; j<clauses[i].size(); j++)
        {
            if(clauses[i][j]>0)
                pn[clauses[i][j]].num_pos++;
            else if(clauses[i][j]<0)
                pn[-clauses[i][j]].num_neg++;
        }
    }

    for(int i=0; i<num_variable; i++)
    {
       if(pn[i].num_pos>maximum)
       {
           maximum=pn[i].num_pos;
           maximum_variable=i;
       }
       if(pn[i].num_neg>maximum)
       {
           maximum=pn[i].num_neg;
           maximum_variable=-i;
       }
    }
    return maximum_variable;

}