# poj3295——Tautology（构造法）

2016-12-16 18:58:45来源:CSDN作者:blue_skyrim人点击

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

K、A、N、C、E为逻辑运算符，
K –> and: x && y
A –> or: x || y
N –> not : !x
C –> implies : (!x)||y
E –> equals : x==y

``#include <iostream>#include <cstring>#include <string>#include <vector>#include <queue>#include <cstdio>#include <set>#include <cmath>#include <map>#include <algorithm>#include <stack>#define INF 0x3f3f3f3f#define MAXN 100010#define Mod 10001using namespace std;int p,q,r,s,t;stack<int> sta;char op[200];void fun(){    int len=strlen(op);    for(int i=len-1;i>=0;--i)    {        if(op[i]=='p')            sta.push(p);        else if(op[i]=='q')            sta.push(q);        else if(op[i]=='r')            sta.push(r);        else if(op[i]=='s')            sta.push(s);        else if(op[i]=='t')            sta.push(t);        else if(op[i]=='K')        {            int t1=sta.top();            sta.pop();            int t2=sta.top();            sta.pop();            int te=t1&&t2;            sta.push(te);        }        else if(op[i]=='A')        {            int t1=sta.top();            sta.pop();            int t2=sta.top();            sta.pop();            int te=t1||t2;            sta.push(te);        }        else if(op[i]=='N')        {            int t1=sta.top();            sta.pop();            int te=!t1;            sta.push(te);        }        else if(op[i]=='C')        {            int t1=sta.top();            sta.pop();            int t2=sta.top();            sta.pop();            int te=(!t1)||t2;            sta.push(te);        }        else if(op[i]=='E')        {            int t1=sta.top();            sta.pop();            int t2=sta.top();            sta.pop();            if(t1==t2)                sta.push(1);            else                sta.push(0);        }    }}bool check(){    for(p=0;p<2;++p)        for(q=0;q<2;++q)            for(r=0;r<2;++r)                for(s=0;s<2;++s)                    for(t=0;t<2;++t)                    {                        fun();                        if(sta.top()==0)                            return false;                    }    return true;}int main(){    while(gets(op))    {        if(op[0]=='0')            break;        if(check())            printf("tautology/n");        else            printf("not/n");    }    return 0;}``