#include <iostream> #include <algorithm> #include <vector> #include <string> #include <map> #include <set> #include <queue> #include <stack> #include <cmath> #include <cassert> #include <cstring> #include <bitset> #include <sstream> //#include <bits/stdc++.h> #include <ext/numeric> using namespace std ; using namespace __gnu_cxx ; typedef long long LL ; typedef pair<int,int> PII ; typedef vector<int> VI ; const int INF = 1e9+100 ; const LL INFLL = (LL)INF*INF ; #define REP(i,n) for(int i=0;i<(n);++i) #define ALL(c) c.begin(),c.end() #define FOREACH(i,c) for(auto i=(c).begin();i!=(c).end();++i) #define CLEAR(t) memset(t,0,sizeof(t)) #define PB push_back #define MP make_pair #define FI first #define SE second template<class T1,class T2> ostream& operator<<(ostream &s, const pair<T1,T2> &x) { return s << "(" << x.FI << "," << x.SE << ")" ;} template<class T> ostream& operator<<(ostream &s, const vector<T> &t) { FOREACH(it, t) s << *it << " " ; return s ; } template<class T> ostream& operator<<(ostream &s, const set<T> &t) { FOREACH(it, t) s << *it << " " ; return s ; } template<class T1,class T2> ostream& operator<<(ostream &s, const map<T1, T2> &t) { FOREACH(it, t) s << *it << " " ; return s ; } template<class T1, class T2> T1 conv(const T2 &x) { stringstream sss ; sss << x ; T1 y ; sss >> y ; return y ; } template<class T> void _debug(bool printName, const char* s, const T &x) { if(printName) cerr << s << "=" ; cerr << x << endl ; } void _debug(bool, const char* s, const char*) { for(;*s;s++) if(*s!='"') { cerr << *s ; } cerr << endl ; } template<class T, class... R> void _debug(bool printName, const char* s, const T &x, R... y) { bool o=0, str=(*s=='"') ; for(; o || *s!=',' ; s++) if(*s=='"') o=!o ; else if(printName||str) cerr<<*s ; for(s++;*s && *s==' '; s++) ; if(!str) { if(printName) cerr << "=" ; cerr << x ; if(*s!='"' && printName) cerr << "," ; } cerr << " " ; _debug(printName, s, y...) ; } template<class T> void _coord(const T &x) { cerr << "[" << x << "]" ; } template<class T, class... R> void _coord(const T &x, R... y) { cerr << "[" << x << "]" ; _coord(y...) ; } template<class T, class I> void _val(T &t, const I &i) { cerr << t[i] ; } template<class T, class I, class... J> void _val(T &t, const I &i, J... j) { _val(t[i], j...) ; } #ifndef LOCAL #define CERR(...) #define DEBUG(...) #define DARRAY(...) #else #define CERR(...) if(DFLAG) _debug(0, #__VA_ARGS__, __VA_ARGS__) #define DEBUG(...) if(DFLAG) _debug(1, #__VA_ARGS__, __VA_ARGS__) #define DARRAY(t,...) if(DFLAG) { cerr << #t ; _coord(__VA_ARGS__) ; cerr << " = " ; _val(t,__VA_ARGS__) ; cerr << endl ; } #define DFLAG 1 #endif //////////////////////////////////////////////////////////////////////////////// struct literal { int nr ; bool isNegated ; } ; vector<literal> readClousure() { vector<literal> Clousure ; literal l ; char c ; cin >> c ; assert(c=='(') ; while(true) { cin >> c ; if(c=='~') { l.isNegated = true ; cin >> c ; } else l.isNegated = false ; assert(c=='x') ; cin >> l.nr ; l.nr-- ; Clousure.PB(l) ; cin >> c ; assert(c=='v' || c==')') ; if(c==')') break ; } return Clousure ; } int main() { ios_base::sync_with_stdio(0) ; int n ; cin >> n ; vector<vector<literal>> sat = { readClousure() } ; char c ; while(cin >> c) { assert(c=='^') ; sat.PB(readClousure()) ; } int ret=0 ; for(int mask=0 ; mask<(1<<n) ; mask++) { bool ok=true ; for(int i=0 ; i<sat.size() && ok ; i++) { bool satisfied=false ; for(int j=0 ; j<sat[i].size() && !satisfied ; j++) satisfied |= ((mask>>sat[i][j].nr)&1) ^ sat[i][j].isNegated ; ok &= satisfied ; } ret += ok ; } cout << ret << endl ; }
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 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 | #include <iostream> #include <algorithm> #include <vector> #include <string> #include <map> #include <set> #include <queue> #include <stack> #include <cmath> #include <cassert> #include <cstring> #include <bitset> #include <sstream> //#include <bits/stdc++.h> #include <ext/numeric> using namespace std ; using namespace __gnu_cxx ; typedef long long LL ; typedef pair<int,int> PII ; typedef vector<int> VI ; const int INF = 1e9+100 ; const LL INFLL = (LL)INF*INF ; #define REP(i,n) for(int i=0;i<(n);++i) #define ALL(c) c.begin(),c.end() #define FOREACH(i,c) for(auto i=(c).begin();i!=(c).end();++i) #define CLEAR(t) memset(t,0,sizeof(t)) #define PB push_back #define MP make_pair #define FI first #define SE second template<class T1,class T2> ostream& operator<<(ostream &s, const pair<T1,T2> &x) { return s << "(" << x.FI << "," << x.SE << ")" ;} template<class T> ostream& operator<<(ostream &s, const vector<T> &t) { FOREACH(it, t) s << *it << " " ; return s ; } template<class T> ostream& operator<<(ostream &s, const set<T> &t) { FOREACH(it, t) s << *it << " " ; return s ; } template<class T1,class T2> ostream& operator<<(ostream &s, const map<T1, T2> &t) { FOREACH(it, t) s << *it << " " ; return s ; } template<class T1, class T2> T1 conv(const T2 &x) { stringstream sss ; sss << x ; T1 y ; sss >> y ; return y ; } template<class T> void _debug(bool printName, const char* s, const T &x) { if(printName) cerr << s << "=" ; cerr << x << endl ; } void _debug(bool, const char* s, const char*) { for(;*s;s++) if(*s!='"') { cerr << *s ; } cerr << endl ; } template<class T, class... R> void _debug(bool printName, const char* s, const T &x, R... y) { bool o=0, str=(*s=='"') ; for(; o || *s!=',' ; s++) if(*s=='"') o=!o ; else if(printName||str) cerr<<*s ; for(s++;*s && *s==' '; s++) ; if(!str) { if(printName) cerr << "=" ; cerr << x ; if(*s!='"' && printName) cerr << "," ; } cerr << " " ; _debug(printName, s, y...) ; } template<class T> void _coord(const T &x) { cerr << "[" << x << "]" ; } template<class T, class... R> void _coord(const T &x, R... y) { cerr << "[" << x << "]" ; _coord(y...) ; } template<class T, class I> void _val(T &t, const I &i) { cerr << t[i] ; } template<class T, class I, class... J> void _val(T &t, const I &i, J... j) { _val(t[i], j...) ; } #ifndef LOCAL #define CERR(...) #define DEBUG(...) #define DARRAY(...) #else #define CERR(...) if(DFLAG) _debug(0, #__VA_ARGS__, __VA_ARGS__) #define DEBUG(...) if(DFLAG) _debug(1, #__VA_ARGS__, __VA_ARGS__) #define DARRAY(t,...) if(DFLAG) { cerr << #t ; _coord(__VA_ARGS__) ; cerr << " = " ; _val(t,__VA_ARGS__) ; cerr << endl ; } #define DFLAG 1 #endif //////////////////////////////////////////////////////////////////////////////// struct literal { int nr ; bool isNegated ; } ; vector<literal> readClousure() { vector<literal> Clousure ; literal l ; char c ; cin >> c ; assert(c=='(') ; while(true) { cin >> c ; if(c=='~') { l.isNegated = true ; cin >> c ; } else l.isNegated = false ; assert(c=='x') ; cin >> l.nr ; l.nr-- ; Clousure.PB(l) ; cin >> c ; assert(c=='v' || c==')') ; if(c==')') break ; } return Clousure ; } int main() { ios_base::sync_with_stdio(0) ; int n ; cin >> n ; vector<vector<literal>> sat = { readClousure() } ; char c ; while(cin >> c) { assert(c=='^') ; sat.PB(readClousure()) ; } int ret=0 ; for(int mask=0 ; mask<(1<<n) ; mask++) { bool ok=true ; for(int i=0 ; i<sat.size() && ok ; i++) { bool satisfied=false ; for(int j=0 ; j<sat[i].size() && !satisfied ; j++) satisfied |= ((mask>>sat[i][j].nr)&1) ^ sat[i][j].isNegated ; ok &= satisfied ; } ret += ok ; } cout << ret << endl ; } |