****大学
人工智能基础课程实验报告
（20##-20##学年第一学期）
启发式搜索 王浩算法
班 级： ***********
学 号： **********
姓 名： ******
指导教师： ******
成 绩：
20##年 1 月 10 日
实验一 启发式搜索算法
1. 实验内容：
使用启发式搜索算法求解8数码问题。
⑴ 编制程序实现求解8数码问题
算法，采用估价函数
，
其中：
是搜索树中结点
的深度；
为结点的数据库中错放的棋子个数；
为结点的数据库中每个棋子与其目标位置之间的距离总和。
⑵ 分析上述⑴中两种估价函数求解8数码问题的效率差别，给出一个是的上界的
的定义，并测试使用该估价函数是否使算法失去可采纳性。
2. 实验目的
熟练掌握启发式搜索算法及其可采纳性。
3. 实验原理
使用启发式信息知道搜索过程，可以在较大的程度上提高搜索算法的时间效率和空间效率；
启发式搜索的效率在于启发式函数的优劣，在启发式函数构造不好的情况下，甚至在存在解的情形下也可能导致解丢失的现象或者找不到最优解，所以构造一个优秀的启发式函数是前提条件。
4.实验内容
1.问题描述
在一个3*3的九宫格 里有1至8 八个数以及一个空格随机摆放在格子中，如下图：
初始状态 目标状态
现需将图一转化为图二的目标状态，调整的规则为：每次只能将空格与其相邻的一个数字进行交换。实质是要求给出一个合法的移动步骤，实现从初始状态到目标状态的转变。
2.算法分析
(1)解存在性的讨论
对于任意的一个初始状态，是否有解可通过线性代数的有关理论证明。按数组存储后，算出初始状态的逆序数和目标状态的逆序数，若两者的奇偶性一致，则表明有解。
（2）估价函数的确定
通过对八数码的特性的研究，找出一个相对好的函数，f(n)=d(n)+h(n)其中h(n)=2*compare(n)+3*S(n);d(n)为已搜索的深度；（compare（n）为当前节点与目标结点相同位置不相同的个数，S(n)为当前节点的无序度。）
（3）节点的处理
取得一个结点后，判断是否有解，然后对其进行扩展，用估价函数从中取得一个最优节点，依次循环将路径得到，直到取的最后的目标状态。
(4)算法设计
a.输入初始结点，判断解的存在性，并与目标节点对比。
b.若不是目标节点则进行扩展，生成其全部后继节点。
c.对于每个后继节点均求其f(n),并比较。
d.将最小f(n)存入正确路径，并与目标节点进行对比。
e.若不是目标节点则循环执行b，若是目标节点则输出
5实验结果
输入输出：
源代码如下：
#include<stdio.h>
int final[9]={1,2,3,8,0,4,7,6,5};//目标状态节点
int a[1000][9],c[9],e[9],f[9];//路径节点和扩展节点
int deep=1,fn;//深度和估计值
int b[9];
char moveaction;//移动方向
int fnjisuan(int b[9])//估价函数
{
int compare=0,s=0,fn1,d[9];
d[0]=b[0];d[1]=b[1];d[2]=b[2];d[3]=b[5];d[4]=b[8];d[5]=b[7];d[6]=b[6];d[7]=b[3];d[8]=b[4];
for(int i=0;i<9;i++)
{
if(b[i]!=final[i]&&i!=4)compare++;
}for(i=0;i<7;i++)if((d[i+1]-d[i])!=1)s++;
fn1=2*compare+3*s+deep;//估价函数计算结果
return fn1;
}
void show(int c[9])//输出节点
{
for(int i=0;i<9;i++)a[deep][i]=c[i];
for(i=0;i<9;i++){
if((i)%3==0)printf("\n");
printf("%d\t",c[i]);
}
deep++;
printf("\n");
}
int jingguo(int e[9])//测试当前节点是否已经经过 避免回溯
{
for(int i=0;i<deep;i++)
{
int k=0;
for(int j=0;j<9;j++)
if(e[j]==a[i][j])k++;
if(k==9)return 0;
}return 1;
}
int move_up(int c[9],int Zerosign)//上移操作
{
for(int i=0;i<9;i++)c[i]=b[i];
c[Zerosign]=c[Zerosign-3];
c[Zerosign-3]=0;
int fn1=fnjisuan(c);
return fn1;
}
int move_down(int c[9],int Zerosign)//下移操作
{
for(int i=0;i<9;i++)c[i]=b[i];
c[Zerosign]=c[Zerosign+3];
c[Zerosign+3]=0;
int fn1=fnjisuan(c);
return fn1;
}
int move_left(int c[9],int Zerosign)//左移操作
{
for(int i=0;i<9;i++)c[i]=b[i];
c[Zerosign]=c[Zerosign-1];
c[Zerosign-1]=0;
int fn1=fnjisuan(c);
return fn1;
}
int move_right(int c[9],int Zerosign)//右移操作
{
for(int i=0;i<9;i++)c[i]=b[i];
c[Zerosign]=c[Zerosign+1];
c[Zerosign+1]=0;
int fn1=fnjisuan(c);
return fn1;
}
int zuixiao(int fn1,int fn2,int fn3,int fn4)//求最小值
{
int f1,f2,f3;
f1=(fn1<=fn2)?fn1:fn2;
f2=(fn3<=fn4)?fn3:fn4;
f3=(f1<=f2)?f1:f2;
return f3;
}
int cixiao(int fn1,int fn2,int fn3,int fn4)//求次小值
{
int f1,f2,f3,f4;
f1=(fn1<=fn2)?fn1:fn2;
f3=(fn1>fn2)?fn1:fn2;
f2=(fn3<=fn4)?fn3:fn4;
f4=(fn1>fn2)?fn1:fn2;
if(f1<=f2)
{
if(f3<=f2)return f3;
else return f2;
}
else if(f4<=f1)return f4;
else return f1;
}
void budeng(int f1,int f2,int fn1,int fn2,int fn3,int fn4,int Zerosign)//处理估价函数最小值唯一的时候
{
if(f1==fn1)
{
if(moveaction!='d'&&jingguo(c))
{move_up(c,Zerosign);moveaction='u';}
else
{
if(f2==fn2){move_right(c,Zerosign);moveaction='r';}
if(f2==fn3){move_left(c,Zerosign);moveaction='l';}
if(f2==fn4){move_down(c,Zerosign);moveaction='d';}
}
}
if(f1==fn2)
{
if(moveaction!='l'&&jingguo(c)){move_right(c,Zerosign);moveaction='r';}
else{
if(f2==fn3){move_left(c,Zerosign);moveaction='l';}
if(f2==fn4){move_down(c,Zerosign);moveaction='d';}
if(f2==fn1){move_up(c,Zerosign);moveaction='u';}
}
}
if(f1==fn3)
{
if(moveaction!='r'&&jingguo(c)){move_left(c,Zerosign);moveaction='l';}
else{
if(f2==fn1){move_up(c,Zerosign);moveaction='u';}
if(f2==fn2){move_right(c,Zerosign);moveaction='r';}
if(f2==fn4){move_down(c,Zerosign);moveaction='d';}
}
}
if(f1==fn4)
{
if(moveaction!='u'&&jingguo(c)){move_down(c,Zerosign);moveaction='d';}
else{
if(f2==fn2){move_right(c,Zerosign);moveaction='r';}
if(f2==fn3){move_left(c,Zerosign);moveaction='l';}
if(f2==fn1){move_up(c,Zerosign);moveaction='u';}
}
}
}
int ceshi(int k[9])//测试估价函数
{
int fn1=100,fn2=100,fn3=100,fn4=100,f1,Zerosign;
for(int i=0;i<9;i++)
if(0==k[i]){Zerosign=i;break;}
if(Zerosign!=0&&Zerosign!=1&&Zerosign!=2&&moveaction!='d')
fn1=move_up(c,Zerosign);
if(Zerosign!=2&&Zerosign!=5&&Zerosign!=8&&moveaction!='l')
fn2=move_right(c,Zerosign);
if(Zerosign!=0&&Zerosign!=3&&Zerosign!=6&&moveaction!='r')
fn3=move_left(c,Zerosign);
if(Zerosign!=6&&Zerosign!=7&&Zerosign!=8&&moveaction!='u')
fn4=move_down(c,Zerosign);
f1=zuixiao(fn1,fn2,fn3,fn4);
return f1;
}
void move(int c[9])//确定移动方向
{
int fn1=100,fn2=100,fn3=100,fn4=100,f1,f2,Zerosign;
for(int i=0;i<9;i++)
if(0==c[i]){Zerosign=i;break;}
if(Zerosign!=0&&Zerosign!=1&&Zerosign!=2&&moveaction!='d')
fn1=move_up(c,Zerosign);
if(Zerosign!=2&&Zerosign!=5&&Zerosign!=8&&moveaction!='l')
fn2=move_right(c,Zerosign);
if(Zerosign!=0&&Zerosign!=3&&Zerosign!=6&&moveaction!='r')
fn3=move_left(c,Zerosign);
if(Zerosign!=6&&Zerosign!=7&&Zerosign!=8&&moveaction!='u')
fn4=move_down(c,Zerosign);
f1=zuixiao(fn1,fn2,fn3,fn4);
f2=cixiao(fn1,fn2,fn3,fn4);
if(f1==f2)
{
if(fn1==fn2&&fn1==f1)
{
move_up(c,Zerosign);
for(i=0;i<9;i++)e[i]=c[i];
move_right(c,Zerosign);
for(i=0;i<9;i++)f[i]=c[i];
if((ceshi(e)<ceshi(f))&&jingguo(e)){move_up(c,Zerosign);moveaction='u';}
else {move_right(c,Zerosign);moveaction='r';}
}
if(fn1==fn3&&fn1==f1)
{
move_up(c,Zerosign);
for(i=0;i<9;i++)e[i]=c[i];
move_left(c,Zerosign);
for(i=0;i<9;i++)f[i]=c[i];
if((ceshi(e)<ceshi(f))&&jingguo(e)){move_up(c,Zerosign);moveaction='u';}
else {move_left(c,Zerosign);moveaction='l';}
}
if(fn1==fn4&&fn1==f1)
{
move_up(c,Zerosign);
for(i=0;i<9;i++)e[i]=c[i];
move_down(c,Zerosign);
for(i=0;i<9;i++)f[i]=c[i];
if((ceshi(e)<ceshi(f))&&jingguo(e)){move_up(c,Zerosign);moveaction='u';}
else {move_down(c,Zerosign);moveaction='d';}
}
if(fn2==fn3&&fn2==f1)
{
move_right(c,Zerosign);
for(i=0;i<9;i++)e[i]=c[i];
move_left(c,Zerosign);
for(i=0;i<9;i++)f[i]=c[i];
if((ceshi(e)<ceshi(f))&&jingguo(e)){move_right(c,Zerosign);moveaction='r';}
else {move_left(c,Zerosign);moveaction='l';}
}
if(fn2==fn4&&fn2==f1)
{
move_right(c,Zerosign);
for(i=0;i<9;i++)e[i]=c[i];
move_down(c,Zerosign);
for(i=0;i<9;i++)f[i]=c[i];
if((ceshi(e)<ceshi(f))&&jingguo(e)){move_right(c,Zerosign);moveaction='r';}
else {move_down(c,Zerosign);moveaction='d';}
}
if(fn3==fn4&&fn3==f1)
{
move_left(c,Zerosign);
for(i=0;i<9;i++)e[i]=c[i];
move_down(c,Zerosign);
for(i=0;i<9;i++)f[i]=c[i];
if((ceshi(e)<ceshi(f))&&jingguo(e)){move_left(c,Zerosign);moveaction='l';}
else {move_down(c,Zerosign);moveaction='d';}
}
}
else budeng(f1,f2,fn1,fn2,fn3,fn4,Zerosign);
}
int duibi(int c[9]) {//与目标节点比较
for(int i=0;i<9;i++)
if(c[i]!=final[i])
break;
if(i>=9)return 1;
else return 0;
}
int cunzaixing(int c[9]) {//得出初始化节点是否存在路径到目标节点
int nixu=0,nixu1=0,i,j;
for( j=0;j<9;j++)
for(int i=j+1;i<9;i++)
if(final[j]>final[i]&&final[j]!=0&&final[i]!=0)nixu++;
for(j=0;j<9;j++)
for( i=j+1;i<9;i++)
if(c[j]>c[i]&&c[j]!=0&&c[i]!=0)nixu1++;
if((nixu%2)-(nixu1%2)==0)
return 1;
else return 0;
}
void main(){//主函数
int sd=1;
printf("请输入初始结点如（2 8 3 1 6 4 7 0 5）以空格隔开的九个0到9之间的不重复数: \n");
for(int i=0;i<9;i++)
{
scanf("%d",&b[i]);
c[i]=b[i];
}printf("您输入的初始矩阵为：\n");
show(c);
deep--;
if(cunzaixing(c)==0)
printf("此矩阵不存在路径至目标矩阵！\n");
else{
while(!duibi(c)&&deep<100){
move(c);
printf("第%d步移动后的矩阵为：\n",sd++);show(c);
for(int i=0;i<9;i++) b[i]=c[i];}
}
}
实验二 王浩算法的实现
1. 实验内容：
实现命题逻辑框架内的王浩算法。
⑴ 将命题逻辑中的王浩算法推广至下述命题语言的情形之下:
ⅰ 命题变量符号：
，
，
，
ⅱ 逻辑连接符：
，
，
，
，
ⅲ 间隔符：
，
⑵ 在上述⑴中所定义的命题语言中实现王浩算法。
2. 实验目的
熟练掌握命题逻辑中的王浩算法。
3. 实验要求
⑴ 实验题目必须由个人独立完成，允许自行参考相关文献资料，但严禁同学间相互拷贝和抄袭程序以及文档资料。实验结束后一周内上交实验报告和实验文档资料。
⑵ 提交的文档资料包括设计文档和程序源代码。设计文档和程序源代码以书面文档方式提供（用
纸打印）；并提交电子文档备查。
四．数据结构
给定公式，例如：(p1->(q1->r1))->((p1->q1)->(p1->r1))
函数inite主要作用是负责将符号初始化成树的结构。
函数clone复制一棵完全相同的符号树。
函数restruct查找所有&，|， <->等符号，并将其拆分成新形式：！，->符号。
函数searching王浩算法的主要函数。
函数show和output:显示符号串和推理过程。
五．实验结果
公式正确
六．实验总结
通过本次实验，使我更深入的理解了启发式搜索的原理以及实现，对于其优越性有一定认识，加深了对语法分析以及逻辑公式理解，同时熟练掌握了对树的操作。
在编程实现过程中出现过不少问题，通过一次次调试得以解决，并一定程度上提高了我的编程能力，而且让我对人工智能这一课程有了更直接的认知。
王浩算法源代码清单：
#include<stdio.h>
#include<stdlib.h>
#include<string.h>
#define MAX_L 5
int i=0;
int stepcount=1;
enum type{and,or,detrusion,equal,level,variable};
struct node{char *s;type kind;int polar;node *next;node *child;int start;};
struct step{step *child;step *brother;node *lhead;node *rhead;int count;char name[30];};
int inite(char *s,node *head){
int len=strlen(s);
int j=0,polar=1;
node *now=NULL;
node *last=NULL;
if(s==NULL)return 0;
last=head;
while(i<len){
if(s[i]=='|'){ if(!(s[i+1]<='Z'&&s[i+1]>='A'||s[i+1]<='z'&&s[i+1]>='a')&&s[i+1]!='1'&&s[i+1]!='0'&&s[i+1]!='('&&s[i+1]!='!'||i==0)return 0;
now=(node*)malloc(sizeof(node));
now->kind=or;
now->s=NULL;
now->next=NULL;
now->child=NULL;
now->polar=polar;
now->start=0;
if(last->kind==level&&last->child==NULL){
last->child=now;
}else{last->next=now;}
last=now;
i++;
}else if(s[i]=='&'){
if(!(s[i+1]<='Z'&&s[i+1]>='A'||s[i+1]<='z'&&s[i+1]>='a')&&s[i+1]!='1'&&s[i+1]!='0'&&s[i+1]!='('&&s[i+1]!='!'||i==0)
return 0;
now=(node*)malloc(sizeof(node));
now->kind=and;
now->s=NULL;
now->next=NULL;
now->child=NULL;
now->polar=polar;
now->start=0;
if(last->kind==level&&last->child==NULL){
last->child=now;
}else{
last->next=now;
}last=now;
i++;
}else if(s[i]=='!'){
if(!(s[i+1]<='Z'&&s[i+1]>='A'||s[i+1]<='z'&&s[i+1]>='a')&&s[i+1]!='1'&&s[i+1]!='0'&&s[i+1]!='('&&s[i+1]!='!')
return 0;
polar=1-polar;
i++;
}else if(s[i]=='-'){ if(s[i+1]!='>'||(s[i+2]!='!'&&s[i+2]!='('&&!(s[i+2]<='Z'&&s[i+2]>='A'||s[i+2]<='z'&&s[i+2]>='a'))||i==0)
return 0;
now=(node*)malloc(sizeof(node));
now->kind=detrusion;
now->s=NULL;
now->next=NULL;
now->child=NULL;
now->polar=polar;
now->start=0;
if(last->kind==level&&last->child==NULL){
last->child=now;
}else{
last->next=now;
}last=now;
i=i+2;
}else if(s[i]=='<'){ if((s[i+1]!='-'||s[i+2]!='>')||(s[i+3]!='!'&&s[i+3]!='('&&!(s[i+3]<='Z'&&s[i+3]>='A'||s[i+3]<='z'&&s[i+3]>='a')||i==0)&&s[i+3]!='1'&&s[i+3]!='0')
return 0;
now=(node*)malloc(sizeof(node));
now->kind=equal;
now->s=NULL;
now->next=NULL;
now->child=NULL;
now->polar=polar;
now->start=0;
if(last->kind==level&&last->child==NULL){
last->child=now;
}else{
last->next=now;
}last=now;
i=i+3;
}else if(s[i]<='Z'&&s[i]>='A'||s[i]<='z'&&s[i]>='a'){
now=(node*)malloc(sizeof(node));
now->kind=variable;
now->next=NULL;
now->child=NULL;
now->polar=polar;
now->start=0;
now->s=(char*)malloc(MAX_L*sizeof(char));
if(last->kind==level&&last->child==NULL){
last->child=now;
}else{
last->next=now;
}last=now;
j=0;
while((s[i]<='Z'&&s[i]>='A'||s[i]<='z'&&s[i]>='a')||(s[i]<='9'&&s[i]>='0'))
(now->s)[j]=s[i];
i++;
j++;
}if(s[i]!='|'&&s[i]!='&'&&s[i]!='-'&&s[i]!='<'&&s[i]!='\0'&&s[i]!=')')
return 0;
(now->s)[j]='\0';
polar=1;
}else if(s[i]=='1'||s[i]=='0'){
if(s[i+1]!='<'&&s[i+1]!='-'&&s[i+1]!='&'&&s[i+1]!='|'&&s[i+1]!=')'&&s[i+1]!='\0')
return 0;
now=(node*)malloc(sizeof(node));
now->kind=equal;
now->s=(char*)malloc(2*sizeof(char));
(now->s)[0]=s[i];
(now->s)[1]='\0';
now->next=NULL;
now->child=NULL;
now->polar=polar;
now->start=0;
if(last->kind==level&&last->child==NULL){
last->child=now;
}else{
last->next=now;
}last=now;
i++;
}else if(s[i]=='('){
if(!(s[i+1]<='Z'&&s[i+1]>='A'||s[i+1]<='z'&&s[i+1]>='a')&&s[i+1]!='1'&&s[i+1]!='0'&&s[i+1]!='!'&&s[i+1]!='(')
return 0;
now=(node*)malloc(sizeof(node));
now->kind=level;
now->s=NULL;
now->next=NULL;
now->child=NULL;
now->polar=polar;
now->start=0;
if(last->kind==level&&last->child==NULL){
last->child=now;
}else{
last->next=now;
}last=now;
i++;
polar=1;
if(!inite(s,last))return 0;
}else if(s[i]==')'){
if(s[i+1]!='P'&&s[i+1]!='1'&&s[i+1]!='0'&&s[i+1]!='-'&&s[i+1]!='<'&&s[i+1]!='&'&&s[i+1]!='|'&&s[i+1]!='\0'&&s[i+1]!=')')
return 0;
i++;
return 1;
}else return 0;
}return 1;
}
node* clone(node *parent){
node *son=NULL;
if(parent==NULL)return NULL;
son=(node*)malloc(sizeof(node));
son->kind=parent->kind;
son->polar=parent->polar;
son->s=parent->s;
son->start=parent->start;
if(parent->next!=NULL) son->next=clone(parent->next);
else son->next=NULL;
if(parent->child!=NULL) son->child=clone(parent->child);
else son->child=NULL;
return son;
}
void remove(node *head){
node *now=NULL;
now=head;
if(now==NULL)return;
if(now->kind==level&&now->child->kind==variable&&now->child->next==NULL){
now->polar=(now->child->polar==now->polar);
now->child->polar=1;
}
while(now->kind==level&&now->child->kind==level&&now->child->next==NULL){
now->polar=(now->polar==now->child->polar);
now->child=now->child->child;
}
if(now->next!=NULL)remove(now->next);
if(now->child!=NULL)remove(now->child);
}
void restruct(node* head){
node *now=NULL;
node *last=NULL;
node *newone=NULL,*newtwo=NULL,*newthree=NULL,*newfour=NULL,*newnow=NULL;
int order=1;
while(order<=4){
last=head;
now=last->child;
while(now!=NULL){
if((now->kind==variable||now->kind==level)&&order==1){
if(now->next!=NULL&&now->next->kind==and){
newone=(node*)malloc(sizeof(node));
newone->child=NULL;
newone->kind=level;
newone->next=NULL;
newone->polar=0;
newone->s=NULL;
newone->start=0;
if(last->kind==level) last->child=newone;
else last->next=newone;
newone->next=now->next->next->next;
newone->child=now;
now->next->next->polar=1-now->next->next->polar;
now->next->kind=detrusion;
now->next->next->next=NULL;
now=newone;
}else{
last=now;
now=now->next;
}
}else if((now->kind==variable||now->kind==level)&&order==2){
if(now->next!=NULL&&now->next->kind==or){
newone=(node*)malloc(sizeof(node));
newone->child=NULL;
newone->kind=level;
newone->next=NULL;
newone->polar=1;
newone->s=NULL;
newone->start=0;
if(last->kind==level) last->child=newone;
else last->next=newone;
newone->next=now->next->next->next;
newone->child=now;
now->polar=1-now->polar;
now->next->kind=detrusion;
now->next->next->next=NULL;
now=newone;
}else{
last=now;
now=now->next;
}
}else if((now->kind==variable||now->kind==level)&&order==3){
if(now->next!=NULL&&now->next->kind==equal){
newone=(node*)malloc(sizeof(node));
newone->child=NULL;
newone->kind=level;
newone->next=NULL;
newone->polar=0;
newone->s=NULL;
newone->start=0;
newtwo=(node*)malloc(sizeof(node));
newtwo->child=NULL;
newtwo->kind=level;
newtwo->next=NULL;
newtwo->polar=1;
newtwo->s=NULL;
newtwo->start=0;
newthree=(node*)malloc(sizeof(node));
newthree->child=NULL;
newthree->kind=detrusion;
newthree->next=NULL;
newthree->polar=1;
newthree->s=NULL;
newthree->start=0;
newfour=(node*)malloc(sizeof(node));
newfour->child=NULL;
newfour->kind=level;
newfour->next=NULL;
newfour->polar=0;
newfour->s=NULL;
newfour->start=0;
if(last->kind==level) last->child=newone;
else last->next=newone;
newone->next=now->next->next->next;
newone->child=newtwo;
now->next->kind=detrusion;
newtwo->child=now;
now->next->next->next=NULL;
newtwo->next=newthree;
newthree->next=newfour;
newfour->next=NULL;
newnow=clone(now);
newnow->next->kind=detrusion;
newfour->child=newnow->next->next;
newnow->next->next->next=newnow->next;
newnow->next->next=newnow;
newnow->next=NULL;
now=newone;
}else{
last=now;
now=now->next;
}
}else if(now->kind==level&&order==4){
restruct(now);
last=now;
now=now->next;
}else{
last=now;
now=now->next;
}
}order++;
}
}
void show(node *head){
node *now=NULL;
now=head;
while(now!=NULL){
if(now->kind==level){
if(now->polar==0)printf("!");
if(now->start!=1||(now->polar==0&&now->child->next!=NULL))printf("(");
show(now->child);
if(now->start!=1||(now->polar==0&&now->child->next!=NULL))printf(")");
now=now->next;
if(now!=NULL&&now->start==1)putchar(',');
}else if(now->kind==and){
printf("&");
now=now->next;
}else if(now->kind==or){
printf("|");
now=now->next;
}else if(now->kind==detrusion){
printf("->");
now=now->next;
}else if(now->kind==equal){
printf("<->");
now=now->next;
}else if(now->kind==variable){
if(now->polar==0)printf("!");
printf("%s",now->s);
now=now->next;
}
}return;
}
int searching(step *one){
node *now=NULL;
node *last=NULL;
node *newlev=NULL;
node *nnow=NULL;
node *nlast=NULL;
step *nextone=NULL;
step *nexttwo=NULL;
int key=0;
int mark=0;
int re1=1;
int re2=1;
nextone=(step*)malloc(sizeof(step));
nextone->brother=NULL;
nextone->child=NULL;
nextone->lhead=NULL;
nextone->rhead=clone(one->rhead);
nextone->lhead=clone(one->lhead);
strcpy(nextone->name,"");
one->child=nextone;
now=nextone->rhead;
last=now;
while(now!=NULL){
if(now->polar==0){
if(now==nextone->rhead)nextone->rhead=now->next;
else last->next=now->next;
now->next=NULL;
remove(now);
now->next=nextone->lhead;
nextone->lhead=now;
now->polar=1-now->polar;
now->start=1;
now=last->next;
strcpy(one->name,"根据规则1");
mark=1;
key=1;
break;
}else if(now->child->next!=NULL&&now->child->next->kind==detrusion){
nlast=now->child;
nnow=now->child->next;
while(nnow->next->next!=NULL&&nnow->next->next->kind==detrusion){
nlast=nnow->next;
nnow=nnow->next->next;
}
now->polar=1-now->polar;
newlev=(node*)malloc(sizeof(node));
newlev->child=nnow->next;
newlev->kind=level;
newlev->polar=1;
newlev->next=NULL;
newlev->start=1;
nlast->next=NULL;
remove(newlev);
newlev->next=now->next;
now->next=NULL;
remove(now);
now->next=newlev;
strcpy(one->name,"根据规则4");
mark=1;
key=1;
break;
}else{
last=now;
now=now->next;
}
}now=nextone->lhead;
last=now;
while(now!=NULL&&key!=1){
if(now->polar==0){
if(now==nextone->lhead)nextone->lhead=now->next;
else last->next=now->next;
now->next=NULL;
remove(now);
now->next=nextone->rhead;
nextone->rhead=now;
now->polar=1-now->polar;
now->start=1;
now=last->next;
strcpy(one->name,"根据规则2");
mark=1;
key=1;
break;
}else if(now->child->next!=NULL&&now->child->next->kind==detrusion){
nexttwo=(step*)malloc(sizeof(step));
nexttwo->brother=NULL;
nexttwo->child=NULL;
nexttwo->lhead=NULL;
nexttwo->rhead=clone(nextone->rhead);
nexttwo->lhead=clone(nextone->lhead);
strcpy(nexttwo->name,"");
nlast=now->child;
nnow=now->child->next;
while(nnow->next->next!=NULL&&nnow->next->next->kind==detrusion){
nlast=nnow->next;
nnow=nnow->next->next;
}
now->polar=1-now->polar;
now->start=1;
nlast->next=NULL;
remove(now);
now=nexttwo->lhead;
last=now;
while(now->child->next==NULL||now->child->next->kind!=detrusion){
last=now;
now=now->next;
}
nlast=now->child;
nnow=now->child->next;
while(nnow->next->next!=NULL&&nnow->next->next->kind==detrusion){
nlast=nnow->next;
nnow=nnow->next->next;
}
newlev=(node*)malloc(sizeof(node));
newlev->child=nnow->next;
newlev->kind=level;
newlev->polar=1;
newlev->next=NULL;
newlev->start=1;
nlast->next=NULL;
if(now==nexttwo->lhead){
newlev->next=now->next;
nexttwo->lhead=newlev;
}else{
newlev->next=now->next;
last->next=newlev;
}
remove(newlev);
nextone->brother=nexttwo;
strcpy(one->name,"根据规则3");
mark=1;
key=1;
break;
}else{
last=now;
now=now->next;
}
}if(mark==0){
one->child=NULL;
now=one->lhead;
nnow=one->rhead;
while(now!=NULL){
nnow=one->rhead;
while(nnow!=NULL){
if(!strcmp(now->child->s,nnow->child->s))break;
nnow=nnow->next;
}if(nnow!=NULL)break;
now=now->next;
}if(now==NULL)
return 0;
else
return 1;
}re1=searching(nextone);
if(nextone->brother!=NULL)re2=searching(nextone->brother);
if(re1&&re2)
return 1;
else
return 0;
}
void output(step *one){
if(one->child!=NULL)output(one->child);
if(one->brother!=NULL)output(one->brother);
one->count=stepcount;
stepcount++;
printf("(%d) ",one->count);
show(one->lhead);
printf("=>");
show(one->rhead);
printf(" ");
if(one->child!=NULL&&one->child->brother==NULL)printf("由(%d)",one->child->count);
else if(one->child!=NULL&&one->child->brother!=NULL)printf("由(%d)(%d)",one->child->count,one->child->brother->count);
else printf("公理");
puts(one->name);
return;
}
void main(){
char s[100];
node head;
step one;
head.child=NULL;
head.kind=level;
head.next=NULL;
head.polar=1;
head.s=NULL;
head.start=1;
one.brother=NULL;
one.child=NULL;
one.lhead=NULL;
one.rhead=&head;
puts("王浩算法推理器");
while(1){
puts("请输入要证明的公式，变量符号可由大小写字母和数字组成:");
scanf("%s",s);
if(inite(s,&head)){
puts("\n化成蕴含式:");
restruct(&head);
remove(&head);
show(&head);
putchar('\n');
if(searching(&one)){
puts("推导结果为:");
output(&one);
break;
}else {
puts("无法推导出公式");
break;
}
}else puts("输入的公式语法有错误");
getchar();
}
}