Untitled
unknown
plain_text
a year ago
9.2 kB
8
Indexable
#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; }
Editor is loading...
Leave a Comment