poj3295

WFF 'N PROOF is a logic game played with dice. Each die has six faces representing some subset of the possible symbols K, A, N, C, E, p, q, r, s, t. A Well-formed formula (WFF) is any string of these symbols obeying the following rules:

p, q, r, s, and t are WFFs
if w is a WFF, Nw is a WFF
if w and x are WFFs, Kwx, Awx, Cwx, and Ewx are WFFs.

The meaning of a WFF is defined as follows:

p, q, r, s, and t are logical variables that may take on the value 0 (false) or 1 (true).
K, A, N, C, E mean and, or, not, implies, and equals as defined in the truth table below.

Definitions of K, A, N, C, and E

w x	Kwx	Awx	Nw	Cwx	Ewx
1 1	1	1	0	1	1
1 0	0	1	0	0	0
0 1	0	1	1	1	0
0 0	0	0	1	1	1

A tautology is a WFF that has value 1 (true) regardless of the values of its variables. For example, ApNp is a tautology because it is true regardless of the value of p. On the other hand, ApNq is not, because it has the value 0 for p=0, q=1.

You must determine whether or not a WFF is a tautology.

Input consists of several test cases. Each test case is a single line containing a WFF with no more than 100 symbols. A line containing 0 follows the last case.

For each test case, output a line containing tautology or not as appropriate.

Waterloo Local Contest, 2006.9.30

代码

#include<stdio.h>
#include<string.h>
#include<stack>
#include<iostream>
#include<algorithm>
using namespace std;
char str[200];
int p,q,r,s,t;
stack<int>Q;
void instack(char c){
       if(c=='p')
       Q.push(p);
       else if(c=='q')
       Q.push(q);
       else if(c=='r')
       Q.push(r);
       else if(c=='s')
       Q.push(s);
       else if(c=='t')
       Q.push(t);
       else
       return;
}
void calculate(char c){
    int a,b,temp;
     if(c=='K'){
         a=Q.top();
         Q.pop();
         b=Q.top();
         Q.pop();
         temp=a&b;
         Q.push(temp);
     }
     else if(c=='A'){
         a=Q.top();
         Q.pop();
         b=Q.top();
         Q.pop();
         temp=a||b;
         Q.push(temp);
     }
     else if(c=='E'){
        a=Q.top();
         Q.pop();
         b=Q.top();
         Q.pop();
         temp=(a==b);
         Q.push(temp);
     }
     else if(c=='C'){
      a=Q.top();
         Q.pop();
         b=Q.top();
         Q.pop();
         temp=(!a)||b;
         Q.push(temp);
     }
     else if(c=='N'){
         a=Q.top();
         Q.pop();
         temp=!a;
         Q.push(temp);
     }
     else
     return ;
}
int main(){
    while(scanf("%s",str)!=EOF){
        getchar();
       if(strcmp(str,"0")==0)
       break;
       int len=strlen(str);
       int flag;
       for( p=0;p<=1;p++){
           for( q=0;q<=1;q++){
               for(r=0;r<=1;r++){
                   for( s=0;s<=1;s++){
                       for( t=0;t<=1;t++){
                            flag=0;
                           for(int i=len-1;i>=0;i--){
                               if(str[i]=='p'||str[i]=='q'||str[i]=='r'||str[i]=='s'||str[i]=='t')
                                  instack(str[i]);
                                  else
                                  calculate(str[i]);
                           }
                           int ans=Q.top();
                           Q.pop();
                           if(ans==0){
                              flag=1;
                              break;
                           }

                       }
                       if(flag) break;
                   }
                    if(flag) break;
               }
                if(flag) break;
           }
            if(flag) break;
       }
       if(flag)
       printf("not ");
       else
       printf("tautology ");
       memset(str,0,sizeof(str));
    }
    return 0;
}

Time Limit: 1000MS		Memory Limit: 65536K
Total Submissions: 10453		Accepted: 3967