#include <iostream> #include <string> #include <algorithm> using namespace std; int clause[64][64]; bool satisfied[64]; int64_t satisfaction = 0; int main() { ios_base::sync_with_stdio( false ); cin.tie( nullptr ); int n; cin >> n; string s; cin.get(); getline( cin, s ); reverse( s.begin(), s.end() ); while( !s.empty() ) { static int x = 0; static bool number = false; static bool negation = false; static int val = 0; char c = s.back(); s.pop_back(); if( number ) { if( '0' <= c && c <= '9' ) { val *= 10; val += c - '0'; } else if( c == ')' || c == ' ' ) { if( negation ) clause[x][val-1] = -1; else clause[x][val-1] = 1; number = false; negation = false; val = 0; if( c == ')' ) ++x; } else exit(113); } else { if( c == ')' ) ++x; else if( c == '~' ) negation = true; else if( c == 'x' ) number = true; } } for( uint64_t mask = 0; mask <= (1ull<<n)-1; ++mask ) { for( uint64_t i=0; i < n; ++i ) { for( int x = 0; x < n; ++x ) if( mask & (1ull<<i) ) //x_i is 1 { if( clause[x][i] == 1 ) satisfied[x] = true; } else if( clause[x][i] == -1 ) satisfied[x] = true; } bool sat = true; for( int x = 0; x < n; ++x ) { if( !satisfied[x] ) sat = false; else satisfied[x] = false; } satisfaction += sat; } cout<<satisfaction; return 0; }
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 | #include <iostream> #include <string> #include <algorithm> using namespace std; int clause[64][64]; bool satisfied[64]; int64_t satisfaction = 0; int main() { ios_base::sync_with_stdio( false ); cin.tie( nullptr ); int n; cin >> n; string s; cin.get(); getline( cin, s ); reverse( s.begin(), s.end() ); while( !s.empty() ) { static int x = 0; static bool number = false; static bool negation = false; static int val = 0; char c = s.back(); s.pop_back(); if( number ) { if( '0' <= c && c <= '9' ) { val *= 10; val += c - '0'; } else if( c == ')' || c == ' ' ) { if( negation ) clause[x][val-1] = -1; else clause[x][val-1] = 1; number = false; negation = false; val = 0; if( c == ')' ) ++x; } else exit(113); } else { if( c == ')' ) ++x; else if( c == '~' ) negation = true; else if( c == 'x' ) number = true; } } for( uint64_t mask = 0; mask <= (1ull<<n)-1; ++mask ) { for( uint64_t i=0; i < n; ++i ) { for( int x = 0; x < n; ++x ) if( mask & (1ull<<i) ) //x_i is 1 { if( clause[x][i] == 1 ) satisfied[x] = true; } else if( clause[x][i] == -1 ) satisfied[x] = true; } bool sat = true; for( int x = 0; x < n; ++x ) { if( !satisfied[x] ) sat = false; else satisfied[x] = false; } satisfaction += sat; } cout<<satisfaction; return 0; } |