Untitled

 avatar
unknown
plain_text
a year ago
20 kB
6
Indexable
#include<iostream>
#include<string>
#include<fstream>
#include<vector>

using namespace std;

enum State{UNSAT = 0, SAT, CONTIN};

struct info
{
    int vari;
    char DF;
};

State DPLL(vector<int>, vector<vector<struct info>>, vector<int>, vector<vector<int>>);
State check(vector<vector<struct info>> &);
void input();
void select(int &, int &, vector<vector<int>> &);
void insert0(int, int, vector<int> &, vector<vector<struct info>> &, vector<int> &, vector<vector<int>> &);
void insert1(int, int, vector<int> &, vector<vector<struct info>> &, vector<int> &, vector<vector<int>> &);
void Unit_propagation(vector<int> &, vector<vector<struct info>> &, vector<int> &, vector<vector<int>> &);
void Pure_Literal_Assign(vector<int> &, vector<vector<struct info>> &, vector<int> &, vector<vector<int>> &);

vector<vector<struct info>> Equ;
vector<int> Ans;
vector<vector<int>> Times;
vector<int> Literals;

int main()
{
    input();

    if(DPLL(Literals, Equ, Ans, Times) == SAT)
    {
        cout << "s SATISFIABLE" << endl;
        for(int i = 1; i < Ans.size(); i++)
        {
            cout << "v “ " << i << " ” -> ";
            if(Ans[i] == 0)
            {
                cout << "False" << endl;
            }
            else if(Ans[i] == 1)
            {
                cout << "True" << endl;
            }
            else
            {
                cout << "True" << endl;
            }
        }
        cout << "Done";
        cout << endl;
        for(int i = 1; i < Ans.size(); i++)
        {
            if(Ans[i] == 0)
            {
                cout << "-1 ";
            }
            else
            {
                cout << "1 ";
            }
        }
    }
    else
    {
        cout << "s UNSATISFIABLE";
    }
}
void input()
{
    int m;
    int n;
    int v;
    int j = 0;

    string filename;
    string s;
    ifstream file;
    cout << "Enter the file name: ";
    cin >> filename;

    file.open(filename);
    while(file.fail())
    {
        cout << "File could not be opened." << endl;
        cout << "Please enter the input file name: ";
        cin >> filename;

        file.open(filename);
    }
    file >> s >> s;
    file >> m >> n;
    Times.push_back(vector<int>(0));
    Times.push_back(vector<int>(0));

    for(int i = 1; i <= n; i++)
    {
        Equ.push_back(vector<struct info>(0));
        Literals.push_back(0);
    }
    for(int i = 0; i <= m; i++)
    {
        Ans.push_back(2); //initial set 2
        Times[0].push_back(0);
        Times[1].push_back(0); //complement
    }
    while(file >> v)
    {
        if(v == 0 && j == Equ.size()-1)
        {
            break;
        }
        else
        {
            if(v == 0)
            {
                j++;
            }
            else
            {
                struct info R;
                R.vari = v;
                Equ[j].push_back(R);
                Literals[j]++;

                if(v > 0)
                {
                    Times[0][v]++;
                }
                else
                {
                    Times[1][-1*v]++; //complement
                }
            }
        }
    }
}
void select(int &m, int &n, vector<vector<int>> &times)
{
    m = 0;
    n = 1;
    int largest = times[m][n];

    if(largest < times[1][1])
    {
        largest = times[1][1];
        m = 1;
    }
    for(int i = 2; i < times[0].size(); i++)
    {
        if(times[0][i] > largest)
        {
            largest = times[0][i];
            m = 0;
            n = i;
        }
        if(times[1][i] > largest)
        {
            largest = times[1][i];
            m = 1;
            n = i;
        }
    }
}
void insert0(int m, int n, vector<int> &literals, vector<vector<struct info>> &equ0, vector<int> &ans0, vector<vector<int>> &times0)
{
    if(m == 0)
    {
        int v = n;

        ans0[v] = 0;
        times0[0][n] = 0;
        times0[1][n] = 0;

        for(int i = 0; i < equ0.size(); i++)
        {
            if(equ0[i][0].DF == 'D')
                continue;
            for(int j = 0; j < equ0[i].size(); j++)
            {
                if(equ0[i][j].vari == v)
                {
                    equ0[i][j].DF = 'F';
                    literals[i]--;
                }
                else if(equ0[i][j].vari == -1*v) //be the complement
                {
                    equ0[i][0].DF = 'D';
                    literals[i] = 0;
                    for(int k = 0; k < equ0[i].size(); k++)
                    {
                        if(equ0[i][k].vari > 0)
                        {
                            int t = equ0[i][k].vari;
                            if(times0[0][t] > 0)
                            {
                                times0[0][t]--;
                            }
                        }
                        else //be an complement
                        {
                            int t = -1*(equ0[i][k].vari);
                            if(times0[1][t] > 0)
                            {
                                times0[1][t]--;
                            }
                        }
                    }
                }
            }
        }
    }
    else if(m == 1) //be the complement
    {
        int v = -1*n; //~A

        ans0[n] = 1;
        times0[0][n] = 0;
        times0[1][n] = 0;

        for(int i = 0; i < equ0.size(); i++)
        {
            if(equ0[i][0].DF == 'D')
                continue;
            for(int j = 0; j < equ0[i].size(); j++)
            {
                if(equ0[i][j].vari == v) //~A = 0
                {
                    equ0[i][j].DF = 'F';
                    literals[i]--;
                }
                else if(equ0[i][j].vari == -1*v) //A = 1
                {
                    equ0[i][0].DF = 'D';
                    literals[i] = 0;
                    for(int k = 0; k < equ0[i].size(); k++)
                    {
                        if(equ0[i][k].vari > 0)
                        {
                            int t = equ0[i][k].vari;
                            if(times0[0][t] > 0)
                            {
                                times0[0][t]--;
                            }
                        }
                        else //be an complement
                        {
                            int t = -1*(equ0[i][k].vari);
                            if(times0[1][t] > 0)
                            {
                                times0[1][t]--;
                            }
                        }
                    }
                }
            }
        }
    }
}
void insert1(int m, int n, vector<int> &literals, vector<vector<struct info>> &equ1, vector<int> &ans1, vector<vector<int>> &times1)
{
    if(m == 0)
    {
        int v = n;

        ans1[v] = 1;
        times1[0][n] = 0;
        times1[1][n] = 0;

        for(int i = 0; i < equ1.size(); i++)
        {
            if(equ1[i][0].DF == 'D')
                continue;
            for(int j = 0; j < equ1[i].size(); j++)
            {
                if(equ1[i][j].vari == -1*v) //be the complement
                {
                    equ1[i][j].DF = 'F';
                    literals[i]--;
                }
                else if(equ1[i][j].vari == v) //assign true to delete clause
                {
                    equ1[i][0].DF = 'D';
                    literals[i] = 0;
                    for(int k = 0; k < equ1[i].size(); k++)
                    {
                        if(equ1[i][k].vari > 0)
                        {
                            int t = equ1[i][k].vari;
                            if(times1[0][t] > 0)
                            {
                                times1[0][t]--;
                            }
                        }
                        else //be an complement
                        {
                            int t = -1*(equ1[i][k].vari);
                            if(times1[1][t] > 0)
                            {
                                times1[1][t]--;
                            }
                        }
                    }
                }
            }
        }
    }
    else if(m == 1) //be the complement
    {
        int v = -1*n; //~A has to be ture

        ans1[n] = 0;
        times1[0][n] = 0;
        times1[1][n] = 0;

        for(int i = 0; i < equ1.size(); i++)
        {
            if(equ1[i][0].DF == 'D')
                continue;
            for(int j = 0; j < equ1[i].size(); j++)
            {
                if(equ1[i][j].vari == -1*v) //A = 0
                {
                    equ1[i][j].DF = 'F';
                    literals[i]--;
                }
                else if(equ1[i][j].vari == v) //~A = 1
                {
                    equ1[i][0].DF = 'D';
                    literals[i] = 0;
                    for(int k = 0; k < equ1[i].size(); k++)
                    {
                        if(equ1[i][k].vari > 0)
                        {
                            int t = equ1[i][k].vari;
                            if(times1[0][t] > 0)
                            {
                                times1[0][t]--;
                            }
                        }
                        else //be an complement
                        {
                            int t = -1*(equ1[i][k].vari);
                            if(times1[1][t] > 0)
                            {
                                times1[1][t]--;
                            }
                        }
                    }
                }
            }
        }
    }
}
State check(vector<vector<struct info>> &equ)
{
    int sat = 1;
    for(int i = 0; i < equ.size(); i++)
    {
        if(equ[i][0].DF != 'D')
        {
            sat *= 0;
        }
        int unsat = 1;
        for(int j = 0; j < equ[i].size(); j++)
        {
            if(equ[i][j].DF != 'F')
            {
                unsat *= 0;
            }
        }
        if(unsat == 1)
        {
            return UNSAT;
        }
    }
    if(sat == 1)
    {
        return SAT;
    }
    return CONTIN;
}
State DPLL(vector<int> literals, vector<vector<struct info>> equ, vector<int> ans, vector<vector<int>> times)
{
    int m, n;
    //copy one as insert 0's
    Unit_propagation(literals, equ, ans, times);

    if(check(equ) == SAT)
    {
        Ans = ans;
        return SAT;
    }
    else if(check(equ) == UNSAT)
    {
        return UNSAT;
    }

    Pure_Literal_Assign(literals, equ, ans, times);

    if(check(equ) == SAT)
    {
        Ans = ans;
        return SAT;
    }
    else if(check(equ) == UNSAT)
    {
        return UNSAT;
    }

    vector<int> literals0 = literals;
    vector<vector<struct info>> equ0 = equ;
    vector<int> ans0 = ans;
    vector<vector<int>> times0 = times;

    select(m, n, times);
    //first call function to insert 1
    //if it's sat return sat and assign current ans to global variable
    //else if it's unsat then use the copy and insert 0
    //  if it's sat return sat and assign current ans to global variable
    //  else if it's unsat return unsat
    //  else call DPLL pass current equ and ans by value
    //else call DPLL pass current equ and ans by value
    insert1(m, n, literals, equ, ans, times);
    if(check(equ) == SAT)
    {
        Ans = ans;
        return SAT;
    }
    else if(check(equ) == UNSAT)
    {
        insert0(m, n, literals0, equ0, ans0, times0);
        if(check(equ0) == SAT)
        {
            Ans = ans0;
            return SAT;
        }
        else if(check(equ0) == UNSAT)
        {
            return UNSAT;
        }
        else
        {
            return DPLL(literals0, equ0, ans0, times0);
        }
    }
    else
    {
        if(DPLL(literals, equ, ans, times) == SAT)
        {
            return SAT;
        }
        else if(DPLL(literals, equ, ans, times) == UNSAT)
        {
            insert0(m, n, literals0, equ0, ans0, times0);
            if(check(equ0) == SAT)
            {
                Ans = ans0;
                return SAT;
            }
            else if(check(equ0) == UNSAT)
            {
                return UNSAT;
            }
            else
            {
                return DPLL(literals0, equ0, ans0, times0);
            }
        }
    }
}
void Unit_propagation(vector<int> &literals, vector<vector<struct info>> &equ, vector<int> &ans, vector<vector<int>> &times)
{
    for(int i = 0; i < literals.size(); i++)
    {
        if(literals[i] == 1)
        {
            int v = equ[i][0].vari;
            if(v > 0)
            {
                ans[v] = 1;
                times[0][v] = 0;
                times[1][v] = 0;
                equ[i][0].DF = 'D';
                literals[i] = 0;

                for(int j = 0; j < equ.size(); j++)
                {
                    if(equ[j][0].DF == 'D')
                        continue;
                    for(int k = 0; k < equ[j].size(); k++)
                    {
                        if(equ[j][k].vari == -1*v) //be the complement
                        {
                            equ[j][k].DF = 'F';
                            literals[j]--;
                        }
                        else if(equ[j][k].vari == v) //assign true to delete clause
                        {
                            equ[j][0].DF = 'D';
                            literals[j] = 0;
                            for(int w = 0; w < equ[j].size(); w++)
                            {
                                if(equ[j][w].vari > 0)
                                {
                                    int t = equ[j][w].vari;
                                    if(times[0][t] > 0)
                                    {
                                        times[0][t]--;
                                    }
                                }
                                else //be an complement
                                {
                                    int t = -1*(equ[j][w].vari);
                                    if(times[1][t] > 0)
                                    {
                                        times[1][t]--;
                                    }
                                }
                            }
                        }
                    }
                }
            }
            else
            {
                ans[-1*v] = 0;
                times[0][-1*v] = 0;
                times[1][-1*v] = 0;
                equ[i][0].DF = 'D';
                literals[i] = 0;

                for(int j = 0; j < equ.size(); j++)
                {
                    if(equ[j][0].DF == 'D')
                        continue;
                    for(int k = 0; k < equ[j].size(); k++)
                    {
                        if(equ[j][k].vari == -1*v) //be the complement
                        {
                            equ[j][k].DF = 'F';
                            literals[j]--;
                        }
                        else if(equ[j][k].vari == v) //assign true to delete clause
                        {
                            equ[j][0].DF = 'D';
                            literals[j] = 0;
                            for(int w = 0; w < equ[j].size(); w++)
                            {
                                if(equ[j][w].vari > 0)
                                {
                                    int t = equ[j][w].vari;
                                    if(times[0][t] > 0)
                                    {
                                        times[0][t]--;
                                    }
                                }
                                else //be an complement
                                {
                                    int t = -1*(equ[j][w].vari);
                                    if(times[1][t] > 0)
                                    {
                                        times[1][t]--;
                                    }
                                }
                            }
                        }
                    }
                }
            }
        }
    }
}
void Pure_Literal_Assign(vector<int> &literals, vector<vector<struct info>> &equ, vector<int> &ans, vector<vector<int>> &times)
{
    for(int i = 1; i < times[0].size(); i++)
    {
        if(times[0][i] == 0 && times[1][i] > 0) //has only complement
        {
            ans[i] = 0;
            times[1][i] = 0;

            for(int j = 0; j < equ.size(); j++)
            {
                if(equ[j][0].DF == 'D')
                    continue;
                for(int k = 0; k < equ[j].size(); k++)
                {
                    if(equ[j][k].vari == -1*i)
                    {
                        equ[j][0].DF = 'D';
                        literals[j] = 0;
                        for(int m = 0; m < equ[j].size(); m++)
                        {
                            if(equ[j][m].vari > 0)
                            {
                                if(times[0][equ[j][m].vari] > 0)
                                {
                                    times[0][equ[j][m].vari]--;
                                }
                            }
                            else
                            {
                                if(times[1][-1*(equ[j][m].vari)] > 0)
                                {
                                    times[1][-1*(equ[j][m].vari)]--;
                                }
                            }
                        }
                    }
                }
            }
        }
        else if(times[0][i] > 0 && times[1][i] == 0) //has no complement
        {
            ans[i] = 1;
            times[0][i] = 0;

            for(int j = 0; j < equ.size(); j++)
            {
                if(equ[j][0].DF == 'D')
                    continue;
                for(int k = 0; k < equ[j].size(); k++)
                {
                    if(equ[j][k].vari == i)
                    {
                        equ[j][0].DF = 'D';
                        literals[j] = 0;
                        for(int m = 0; m < equ[j].size(); m++)
                        {
                            if(equ[j][m].vari > 0)
                            {
                                if(times[0][equ[j][m].vari] > 0)
                                {
                                    times[0][equ[j][m].vari]--;
                                }
                            }
                            else
                            {
                                if(times[1][-1*(equ[j][m].vari)] > 0)
                                {
                                    times[1][-1*(equ[j][m].vari)]--;
                                }
                            }
                        }
                    }
                }
            }
        }
    }
}

Editor is loading...
Leave a Comment