Untitled
unknown
plain_text
a year ago
14 kB
4
Indexable
#include<iostream> #include<algorithm> #include<string> #include<iomanip> #include<vector> #include<sstream> #include<cstdlib> #include<fstream> using namespace std ; /* tell if the algorism can be satisfied or not ˅, ˄, ¬: respectively represent logic OR, AND, and NOT. Clause: Each clause is a disjunction of one or more literals, like (A ˅ B). what i might do is seperate the whole input by the {} clause use dynamic memory to store each clause struct ,pointer what if clause contain clause detect the first { if the next clause is also { means the clause in the containing another clause find { and run until '}' if detect { first than first determine the biggest layer second use insert since everyclause is && together then i just need to find a solution make every clause true when cout , the variable a b c are 1 2 3 . */ const int MAX_VARIAbLE = 100 ; int deletedclauses = 0 ; void input_file( char *argv , int &variables , int &clauses , vector<int> numbers ) { ifstream input( argv , ios::in ) ; char ch; int in ; string gar ; input >> gar ; input >> gar ; while ( input >> in ) { //number or not if( !input.fail() ){// if it is a number if( variables == 0 ) variables = in ; else if( clauses == 0 ) clauses = in ; else numbers.push_back( in ) ; } } } void output_file( char *argv , int variables , int arrofvariables[ ] , bool satisfiable ) { ofstream outputfile( argv , ios::out ) ; if ( satisfiable ){ outputfile << "s SATISFIABLE" << endl ; for( int i = 0 ; i < variables ; i ++ ){ outputfile << "v “ " << i + 1 << " -> " <<( arrofvariables[ i ] == 1 ? "True" : "False" ) << endl; }// if == 1 true ,if == -1 false , if == 0 false because the equation can already be satisfied when it havent be assign yet //it means no matter it is true or false the equation can be satisfied outputfile << " Done " << endl; }else{ outputfile << "s UNSATISFIABLE" << endl ; } } void seperate ( vector<int> numbers , int sizeofvector , int identical[][MAX_VARIAbLE] , int clauses , int variables ) { for( int i = 0 , j = 0 , a = 0 ; a < sizeofvector ; j ++ , a ++ ){ if( numbers[ a ] == 0 ){ i ++ ; j = 0 ; a ++ ; while( numbers[a] == 0 ) a ++ ; identical[ i ][ j ] = numbers[ a ] ; } else { identical[ i ][ j ] = numbers[ a ] ; } } //my rule if numbers[ a ] == 1 than [ i ][ j ] == 1 //but if numbers [ a ] == -1 } void eli_do ( int identical[][MAX_VARIAbLE] , int clauses , int variables , int aim , int clau , int vari , int operation ) { if( operation == 1 ){ for( int i = clau + 1 ; i < clauses ; i ++ ) for( int j = 0 ; j < variables ; j ++ ){ //delete whole clauses int temp = identical[i][j] ; identical[ i - 1 ][ j ] = temp ; } } if( operation == 2 ){ for( int c = vari + 1 ; c < variables ; c ++ ){ identical[ clau ][ c - 1 ] = identical[ clau ][ c ] ; } } } void elimination ( int identical[][MAX_VARIAbLE] , int clauses , int variables , int aim ) { int clau = 0 ; int vari = 0 ; int counter = 0 ; //check for( int i = 0 ; i < clauses ; i ++ ) for( int j = 0 ; j < variables ; j ++ ){ if( identical[i][j] == aim ){ clau = i ; vari = j ; eli_do( identical , clauses , variables , aim , clau , vari , 1 ) ; i -- ; j = 0 ; counter ++ ; for( int b = 0 ; b < variables ; b ++ ) identical[ clauses - counter ][b] = 0 ; } } for( int i = 0 ; i < clauses ; i ++ ) for( int j = 0 ; j < variables ; j ++ ){ if( identical[i][j] == aim * -1 ){ clau = i ; vari = j ; eli_do( identical , clauses , variables , aim , clau , vari , 2 ) ; i -- ; j = 0 ; } } } void elimination_PLE ( int identical[][MAX_VARIAbLE] , int clauses , int variables , int aim ) { for( int i = 0 ; i < clauses ; i ++ ) for( int j = 0 ; j < variables ; j ++ ){ if( identical[ i ][ j ] == aim ){ //delete whole clauses for( int a = i + 1 ; a < clauses ; a ++ ){ for( int b = 0 ; b < variables ; b ++ ){ int temp = identical[i][j] ; identical[ i - 1 ][ j ] = temp ; } } } } } int DPLL_algorithm ( int forcheck[][MAX_VARIAbLE] , int clauses , int variables , int arrofvariables[] ) { //calculate the truth value of the clause //what algorithm really do is //calculate every clause at a time and and with bool_temp int bool_inside = 0 ; int bool_iden = 0 ; int temp = 0 ; int truth_value = 0 ; for( int i = 0 ; i < clauses ; i ++ ){ for( int j = 0 ; j < variables ; j ++ ){ //what's the variable , such as : a, -b ,c ... if( forcheck[i][j] != 0 ){ temp = forcheck[i][j] ; if( temp < 0 ) bool_iden = arrofvariables[ temp*-1 - 1 ] * temp ; else bool_iden = arrofvariables[ temp - 1 ] * temp ; if( bool_iden != 0 ){ if( bool_iden == 1 || bool_inside == 1 ) bool_inside = 1 ; } } } if( truth_value == 1 && bool_inside == 1 ) truth_value = 1 ; else truth_value = 0 ; } //see if unsatisfiable int check = 0 ; for( int i = 0 ; i < variables ; i ++ ) if( arrofvariables[i] != 0 ) check ++ ; if( check == variables && truth_value == 0) truth_value = 2 ; return truth_value ; } void DLIS ( int identical[][MAX_VARIAbLE] , int clauses , int variables , int counter[][MAX_VARIAbLE] , int arrofvariables[] ) //call by DPLL { //𝑤(𝐹, 𝑢) = ∑ 𝑑𝑘(𝐹, 𝑢) //Φ(𝑥, 𝑦) = max{𝑥, 𝑦} /* determine priority of variables by search how many clauses contain the variable assign the variable that contained by the most clauses true if a is the most contained variable false if -a is the most contained */ int biggest = 0 ; int symbol = 0 ; int who = 0 ; int aim = 0 ; //determine whose show up the most times for( int i = 0 ; i < 2 ; i ++ ) for( int j = 0 ; j < variables ; j ++ ) if( counter[i][j] > biggest ){ biggest = counter[i][j] ; symbol = i ;// y who = j ; // x } //assign true if the positive version is more than its negative version of the variable //else assign false if( symbol == 0 ){ arrofvariables[ who ] = 1 ; aim = who + 1 ; } else{ arrofvariables[ who ] = -1 ; aim = who + 1 ; aim *= -1 ; } //delete clauses contain the variable elimination( identical , clauses , variables , aim ) ; } void DPLL_funtion ( int identical[][ MAX_VARIAbLE ] , int clauses , int variables , int arrofvariables[] ,int counter[][MAX_VARIAbLE] ) { //including assign variables true or false int aim = 0 ; for( int i = 0 ; i < 2 ; i ++ ) for( int j = 0 ; j < variables ; j ++ ) counter[i][j] = 0 ; //unit propagation //............................................................... //there is a clauses that only contain a variable //(A) ˄ (A ˅ B ˅ D) ˄ (¬A ˅ B) ˄ (¬A ˅ B ˅ C) //Because (A) is the unit clause, A must be set to “TRUE”. The formula can be //simplified to (B) ˄ (B ˅ C) // looking for clause with only one variables for( int i = 0 ; i < clauses ; i ++ ) for( int j = 0 ; j < 2 ; j ++ ){ if ( ( identical[ i ][ 1 ] == 0 ) && (identical[i][0] != 0 ) ){//already 0 when j = 2 //means the clauses has only one variable int temp = identical[ i ][ j - 1 ] ;//what's the variable arrofvariables[ temp - 1 ] = 1 ; aim = temp ; elimination ( identical , clauses , variables , aim ) ; //check every clauses has the variable //delete the clauses that containing a and the variable -a in other clauses } } //pure literal elimination //.................................................................. //there is a variable only exist in a clause and shown one times //Example: //(A) ˄ (A ˅ B) ˄ (¬A ˅ B ˅ C) //Because C appears only once throughout the entire formula., C can be //assigned to “TRUE”. The formula can be simplified to (A) ˄ (A ˅ B) //see each variables contained by how many clauses //save in counter for( int i = 0 ; i < clauses ; i ++ ){ for( int j = 0 ; j < variables ; j ++ ){ if( identical[i][j] > 0 ){ int temp = identical[i][j] ; counter[0][ temp - 1 ] ++ ; }else if ( identical[i][j] < 0 ){ int temp = identical[i][j] ; temp *= -1 ; counter[1][ temp - 1 ] ++ ; }else break ; } } //assign the variable into true if the variable only show in positive or negative //check the counter array to see if there any variable that satisfied for( int i = 0 ; i < 2 ; i ++ ) for( int j = 0 ; j < variables ; j ++ ){ if( ( counter[0][j] != counter[1][j] ) && ( counter[0][j] == 0 || counter[1][j] == 0 ) ){ if( i == 0 ){ aim = ( j + 1 ) ; arrofvariables[ j ] = 1 ; } else{ cout<< "wrong here "<< endl; aim = ( j + 1 ) * -1 ; arrofvariables[ j ] = -1 ; } elimination_PLE ( identical , clauses , variables , aim ) ; } } //if( the whole question is already empty ) //return true ; //if ( there is one clause is empty ) //return false ; //because 0 && with other clauses is 0 } bool DPLL_main ( int identical[][MAX_VARIAbLE] , int clauses , int variables , int forcheck[][MAX_VARIAbLE] , int arrofvariables[] ) { //0 = not assigned yet , 1 = true , -1 = false int counter[ 2 ][ MAX_VARIAbLE ] = { 0 } ; for ( int i = 0 ; i < 2 ; i ++ ) for ( int j = 0 ; j < variables ; j ++ ) counter[ i ][ j ] = 0 ; //for all zero int truth_value = 0 ; bool satisfiable = false ; do{ DPLL_funtion( identical , clauses , variables , arrofvariables , counter ) ; // delete what should be delete DLIS( identical , clauses , variables , counter , arrofvariables) ; //assign and delete truth_value = DPLL_algorithm( forcheck , clauses , variables , arrofvariables ) ; if( identical[0][0] == 0 ) break ; //check satisfied yet }while( truth_value != 1 && truth_value != 2) ; if( truth_value == 1 || truth_value == 2 ) satisfiable = true ; return satisfiable ; } int main( int argc , char *argv[] ) { //open the file first //....get question int variables = 0 , clauses = 0 ; vector< int > numbers ; //compile your .cpp by : g++ -std=c++11 112501557_Final.cpp -o Final.out //when execute your .out by : ./Final.out testcase1.cnf testcase1.txt //argv[0] represent ./Final.out //argv[1] represent testcase1.cnf //argv[2] represent testcase1.txt //1.open the file and get the data stored in a string input_file( argv[ 1 ] , variables , clauses , numbers ) ; int sizeofvector = numbers.size() ; int arrofvariables[ variables ] ; for ( int i = 0 ; i < variables ; i ++ ) arrofvariables [ i ] = 0 ;//all false int identical [ 200 ][ MAX_VARIAbLE ] = { 0 } ; //all zero for( int i = 0 ; i < clauses ; i ++ ) for( int j = 0 ; j < variables ; j ++ ) identical[ i ][ j ] = 0 ; //2. bool satisfiable = false ; //devided into small clause seperate( numbers , sizeofvector , identical , clauses , variables ) ; int forcheck [ 200 ][ MAX_VARIAbLE ] = { 0 } ; //all zero for( int i = 0 ; i < clauses ; i ++ ) for( int j = 0 ; j < variables ; j ++ ) forcheck[ i ][ j ] = 0 ; for( int i = 0 ; i < clauses ; i ++ ) for( int j = 0 ; j <variables ; j ++ ) forcheck[i][j] = identical[i][j] ; //3.calculate the formula //4.get the truth value of clauses satisfiable = DPLL_main( identical , clauses , variables , forcheck , arrofvariables ) ; output_file( argv[ 2 ] , variables , arrofvariables , satisfiable ) ; return 0 ; }
Editor is loading...
Leave a Comment