112501540_Final.cpp

//#include <bits/stdc++.h>
#include <fstream>
#include <cstdlib>
#include <vector>
#include <iostream>

using namespace std;

void remove_v(vector<vector<int>>& clauses, vector<int> assignment) {
    int literal = assignment.back();
    vector<int> erase_vector; //�������@�M��n�R�����s�_��
    for (int i = 0; i < clauses.size(); i++) {
        for (int j = 0; j < clauses[i].size(); j++) {
            if (clauses[i][j] == literal) {
                erase_vector.push_back(i);
                break;
            }
            else if (clauses[i][j] == -literal) {
                clauses[i].erase(clauses[i].begin() + j);
                break;
            }
        }
    }
    for (int i = erase_vector.size() - 1; i >=0 ; i--) { //�n�q�᭱�}�l�R�~���|�����ޭȶ]��
        clauses.erase(clauses.begin() + erase_vector[i]);
    }
    return;
}
bool check(vector<vector<int>>& clauses) {
    for (int i = 0; i < clauses.size(); i++) {
        if (clauses[i].size() == 0)
            return true;
    }
    return false;
}

bool unit_prop(vector<vector<int>>& clauses, vector<int>& assignment) {
    bool up_h = true;
    bool modify = false; // �p�G�����clauses�A�^��true
    while (up_h) {
        up_h = false;
        for (int i = 0; i < clauses.size(); i++) {
            if (clauses[i].size() == 1) {
                up_h = true;
                assignment.push_back(clauses[i][0]);
                remove_v(clauses, assignment);
                modify = true;
                break;
            }
        }
    }
    return modify;
}


bool pure_literal(vector<vector<int>>& clauses, vector<int>& assignment, int vnum) {
    vector<pair<int, int>> checker(vnum + 1, { 0,0 });
    bool modify = false; // �p�G�����clauses�A�^��true

    for (int i = 0; i < clauses.size(); i++) {
        for (int j = 0; j < clauses[i].size(); j++) {
            int num = clauses[i][j];
            if (num < 0) {
                checker[-1 * num].second = 1;
            }
            else {
                checker[num].first = 1;
            }
        }
    }

    for (int i = 1; i <= vnum; i++)
    {
        if (checker[i].first == 1 && checker[i].second == 0) {
            assignment.push_back(i);
            remove_v(clauses, assignment);
            modify = true;
        }
        else if (checker[i].first == 0 && checker[i].second == 1) {
            assignment.push_back(-i);
            remove_v(clauses, assignment);
            modify = true;
        }
    }
    return modify;
}
void first_check(vector<vector<int>>& clauses, vector<int>& assignment, int vnum) {
    // �Y�i��unit_prop��pure_literal����������ק�A�N�n�A���O����A�Ȩ�S������קﲣ��
    while (true) {
        bool unit_prop_complete = unit_prop(clauses, assignment);
        bool pure_literal_complete = pure_literal(clauses, assignment, vnum);
        if (!unit_prop_complete && !pure_literal_complete) break;
    }
}

int DLIS(vector<vector<int>>& clauses, int vnum) {
    int maxv = -1, selectv = -1, literals, variable;
    //array�j�p����O�ܼơA�ҥH���vector
    vector<int> count_arr1(vnum + 1, 0);
    vector<int> count_arr2(vnum + 1, 0);
    int cl = clauses.size();

    for (int i = 0; i < cl; i++) {
        for (int j = 0; j < clauses[i].size(); j++) {
            literals = clauses[i][j];
            variable = abs(literals);
            if (literals > 0)
                count_arr1[variable]++;
            else
                count_arr2[variable]++;
        }
    }

    for (int i = 1; i <= vnum; i++) {
        if (count_arr1[i] + count_arr2[i] > maxv) {
            maxv = count_arr1[i] + count_arr2[i];
            selectv = i;
        }
    }
    if (count_arr1[selectv] >= count_arr2[selectv])
        return selectv;
    else
        return -1 * selectv;
}

bool DPLL(vector<vector<int>>& clauses, vector<int>& assignment, int next, const int vnum, vector<vector<int>> new_clauses, vector<int> new_assignment) {
    // ���F�����j����ھڤ��P�����䲣�ͤ��P�����G�A�u���b����O�ϥ�call by value��new_clauses�Bnew_assignment
    // ���M�|�y���^�ǫ�n�i��t�~������M���e��i�h�����A���P
    // �̫�Y��쵲�G�h�A��new_clauses�Bnew_assignment���w��call by reference��clauses�Bassignment
    new_assignment.push_back(next);
    remove_v(new_clauses, new_assignment);
    first_check(new_clauses, new_assignment, vnum);

    if (new_clauses.size() == 0) {
        assignment = new_assignment;
        clauses = new_clauses;
        return true;
    }

    if (check(new_clauses)) {
        return false;
    }
    int newone = DLIS(new_clauses, vnum);
    return DPLL(clauses, assignment, newone, vnum, new_clauses, new_assignment) || DPLL(clauses, assignment, -1 * newone, vnum, new_clauses, new_assignment);

}
vector<int> find_solution(vector<int>& assignment, int vnum) {
    vector<int> solution(vnum + 1, 1);
    for (int i = 0; i < assignment.size(); i++)
    {
        int val = assignment[i];
        if (val < 0)
        {
            solution[val * -1] = -1;
        }
    }

    return solution;
}

void save_ans(string filename, bool ans, vector<int> solution) {
    ofstream outputfile(filename, ios::trunc);
    if (ans) {
        outputfile << "s SATISFIABLE" << endl;
        for (int i = 1; i < solution.size(); i++)
        {
            string ans;
            if (solution[i] == 1) ans = "True";
            else ans = "False";
            outputfile << "v \" " << i << " \" -> " << ans << endl;
        }
        outputfile << "Done";
    }
    else {
        outputfile << "s UNSATISFIABLE" << endl;
    }
}

int main(int argc, char* argv[]) {
    int vnum, cnum;

    string trash;

    //string filename = "test1.txt";
    //string filename = "testcase3.cnf";

    ifstream inputfile(argv[1], ios::in);

    inputfile >> trash;
    inputfile >> trash;
    inputfile >> vnum;
    inputfile >> cnum;

    vector<vector<int>> clauses(cnum);

    for (int i = 0; i < cnum; i++) {
        int x;
        inputfile >> x;
        while (x != 0) {
            clauses[i].push_back(x);
            inputfile >> x;
        }
    }


    vector<int> assignment;


    int  newone = DLIS(clauses, vnum);
    bool ans = DPLL(clauses, assignment, newone, vnum, clauses, assignment) || DPLL(clauses, assignment, -1 * newone, vnum, clauses, assignment);
    vector<int> solution;
    if (ans) {
        solution = find_solution(assignment, vnum);
    }

    save_ans(argv[2], ans, solution);
    return 0;
}