main.cpp
unknown
c_cpp
a year ago
5.4 kB
10
Indexable
#include<bits/stdc++.h> #include <fstream> using namespace std; struct myclass { bool operator() (int a, int b) { return abs(a)< abs(b); } } sorting; int check_empty_clause(vector<set<int>> &clauses){ int cl = clauses.size(); for(int i=0;i<cl;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-=1; } 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(); assignment.push_back(*it); clauses.erase(clauses.begin()); remove_new_p(clauses,assignment); break; } } } return; } void pure_literal(vector<set<int>> &clauses, vector<int> &assignment, int literals){ int check_arr1[literals+1]; int check_arr2[literals+1]; for(int i=0;i<=literals;i++){ check_arr1[literals]=0; check_arr2[literals]=0; } int cl = clauses.size(); for(int i=0;i<cl;i++) { for (auto pl=clauses[i].begin(); pl != clauses[i].end(); pl++) { int val = *pl; if(val>0){ check_arr1[-val]=1; } else if(val<0){ check_arr2[val]=-1; } } } for(int i=1;i<=literals;i++) { if(check_arr1[i]==1 &&check_arr2[i]==0){ assignment.push_back(check_arr1[i]*1); remove_new_p(clauses,assignment); } else if(check_arr2[i]==-1&&check_arr1[i]==0){ assignment.push_back(check_arr2[i]*(-1)); 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(), sorting); int counter= 0; for(int i=0; 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){ sort_ans(assignment,literals); for(int i=0;i<literals;i++){ cout<< "v \" " << i+1 << " \" -> "<<(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 -maxv; } } bool DPLL(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(clauses, assignment,newp, vnum) || DPLL(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; int new_p = DLIS(clauses,vnum); bool answer = DPLL(clauses, assignment,new_p, vnum) || DPLL(clauses,assignment,-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