#include<bits/stdc++.h>
#include<cstdio>
using namespace std;
#define R(p, k) for(int i = p; i <= k; i++)
#define RI(i, p, k) for(int i = p; i <= k; i++)
#define IR(k, p) for(int i = k; i >= p; i--)
#define IRI(i, p, k) for(int i = k; i >= p; i--)
#define DEB 0
#if DEB
#define EPRLL(a) fprintf(stderr, "%s %lld ", #a, a);
#define EPR(a) fprintf(stderr, "%s %d ", #a, a);
#define EPRS(a) fprintf(stderr, "%s\n", a);
#define EPRN fprintf(stderr, "\n");
#else
#define EPRLL(a)
#define EPR(a)
#define EPRS(a)
#define EPRN
#endif
const int MN=30, MM=1e6+6;
int n, m=1, result=0;
bool lit[MM];
vector<pair<int, bool> > clause[MM];
char s;
void get_lit(int i){
int a, pos;
scanf("%c", &s); //x lub ~
pos = true;
if(s=='~'){
pos=false;
scanf("%c", &s); //x
}
scanf("%d", &a);
clause[i].push_back(make_pair(a, pos));
EPR(a);
EPR(pos);
}
void check(){
bool ifform=true;
RI(j, 1, m){
bool ifclause=false;
R(0, (signed)clause[j].size()-1){
if(clause[j][i].second == lit[clause[j][i].first]){
ifclause=true;
break;
}
}
if(!ifclause){
ifform=false;
break;
}
}
if(ifform)
result++;
EPR(result);
}
int main(){
scanf("%d", &n);
scanf("%c", &s);
while(scanf("%c", &s) && s!=10){
if(s=='^' || s==' ')
continue;
//zaczynamy klauzule
EPRN;
EPR(m);
get_lit(m);
while(scanf("%c", &s) && s != ')'){ //' ' lub ')'
scanf("%c", &s); //v
scanf("%c", &s); //
get_lit(m);
}
m++;
}
m--;
/* R(1, m){
sort(clause[i].begin(), clause[i].end());
}*/
R(0, (1<<n)-1){
EPRN;
EPR(i);
RI(j, 0, n-1){
lit[j+1]=(i & (1<<j));
EPR(lit[j+1]);
}
check();
}
printf("%d\n", result);
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 95 96 97 98 99 100 101 | #include<bits/stdc++.h> #include<cstdio> using namespace std; #define R(p, k) for(int i = p; i <= k; i++) #define RI(i, p, k) for(int i = p; i <= k; i++) #define IR(k, p) for(int i = k; i >= p; i--) #define IRI(i, p, k) for(int i = k; i >= p; i--) #define DEB 0 #if DEB #define EPRLL(a) fprintf(stderr, "%s %lld ", #a, a); #define EPR(a) fprintf(stderr, "%s %d ", #a, a); #define EPRS(a) fprintf(stderr, "%s\n", a); #define EPRN fprintf(stderr, "\n"); #else #define EPRLL(a) #define EPR(a) #define EPRS(a) #define EPRN #endif const int MN=30, MM=1e6+6; int n, m=1, result=0; bool lit[MM]; vector<pair<int, bool> > clause[MM]; char s; void get_lit(int i){ int a, pos; scanf("%c", &s); //x lub ~ pos = true; if(s=='~'){ pos=false; scanf("%c", &s); //x } scanf("%d", &a); clause[i].push_back(make_pair(a, pos)); EPR(a); EPR(pos); } void check(){ bool ifform=true; RI(j, 1, m){ bool ifclause=false; R(0, (signed)clause[j].size()-1){ if(clause[j][i].second == lit[clause[j][i].first]){ ifclause=true; break; } } if(!ifclause){ ifform=false; break; } } if(ifform) result++; EPR(result); } int main(){ scanf("%d", &n); scanf("%c", &s); while(scanf("%c", &s) && s!=10){ if(s=='^' || s==' ') continue; //zaczynamy klauzule EPRN; EPR(m); get_lit(m); while(scanf("%c", &s) && s != ')'){ //' ' lub ')' scanf("%c", &s); //v scanf("%c", &s); // get_lit(m); } m++; } m--; /* R(1, m){ sort(clause[i].begin(), clause[i].end()); }*/ R(0, (1<<n)-1){ EPRN; EPR(i); RI(j, 0, n-1){ lit[j+1]=(i & (1<<j)); EPR(lit[j+1]); } check(); } printf("%d\n", result); return 0; } |
English