Untitled
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>> ×) { 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>> ×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'; 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>> ×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'; 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>> ×) { 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>> ×) { 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