POJ-3295-Tautology

Tautology

Time Limit: 1000MS		Memory Limit: 65536K
Total Submissions: 11717		Accepted: 4438

Description

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

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.

Output

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

Sample Input

ApNp
ApNq
0

Sample Output

tautology
not

Source
Waterloo Local Contest, 2006.9.30
#include <stdio.h>
#include<string.h>
#include<math.h>

bool WFF(char s[], int x)
{
int a[5];
for(int i = 4; i>=0; --i)
{
a[i] = x/pow(2, i);
x%=(int)pow(2,i);
}
int len = strlen(s);
int xt[100010],top = 0;
for(int i = len-1; i>=0; --i)
{
if(s[i]>='p'&&s[i]<='t')
xt[++top]= a[s[i]-'p'];
else
{
if(s[i]=='N')xt[top] = !xt[top];
else if(s[i]=='A')
{
xt[top-1] = xt[top]||xt[top-1];
--top;
}
else if(s[i]=='K')
{
xt[top-1] = xt[top]&&xt[top-1];
--top;
}
else if(s[i]=='C')
{
xt[top-1] = (!xt[top-1])||xt[top];
--top;
}
else if(s[i]=='E')
{
if(xt[top-1]==xt[top])xt[top-1] = 1;
else xt[top-1] = 0;
--top;
}
}

}
return xt[1];
}
int main()
{
char s[120],ss[120];
while(~scanf("%s",s)&&strcmp(s, "0"))
{
int flag = 1;
for(int i = 0; i<32; ++i)
{
strcpy(ss,s);
if(!WFF(ss, i))
{
flag = 0;
break;
}
}
if(flag)printf("tautology\n");
else printf("not\n");
}
return 0;
}