Untitled
unknown
plain_text
a year ago
10 kB
3
Indexable
#include <iostream> #include <fstream> #include<string> #include<cstdlib> #include<cmath> using namespace std; enum TYPE { UNASSIGNED = 0, NOPRIME = 1, PRIME = 2, DONTCARE = 3 }; void update_input(TYPE **input, bool *phi, int variable, bool decision, int num_v, int num_c){ for(int i=0;i<num_c;++i){ if(!phi[i]){ if(input[variable][i] == NOPRIME){ if(decision){ phi[i] = true; for(int j=0;j<num_v;++j) { input[j][i]=UNASSIGNED; } } else{ input[variable][i] = UNASSIGNED; } } else if(input[variable][i] == PRIME){ if(decision){ input[variable][i] = UNASSIGNED; } else{ phi[i] = true; for(int j=0;j<num_v;++j) { input[j][i]=UNASSIGNED; } } } } } } //Unit propagation void unit_propagation(TYPE **input,bool *phi,bool*answer1,bool*answer2, int num_v,int num_c) { int count,variable,clause; for(int i=0;i<num_c;i++) { if(!phi[i]) { count = 0; for(int j=0;j<num_v;j++) { if(input[j][i] != UNASSIGNED) { count++; variable = j; clause = i; } if(count == 2) { break; } } if(count == 1) { //assign value to input[variable] answer1[variable] = true; if(input[variable][clause] == NOPRIME) { answer2[variable] = true; update_input(input,phi,variable,true,num_v,num_c); } else { answer2[variable] = false; update_input(input,phi,variable,false,num_v,num_c); } unit_propagation(input, phi, answer1,answer2, num_v, num_c); return; } } } } //Pure Literal Assign void pure_literal_assign(TYPE **input,int variable_num,bool *phi,bool *answer1,bool *answer2,int clause_num) { bool noprime; bool prime; for(int i=0;i<variable_num;i++) { if(!answer1[i]) { noprime = prime = true; for(int j=0;j<clause_num;j++) { if(input[i][j] == NOPRIME){ prime = false; } else if(input[i][j] == PRIME){ noprime = false; } if(!(noprime || prime)){ continue; } if(j == clause_num-1){ answer1[i]=true; if(prime&&noprime) { ; } else if(prime){ answer2[i]=false; update_input(input,phi,i,false,variable_num,clause_num); } else if(noprime){ answer2[i]=true; update_input(input,phi,i,true,variable_num,clause_num); } pure_literal_assign(input,variable_num,phi,answer1,answer2,clause_num); return; } } } } } bool phi_is_empty(bool *phi, int num_c) { for(int i=0;i<num_c;++i) { if(!phi[i]) { return false; } } return true; } bool containing_empty_clause(TYPE **input,bool *phi, int num_v, int num_c) { bool lala; for(int i=0;i<num_c;++i){ if(!phi[i]){ lala = true; for(int j=0;j<num_v;++j){ if(input[j][i] != UNASSIGNED){ lala = false; break; } } if(lala){ return true; } } } return false; } int choose_a_literal(bool*answer1, int num_v) { for(int i=0;i<num_v;++i) { if(!answer1[i]) { return i+1; } } return 0; } //use a recurtion function bool DPLL(TYPE **input, bool *answer1, bool *answer2, bool *phi, int num_v, int num_c, int literal) { TYPE** input_1 = new TYPE*[num_v]; bool* answer1_1 = new bool[num_v]; bool* phi_1 = new bool[num_c]; for(int i = 0; i < num_v; ++i) { input_1[i] = new TYPE[num_c]; } for(int i=0;i<num_v;++i) { for(int j=0;j<num_c;++j) { input_1[i][j] = input[i][j]; } answer1_1[i] = answer1[i]; } for(int i=0;i<num_c;++i){ phi_1[i] = phi[i]; } if(literal != 0) { int y = abs(literal) - 1; answer1[y] = true; answer2[y] = (literal > 0); update_input(input, phi, y, (literal > 0), num_v, num_c); } unit_propagation(input, phi, answer1, answer2, num_v, num_c); pure_literal_assign(input, num_v, phi, answer1, answer2, num_c); if(phi_is_empty(phi, num_c)) { for(int i = 0; i < num_v; ++i) { delete[] input_1[i]; } delete[] input_1; delete[] answer1_1; delete[] phi_1; return true; } if(containing_empty_clause(input, phi, num_v, num_c)) { for(int i=0;i<num_v;++i) { for(int j=0;j<num_c;++j) { input[i][j] = input_1[i][j]; } answer1[i] = answer1_1[i]; } for(int i=0;i<num_c;++i){ phi[i] = phi_1[i]; } for(int i = 0; i < num_v; ++i) { delete[] input_1[i]; } delete[] input_1; delete[] answer1_1; delete[] phi_1; return false; } int lit = choose_a_literal(answer1, num_v); if(!(DPLL(input, answer1, answer2, phi, num_v, num_c, lit) || DPLL(input, answer1, answer2, phi, num_v, num_c, -lit))) { for(int i=0;i<num_v;++i) { for(int j=0;j<num_c;++j) { input[i][j] = input_1[i][j]; } answer1[i] = answer1_1[i]; } for(int i=0;i<num_c;++i){ phi[i] = phi_1[i]; } for(int i = 0; i < num_v; ++i) { delete[] input_1[i]; } delete[] input_1; delete[] answer1_1; delete[] phi_1; return false; } for(int i = 0; i < num_v; ++i) { delete[] input_1[i]; } delete[] input_1; delete[] answer1_1; delete[] phi_1; return true; } void input_file(char *argv,TYPE **input,bool *phi,bool *answer1,bool *answer2,int num_of_clause,int num_of_variable,istream &infile) { int x,y; for(int i=0;i<num_of_clause;++i) { cin >> x; while(x != 0) { y= abs(x)-1; if(input[y][i] == UNASSIGNED) { input[y][i] = (x > 0 ? NOPRIME : PRIME); } else if(input[y][i] == NOPRIME) { if(x < 0) { input[y][i] = DONTCARE; } } else if(input[y][i] == PRIME) { if(x > 0) { input[y][i] = DONTCARE; } } cin >> x; } } } void output_file(char *argv,bool *answer1, bool *answer2,int num_of_variable,bool result) { ofstream outfile(argv,ios::out); if(result) { cout<<"s SATISFIABLE"<<endl; for(int i=0;i<num_of_variable;i++) { cout<<"v \" "<<i+1<<" \" -> "<<(answer2[i] ? "True":"False")<<endl; } cout<<"Done"; return; } else { cout<<"s UNSATISFIABLE"; return; } } int main(int agrc,char*argv[]) { ifstream infile(argv[1],ios::in); int num_of_variable,num_of_clause ; string trash; infile>>trash>>trash; infile>>num_of_variable; infile>>num_of_clause; bool result; TYPE** input = new TYPE*[num_of_variable]; for (int i = 0; i < num_of_variable; ++i) { input[i] = new TYPE[num_of_clause]{UNASSIGNED}; } bool phi[num_of_clause]; for(int i=0;i<num_of_clause;++i){ phi[i] = false; } bool answer1[num_of_variable]; //check if assigned value bool answer2[num_of_variable]; //the real value for(int i=0;i<num_of_variable;++i){ answer1[i] = false; answer2[i] = false; } input_file(argv[1],input,phi,answer1,answer2,num_of_clause,num_of_variable,infile); ///////////////////////////////////////////////////////////// for(int i=0;i<num_of_clause;++i){ for(int j=0;j<num_of_variable;++j){ if(input[j][i] == DONTCARE){ phi[i] = true; for(int j=0;j<num_of_variable;++j) { input[j][i]=UNASSIGNED; } break; } } } result=DPLL(input, answer1, answer2, phi, num_of_variable, num_of_clause, 0); output_file(argv[2],answer1,answer2,num_of_variable,result); /////////////////////////////////////////////////////// for(int i = 0; i < num_of_variable; ++i) { delete[] input[i]; } delete[] input; }
Editor is loading...
Leave a Comment