Untitled
unknown
plain_text
a year ago
18 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<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<vector<struct info>> &, vector<int> &, vector<vector<int>> &); void insert1(int, int, vector<vector<struct info>> &, vector<int> &, vector<vector<int>> &); void Unit_propagation(); void Pure_Literal_Assign(); vector<vector<struct info>> Equ; vector<int> Ans; vector<vector<int>> Times; int main() { input(); Unit_propagation(); Pure_Literal_Assign(); if(DPLL(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"; } 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)); } 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); if(v > 0) { Times[0][v]++; } else { Times[1][-1*v]++; //complement } } } } } void select(int &m, int &n, vector<vector<int>> ×) { 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<vector<struct info>> &equ0, vector<int> &ans0, vector<vector<int>> ×0) { 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'; } else if(equ0[i][j].vari == -1*v) //be the complement { equ0[i][0].DF = 'D'; 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'; } else if(equ0[i][j].vari == -1*v) //A = 1 { equ0[i][0].DF = 'D'; 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<vector<struct info>> &equ1, vector<int> &ans1, vector<vector<int>> ×1) { 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'; } else if(equ1[i][j].vari == v) //assign true to delete clause { equ1[i][0].DF = 'D'; 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'; } else if(equ1[i][j].vari == v) //~A = 1 { equ1[i][0].DF = 'D'; 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<vector<struct info>> equ, vector<int> ans, vector<vector<int>> times) { int m, n; //copy one as insert 0's 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, equ, ans, times); if(check(equ) == SAT) { Ans = ans; return SAT; } else if(check(equ) == UNSAT) { insert0(m, n, equ0, ans0, times0); if(check(equ0) == SAT) { Ans = ans0; return SAT; } else if(check(equ0) == UNSAT) { return UNSAT; } else { return DPLL(equ0, ans0, times0); } } else { if(DPLL(equ, ans, times) == SAT) { return SAT; } else if(DPLL(equ, ans, times) == UNSAT) { insert0(m, n, equ0, ans0, times0); if(check(equ0) == SAT) { Ans = ans0; return SAT; } else if(check(equ0) == UNSAT) { return UNSAT; } else { return DPLL(equ0, ans0, times0); } } } } void Unit_propagation() { for(int i = 0; i < Equ.size(); i++) { if(Equ[i].size() == 1) { if(Equ[i][0].vari < 0) { Ans[-1*(Equ[i][0].vari)] = 0; Times[1][-1*(Equ[i][0].vari)] = 0; Times[0][-1*(Equ[i][0].vari)] = 0; Equ[i][0].DF = 'D'; 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 == Equ[i][0].vari) { Equ[j][0].DF = 'D'; 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(Equ[j][k].vari == -1*(Equ[i][0].vari)) { Equ[j][k].DF = 'F'; //assign false } } } } else { Ans[Equ[i][0].vari] = 1; Times[0][Equ[i][0].vari] = 0; Times[1][Equ[i][0].vari] = 0; Equ[i][0].DF = 'D'; 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 == Equ[i][0].vari) { Equ[j][0].DF = 'D'; 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(Equ[j][k].vari == -1*(Equ[i][0].vari)) { Equ[j][k].DF = 'F'; //assign false } } } } } } } void Pure_Literal_Assign() { 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'; 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'; 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