Untitled
unknown
plain_text
a year ago
7.4 kB
4
Indexable
#include <iostream> #include <fstream> #include <vector> using namespace std; void deleting(int judge,int deleteliteral, vector<vector<int>> &clause, vector<int> &plusliteral, vector<int> &minusliteral, vector<int> &literalnum, int clausenum, int variablenum, vector<int> &ans) { for(int i=1; i<=clausenum; i++){ if(clause[i][0]==0){ if(clause[i][deleteliteral]!=2){ if(clause[i][deleteliteral]==judge){ clause[i][0]=1; literalnum[i]=0; minusliteral[deleteliteral]=0; plusliteral[deleteliteral]=0; ans[deleteliteral]=judge; for(int k=1; k<=variablenum; k++){ if(clause[i][k]==0) minusliteral[k]--; else if(clause[i][k]==1) plusliteral[k]--; } } else literalnum[i]--; } } } } bool unit(vector<vector<int>> &clause, vector<int> &plusliteral, vector<int> &minusliteral, vector<int> &literalnum, int clausenum, int variablenum, vector<int> &ans) { for (int i=1; i<=clausenum; i++){ if(clause[i][0]==0){ if(literalnum[i]==1){ for(int j=1; j<=variablenum; j++){ if(clause[i][j]==1){ if(ans[j]==2){ ans[j]=1; deleting(1, j, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans); } } else if(clause[i][j]==0){ if(ans[j]==2){ ans[j]=0; deleting(0, j,clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans); } } } } } } for (int i=1; i<=clausenum; i++){ if(clause[i][0]==0){ if(literalnum[i]==0){ return 0; break; } } if(i == clausenum) return 1; } } bool pure(vector<vector<int>> &clause, vector<int> &plusliteral, vector<int> &minusliteral, vector<int> &literalnum, int clausenum, int variablenum, vector<int> &ans) { for(int i=1; i<=variablenum; i++){ if(plusliteral[i]>0 && minusliteral[i]==0){ if(ans[i]==2){ ans[i]=1; deleting(1, i, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans); } } else if(plusliteral[i]==0 && minusliteral[i]>0){ if(ans[i]==2){ ans[i]=0; deleting(0, i, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans); } } } for (int i=1; i<=clausenum; i++){ if(clause[i][0]==0){ if(literalnum[i]==0){ return 0; break; } } if(i == clausenum) return 1; } } int dlis(vector<vector<int>> &clause, vector<int> &plusliteral, vector<int> &minusliteral, vector<int> &literalnum, int clausenum, int variablenum, vector<int> &ans) { int most=0, mostliteral=0; for(int i=1; i<=variablenum; i++){ if(plusliteral[i]+minusliteral[i]>most){ if(ans[i]==2){ most = plusliteral[i]+minusliteral[i]; mostliteral = i; } } if (i==variablenum) return i; } } bool dpll(int value, int deleteliteral, vector<vector<int>> clause, vector<int> plusliteral, vector<int> minusliteral, vector<int> literalnum, int clausenum, int variablenum, vector<int> ans) { if(deleteliteral!=0){ deleting(value, deleteliteral,clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans); } bool clauseanswer=0, wronganswer=1; wronganswer = unit(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans); if (wronganswer==0) return 0; wronganswer = pure(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans); if (wronganswer==0) return 0; deleteliteral = dlis(clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans); for (int i=1; i<=clausenum; i++){ if(clause[i][0]==0){ clauseanswer=0; break; } if(i==clausenum) clauseanswer=1; } for (int i=1; i<=clausenum; i++){ if(clause[i][0]==0){ if(literalnum[i]==0){ wronganswer=0; break; } } if(i == clausenum) return 1; } if (wronganswer == 0) return 0; else return dpll(0, deleteliteral, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans) || dpll(1, deleteliteral, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans); } int main(int argc, char *argv[]) { char p; string cnf; int inputnum, variablenum, clausenum, counter=1; ifstream inputfile(argv[1], ios::in); inputfile >> p >> cnf >> variablenum >> clausenum; vector <vector<int>>clause(clausenum+1, vector<int>(variablenum+1)); for (int i=0; i<=clausenum; i++){ for (int j=0; j<=variablenum; j++){ clause[i][j]=2; } } for (int i=0; i<=clausenum; i++) clause[i][0]=0; //this array caculate the number of literal in each clauses vector <int>literalnum(clausenum+1); for (int i=0; i<=clausenum; i++) literalnum[i]=0; vector <int>plusliteral(variablenum+1); vector <int>minusliteral(variablenum+1); for (int i=0; i<=variablenum; i++){ plusliteral[i]=0; minusliteral[i]=0; } //store file into array while (inputfile >> inputnum){ for (int i=1; i<=variablenum; i++){ if (inputnum==i){ clause[counter][i]=1; literalnum[counter]++; plusliteral[i]++; } else if(inputnum==-i){ clause[counter][i]=0; minusliteral[i]++; literalnum[counter]++; } } if (inputnum==0) counter ++; if (counter > clausenum) break; } //set ans array vector <int>ans(variablenum+1); for(int i=0; i<=variablenum; i++) ans[i]=2; ofstream outputfile(argv[2], ios::out); if (dpll(0, 0, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans)==1){ outputfile << "s SATISFIABLE"<<endl; for(int i=1; i<=variablenum; i++){ outputfile << "v “ "<<i<< " ” -> "; if(ans[i]==0) outputfile << "False"<<endl; else outputfile << "True"<< endl; } outputfile << "Done"; } else if(dpll(0, 0, clause, plusliteral, minusliteral, literalnum, clausenum, variablenum, ans)==0){ outputfile << "s UNSATISFIABLE"; } return 0; }
Editor is loading...
Leave a Comment