main.cpp
unknown
c_cpp
a year ago
5.8 kB
10
Indexable
#include<bits/stdc++.h> #include <fstream> using namespace std; int check_empty_clause(vector<set<int>> &clauses){ int rows = clauses.size(); for(int i=0;i<rows;i++) { if(clauses[i].size()==0) return 1; } return 0; } void remove_new_p(vector<set<int>>&clauses, vector<int> &assignment){ int new_p = assignment.back(); for(int i=0;i<clauses.size();i++) { if(clauses[i].find(new_p) != clauses[i].end()){ clauses.erase(clauses.begin()+i); i--; } else if(clauses[i].find(-1*new_p)!=clauses[i].end()){ clauses[i].erase(clauses[i].find(-1*new_p)); } } return; } void unit_prop(vector<set<int>> &clauses,vector<int> &assignment){ int flag=1; while(flag==1){ flag=0; int rows = clauses.size(); for(int i=0;i<rows;i++){ if(clauses[i].size()==1){ flag=1; set<int>::iterator it = clauses[i].begin(); clauses.erase(clauses.begin()+i); assignment.push_back(*it); remove_new_p(clauses,assignment); break; } } } return; } void pure_literal(vector<set<int>> &clauses, vector<int> &assignment, int literals){ vector<int> check(literals+1, 0); int curr_rows = clauses.size(); for(int i=0;i<curr_rows;i++) { for (auto it=clauses[i].begin(); it != clauses[i].end(); ++it) { int val = *it; if(val<0){ if(check[-1*val]==1) check[-1*val]=2; else if(check[-1*val]==0) check[-1*val]=-1; else if(check[-1*val]==2) check[-1*val]=2; } else{ if(check[val]==-1) check[val]=2; else if(check[val]==0) check[val]=1; else if(check[val]==2) check[val]=2; } } } for(int i=1;i<=literals;i++) { if(check[i]==1 || check[i]==-1){ assignment.push_back(check[i]*i); remove_new_p(clauses,assignment); } } return; } void sort_ans(vector<int> &assignment, int literals){ vector<int> store = assignment; assignment.resize(0); sort(store.begin(), store.end(), [](int a, int b){return abs(a) < abs(b);}); int counter= 0; for(int i=1; i<=literals; i++){ if (abs(store[counter]) == i){ assignment.push_back(store[counter]); counter++; } else{ assignment.push_back(i); } } } void print_ans(vector<int> &assignment, int literals){ int size = assignment.size(); sort_ans(assignment,literals); vector<int> solution(literals+1,1); for(int i=1;i<=literals;i++){ cout<< "v \" " << i << " \" -> "<<(assignment[i]>0?"True":"False")<<endl; } cout<<"Done"; return; } int DLIS(vector<set<int>> &clauses, int vnum){ vector<pair<int, int>> cnt_literal(vnum + 1, {0, 0}); int clause_cnt = clauses.size(); for(int i=0; i<clause_cnt; i++){ for(set<int> ::iterator it = clauses[i].begin(); it != clauses[i].end(); ++it){ int num = *it; if (num < 0){ cnt_literal[-1 * num].second += 1; } else{ cnt_literal[num].first += 1; } } } int maxnum = -1; int maxv; for(int i=1; i<cnt_literal.size(); i++){ if (maxnum < (cnt_literal[i].first + cnt_literal[i].second)){ maxnum = cnt_literal[i].first + cnt_literal[i].second; maxv = i; } } if (cnt_literal[maxv].first >= cnt_literal[maxv].second){ return maxv; } else { return -1 * maxv; } } bool DPLL_algo(vector<set<int>>clauses,vector<int> assignment,int new_p, int vnum){ assignment.push_back(new_p); remove_new_p(clauses,assignment); unit_prop(clauses,assignment); pure_literal(clauses,assignment,vnum); if(clauses.size()==0){ print_ans(assignment,vnum); return true; } if(check_empty_clause(clauses)==1){ return false; } int newp = DLIS(clauses,vnum); return DPLL_algo(clauses, assignment,newp, vnum) || DPLL_algo(clauses,assignment,-1*newp,vnum); } int main() { string trash; string file; cout<<"Enter name of file: "<<endl; cin>>file; ifstream inputfile(file,ios::in); inputfile>>trash; inputfile>>trash; int cnum; int vnum; inputfile>> vnum; inputfile>>cnum; vector<set<int>> clauses(cnum); int num; for(int i=0;i<cnum;i++) { inputfile>>num; while(num!=0) { clauses[i].insert(num); inputfile>>num; } } vector<int> assignment; unit_prop(clauses,assignment); pure_literal(clauses,assignment,vnum); if(clauses.size()==0){ print_ans(assignment,vnum); cout<<"s SATISFIABLE"<<endl; return 0; } if(check_empty_clause(clauses)==1){ cout<<"s UNSATISFIABLE"<<endl; return 0; } int new_p = DLIS(clauses,vnum); bool answer = DPLL_algo(clauses, assignment,new_p, vnum) || DPLL_algo(clauses,assignment,-1*new_p,vnum); if(answer){ print_ans(assignment,vnum); cout<<"s SATISFIABLE"<<endl; } else cout<<"s UNSATISFIABLE"<<endl; return 0; }
Editor is loading...
Leave a Comment