Untitled
unknown
c_cpp
a year ago
5.0 kB
8
Indexable
#include <bits/stdc++.h> using namespace std; vector < vector<int> > clauses; unordered_map<int,int> l_freq; unordered_map<int,bool> l_assign; void input_file(), reset(vector<vector<int>>), unit_propagate(vector<vector<int>>), pure(vector<vector<int>>), dlis(vector<vector<int>>); bool isunit(vector<vector<int>>), dpll(vector<vector<int>>); int main(int argc, char *argv[]) { input_file(); if(dpll(clauses)) { cout << "s SATISFIABLE"; for(auto f: l_assign) { cout << "v \" " << f.first << " \" -> " << f.second; } cout << "Done"; } else { cout << "s UNSATISFIABLE"; return 0; } /*for(int a=0; a<clauses.size(); a++) { for(int b=0; b<clauses[a].size(); b++) { cout << clauses[a][b] << " "; } cout << endl; }*/ } void input_file(char *argv[]) { ifstream file("testcase1.cnf"); vector<int> temp; string line, t; getline(file, line); stringstream ss(line); int n; ss >> t; ss >> t; ss >> n; ss >> n; for(int a=0; a<n; a++) { getline(file, line); stringstream ss(line); int l; while(ss>>l && l!=0) { temp.push_back(l); } clauses.push_back(temp); temp.clear(); } } void reset(vector < vector<int> > clause) { for(int a=0; a<clause.size(); a++) { for(int b=0; b<clause[a].size(); b++) { l_assign[abs(clause[a][b])]==true; } } } bool dpll(vector < vector<int> > clause) { reset(clause); for(int a=0; a<clause.size(); a++) { for(int b=0; b<clause[a].size(); b++) { l_freq[clause[a][b]]++; } } while(isunit(clause)) { unit_propagate(clause); } pure(clause); if(clause.empty()) { return true; } for(int a=0; a<clause.size(); a++) { if(clause[a].empty()) { return false; } } dlis(clause); } bool isunit(vector < vector<int> > clause) { for(int a=0; a<clause.size(); a++) { if(clause[a].size()==1) { return true; } } return false; } void unit_propagate(vector < vector<int> > clause) { for(int a=0; a<clause.size(); a++) { if(clause[a].size()==1) { if(clause[a][0]<0) { l_assign[0-clause[a][0]]=false; } for(int b=0; b<clause.size(); b++) { auto i= find(clause[b].begin(), clause[b].end(), clause[a][0]); auto ni= find(clause[b].begin(), clause[b].end(), 0-clause[a][0]); if(i!= clause[b].end()) { clause.erase(clause.begin()+b); } if(ni!= clause[b].end()) { clause[b].erase(ni); } } clause.erase(clause.begin()+a); } } } void pure(vector < vector<int> > clause) { for(auto f: l_freq) { if(f.second+l_freq[0-(f.first)]==1) { for(int a=0; a<clause.size(); a++) { auto it=find(clause[a].begin(), clause[a].end(), f.first); if(it!=clause[a].end()) { if(f.first<0) { l_assign[abs(f.first)]=false; } clause.erase(clause.begin()+a); } } } } } void dlis(vector < vector<int> > clause) { int large=0, fr=0; for(auto f: l_freq) { if(l_freq[f.first]+ l_freq[0-f.first] > fr) { if(l_freq[f.first] >= l_freq[0-f.first]) { large=f.first; } else { large=0-f.first; } fr=l_freq[f.first]+ l_freq[0-f.first]; } } if(large<0) { l_assign[abs(large)]=false; } int b=0; for(; b<clause.size(); b++) { //cout << 1; auto i= find(clause[b].begin(), clause[b].end(), large); //cout << 2; auto ni= find(clause[b].begin(), clause[b].end(), 0-large); //cout << 3; if(i!= clause[b].end()) { clause.erase(clause.begin()+b); } //cout << 4; if(ni!= clause[b].end()) { clause[b].erase(ni); } //cout << 5; } for(int a=0; a<clauses.size(); a++) { for(int b=0; b<clauses[a].size(); b++) { cout << clauses[a][b] << " "; } cout << endl; } dpll(clause); }
Editor is loading...
Leave a Comment