Tautology POJ - 3295
题目链接：https://vjudge.net/problem/POJ-3295
题意：
p
,
q
,
r
,
s
,
t
p,q,r,s,t
p,q,r,s,t都是公式里的变量，
K
,
A
,
N
,
C
,
E
K,A,N,C,E
K,A,N,C,E是运算符。分别代表
a
n
d
,
o
r
,
n
o
t
,
i
m
p
l
i
e
s
,
e
q
u
a
l
and,or,not,implies,equal
and,or,not,implies,equal运算。运算符真值表如下。
p
,
q
,
r
,
s
,
t
p,q,r,s,t
p,q,r,s,t是公式
如果
w
w
w是公式,则
N
w
Nw
Nw也是公式
如果
w
,
x
w,x
w,x是公式，则
K
w
x
,
A
w
x
,
C
w
x
,
E
w
x
Kwx,Awx,Cwx,Ewx
Kwx,Awx,Cwx,Ewx也是公式。
如果一个公式的逻辑值恒为1，这称这个公式为
t
a
u
t
o
l
o
g
y
tautology
tautology。
问题：现在给你一个公式，请你判断它是不是 t a u t o l o g y tautology tautology.
思路：构造法，用栈模拟这个运算过程，算法步骤具体如下：
枚举p,q,r,s,t的取值，复杂度
2
5
2^5
25。
对于每一种取值，从字符串尾部向前遍历，遇到一个字符，如果是遍历，则入栈。如果是运算符，则根据具体的运算符规则操作。（如果是双目运算符，将头两个元素出栈，并作相关运算，将结果压入栈；单目出栈一个，做运算，将结果压入栈）
这样运算到最后栈顶的元素就是运算结果。(你也许需要定义’T’,'F’来在栈中表示1和0)
那么每一种结果都为真，则为
t
a
u
t
o
l
o
g
y
tautology
tautology。否则
n
o
t
not
not
具体见代码：
#include<iostream>
#include<stack>
#include<cmath>
using namespace std;
//栈模拟运算。
stack<char>stk;
bool is_var(char c){
if(c=='p'||c=='q'||c=='r'||c=='s'||c=='t'||c=='T'||c=='F'){
return true;
}
else return false;
}
int bit[7];
int getvalue(char c){
int res;
if(c=='p')res=bit[1];
else if(c=='q')res=bit[2];
else if(c=='r')res=bit[3];
else if(c=='s')res=bit[4];
else if(c=='t')res=bit[5];
else if(c=='T')res=1;
else if(c=='F')res=0;
return res;
}
int N(int x){
int res=1-x;
return res;
}
int C(int w,int x){
int res;
if(w==1&&x==1)res=1;
else if(w==1&&x==0)res=0;
else if(w==0&&x==1)res=1;
else if(w==0&&x==0)res=1;
return res;
}
int main(){
string s;
while(cin>>s){
if(s=="0")break;
int i,h;
int flag=1;
for(h=0;h<=pow(2,5)-1;h++)
{
while(!stk.empty())stk.pop();
//to bit
int tem=5;
int hh=h;
while(1){
bit[tem]=hh&1;
tem--;
hh>>=1;
if(tem==0)break;
}
//pqrst
// p=bit[1];
// q=bit[2];
// r=bit[3];
// s=bit[4];
// t=bit[5];
int len=s.size();
for(i=len-1;i>=0;i--){
//is variable
if(is_var(s[i])){
stk.push(s[i]);
}//is operator
else{
if(s[i]=='K'){
char w=stk.top();
stk.pop();
char x=stk.top();
stk.pop();
int w1,x1;
w1=getvalue(w);
x1=getvalue(x);
int ans=w1&x1;
if(ans)stk.push('T');
else stk.push('F');
}
if(s[i]=='A'){
char w=stk.top();
stk.pop();
char x=stk.top();
stk.pop();
int w1,x1;
w1=getvalue(w);
x1=getvalue(x);
int ans=w1|x1;
if(ans)stk.push('T');
else stk.push('F');
}
if(s[i]=='N'){
char w=stk.top();
stk.pop();
int w1=getvalue(w);
int ans=N(w1);
if(ans)stk.push('T');
else stk.push('F');
}
if(s[i]=='C'){
char w=stk.top();
stk.pop();
char x=stk.top();
stk.pop();
int w1,x1;
w1=getvalue(w);
x1=getvalue(x);
int ans=C(w1,x1);
if(ans)stk.push('T');
else stk.push('F');
}
if(s[i]=='E'){
char w=stk.top();
stk.pop();
char x=stk.top();
stk.pop();
int w1,x1;
w1=getvalue(w);
x1=getvalue(x);
int ans=(w1==x1);
if(ans)stk.push('T');
else stk.push('F');
}
}
}
//stk.top();
int w=stk.top();
int ans=getvalue(w);
if(ans==0){
flag=0;
break;
}
}
if(flag)cout<<"tautology\n";
else cout<<"not\n";
}
return 0;
}