1836 永真公式的验证

这学期我们正在学习离散数学，离散数学可以称为计算机数学，是以后很多计算机专业课的基础课。

现在我们尝试用计算机编程去解决离散数学中的问题，既可复习离散数学，又可进行编程实践，可谓两全其美。

任务

编程序判断一个命题公式是否为永真公式 ( 又称为重言式 ) 。

永真公式定义为：给定一个命题公式，若无论对分量作怎样的指派，其对应的真值永为真。

在此，我们限定所出现的命题联结词只有 4 种，即否定 ( 用 not 来表示 ) 、合取 ( 用 and 来表示 ) 、析取 ( 用 or 来表示 ) 、条件联结词 (又称蕴含联结词， 用 then 来表示 ) ，每个原子命题用一个大写英文字母来表示。

输入

一次输入可能包含多组数据。每组数据占用一行。当输入 end 的时候结束。

注意每个联结词前后都有空格， not 位于一行开始的时候前面可以没有空格。原子命题与小括号之间可以没有空格。

联结词的优先级在输入中通过小括号已经全部体现出来，编程时只需判断小括号就可以了。

每组测试用例输入的字符串长度不超过 1000.

输出

针对每一组输入，如果该命题公式为永真公式，输出 1 ；否则输出 0 。

样例输入

( not P) then (P then Q)

((P or S) and R) or ( not ((P or S) and R))

(P and Q) then M

end

样例输出

1

1

0

模拟题，分情况讨论

#include "stdio.h"
#include "string.h"
#include "math.h"
#define AND 1
#define OR 2
#define THEN 3
#define NOT 4
#define TRUE 1
#define FALSE 0
#define MAX_SIZE 1100void transform(int start_pos,int end_pos,char formular[])
{int i,j,variable[2];    /* variable记录公式中出现的命题变元的值 */int flag;               /* flag 标记该公式中是否含有逻辑运算词 */int op;                 /* op 记录逻辑运算词 */int res;     /* 括号内的值 */j=0;flag=0;for (i=start_pos;i<=end_pos;i++){if ( formular[i]=='0' || formular[i]=='1' ){variable[j++]=formular[i]-48;}if ( formular[i]>='a' && formular[i]<='z' )  /* 遇到逻辑运算词 */{flag=1;/* 记录逻辑运算词 */switch (formular[i]){case 'a':op=AND;i+=2;break;case 'o':op=OR;i+=1;break;case 't':op=THEN;i+=3;break;case 'n':op=NOT;i+=2;break;}}}if ( flag )   /* 包含逻辑运算符 */{switch (op){case AND:res=variable[0] & variable[1];break;case OR:res=variable[0] | variable[1];break;case THEN:res= ( ( variable[0]==1 && variable[1]==0 )? 0 : 1 );break;case NOT:res=( ( variable[0]==1 )? 0 : 1 );break;}}else{res=variable[0];}formular[start_pos]=res+48;for (i=start_pos+1;i<=end_pos;i++){formular[i]=' ';}return ;
}int Judge(char formular[])   /* 判断该公式是否为永真公式，是则返回TRUE */
{int search(char formular[],char F[]);int get_res(char formular[]);char variable[30];      /* 存储各个变元的真值 */char F_var[30];         /* 对应的关系 */char temp[MAX_SIZE];    /* 用真值来替代各个命题变元的字符串 */int n,j;                  /* n的值为该命题公式的命题变元的数量 */int flag;long i,max,temp_i;n=search(formular,F_var);max=pow(2,n)-1;/* 枚举所有情况以确定是否为永真公式 */for (i=0;i<=max;i++){temp_i=i;/* 依次给各个命题变元赋真值 */for (j=n;j>=1;j--){variable[F_var[j]-64]=temp_i%2+48;temp_i=temp_i/2;}/* 替换命题变元 */for (j=0;formular[j]!='\0';j++){if ( formular[j]>='A' && formular[j]<='Z' )  /* 遇到命题变元，用真值替换 */{temp[j]=variable[formular[j]-64];}else{temp[j]=formular[j];}}temp[j]='\0';/* 计算在该真值下此命题公式的值 */flag=get_res(temp);if ( flag==FALSE )return FALSE ;}return TRUE ;
}int search(char formular[],char F[])  /* 该函数求一个公式的命题变元的数目，并讲命题变元依次存入F[]的映射关系中 */
{int i,j,count,flag;count=0;for (i=0;formular[i]!='\0';i++){if ( formular[i]>='A' && formular[i]<='Z' ){flag=0;for (j=1;j<=count;j++){if ( F[j]==formular[i] ){flag=1;   /* 说明该命题变元出现过,不记录 */}}if ( !flag ){F[++count]=formular[i];}}}return count ;
}int get_res(char formular[])    /* 计算一个已经给各个命题变元指派真值的命题公式的真值 */
{void transform(int start_pos,int end_pos,char formular[]);int i,j,flag;   /* flag 记录该命题公式中是否还存在括号 */int left,right;  /* 分别记录左括号和右括号的位置 */flag=FALSE;left=0;right=0;for (i=0;formular[i]!='\0';i++){if ( formular[i]=='(' ){left=i;}if ( formular[i]==')' ){flag=TRUE;right=i;break;}}while ( flag ){transform(left+1,right-1,formular);/* 判断，消去括号 */formular[left]=' ';formular[right]=' ';/* 继续判断是否存在括号 */flag=FALSE;for (i=0;formular[i]!='\0';i++){if ( formular[i]=='(' ){left=i;}if ( formular[i]==')' ){flag=TRUE;right=i;break;}}}transform(0,strlen(formular)-1,formular);for (i=0;formular[i]!='\0';i++){if ( formular[i]=='1' ){flag=TRUE;break;}else if ( formular[i]=='0' ){flag=FALSE;break;}}return flag;
}int input(char formular[])    /* 处理输入的函数 */
{gets(formular);if ( formular[0]=='e' )return TRUE;return FALSE ;
}int main(void)
{char formular[MAX_SIZE];int end;end=input(formular);while ( end==FALSE ){printf("%d\n",Judge(formular));;end=input(formular);}return 0;
}