POJ 3295 Tautology（构造法）

 1 #include<iostream> 
 2 #include<string>
 3 #include<cstring>
 4 using namespace std;
 5 
 6 const int MAXN = 120;
 7 
 8 int sta[MAXN];
 9 char str[MAXN];
10 int p, q, r, s, t;
11 
12 void  judge()
13 {
14     int top = 0;
15     int len = strlen(str);
16     for (int i = len - 1; i >= 0; i--)
17     {
18         if (str[i] == ‘p‘) sta[top++] = p;
19         else if (str[i] == ‘q‘) sta[top++] = q;
20         else if (str[i] == ‘r‘) sta[top++] = r;
21         else if (str[i] == ‘s‘) sta[top++] = s;
22         else if (str[i] == ‘t‘) sta[top++] = t;
23         else if (str[i] == ‘K‘)
24         {
25             int t1 = sta[--top];
26             int t2 = sta[--top];
27             sta[top++] = (t1&&t2);
28         }
29         else if (str[i] == ‘A‘)
30         {
31             int t1 = sta[--top];
32             int t2 = sta[--top];
33             sta[top++] = (t1 || t2);
34         }
35         else if (str[i] == ‘N‘)
36         {
37             int t1 = sta[--top];
38             sta[top++] = (!t1);
39         }
40         else if (str[i] == ‘C‘)
41         {
42             int t1 = sta[--top];
43             int t2 = sta[--top];
44             if (t1 == 1 && t2 == 0)sta[top++] = 0;
45             else sta[top++] = 1;
46         }
47         else if (str[i] == ‘E‘)
48         {
49             int t1 = sta[--top];
50             int t2 = sta[--top];
51             if ((t1 == 1 && t2 == 1) || (t1 == 0 && t2 == 0)) sta[top++] = 1;
52             else sta[top++] = 0;
53         }
54     }
55 }
56 
57 bool solve()
58 {
59     for (p = 0; p<2; p++)
60     for (q = 0; q<2; q++)
61     for (r = 0; r<2; r++)
62     for (s = 0; s<2; s++)
63     for (t = 0; t<2; t++)
64     {
65         judge();
66         if (sta[0] == 0)return false;
67     }
68     return true;
69 }
70 
71 int main()
72 {
73     //freopen("D:\\txt.txt", "r", stdin);
74     while (gets(str) && str[0] != ‘0‘)
75     {
76         if (solve())  cout << "tautology" << endl;
77         else          cout << "not" << endl;
78     }
79     return 0;
80 }