sat.c

并行程序说明：输出结果为最小生成树的边。运行：本实例中使用了5个处理器

				}
			}
		}
	*Serial=0;  /*变量指针格式化*/
	return FALSE;  /*其它情况,返回假(0)*/
}


/******************************************/ 
/*该函数检查Cnf是否有纯文字
输入：Cnf一个CNF结构，Serial变量的编号
输出：HasPureLiteral取值TRUE或FALSE*/ 
/******************************************/ 
int HasPureLiteral(struct CNF  Cnf,int* Serial)  /*测试CNF是否含有纯文字(参数:CNF式,指向变量的指针)*/
{
	int i,j,k,in_flag=FALSE;  /*标记初始设为假*/
	for(i=0;i<NVARS;i++)  /*在给定的变量数目范围(100)内*/
		if (Cnf.var[i].value==NOVALUE)  /*CNF中相应变量没有值*/
		{
			for(j=0;j<NCLAUSES;j++)  /*在给定的子句数目范围(350)内*/
			{
				for(k=0;k<LENGTH_CLAUSE;k++)  /*在给定的子句长度范围(3)内*/
					if (Cnf.clause[j].lit[k].value==-i) break;  /*子句中相应的文字的值为对应的负值,退出*/
					else if (Cnf.clause[j].lit[k].value==i) in_flag=TRUE;  /*子句中相应的文字的值为对应的正值,标记设为真*/
				if( k < LENGTH_CLAUSE ) break;  /*子句长度小于其最大值(3),退出循环*/
			}
			if(in_flag && j==NCLAUSES)  /*标记为真且在给定的子句数目范围(350)内*/
			{
				*Serial=i;  /*相应变量赋值*/
				return TRUE;  /*返回真(1)*/
			}
		}
	*Serial=0;  /*变量指针格式化*/
	return FALSE;  /*其它情况,返回假(0)*/
}


/******************************************/ 
/*该函数根据变量NO.Serial设置Cnf的值
输入：Cnf一个CNF结构，Serial变量编号*/ 
/******************************************/ 
void UpdateCNF(struct CNF  * Cnf,int Serial)  /*为变量赋新值时更新CNF(参数:CNF式,整型变量)*/
{
	int i,j;
	Cnf->num_uncertain--;  /*CNF式中未赋值数减1*/
	for(i=0;i<NCLAUSES;i++)  /*在给定的子句数目范围(350)内*/
		for(j=0;j<LENGTH_CLAUSE;j++)  /*在给定的子句长度范围(3)内*/
			if (Cnf->clause[i].lit[j].value==Serial || Cnf->clause[i].lit[j].value==-Serial)  /*子句中相应的文字的值为对应的变量正值或负值*/
			{
				Cnf->clause[i].num_unassigned--;  /*子句中未赋值数减1*/			
			if(Cnf->clause[i].lit[j].value==Abs(Serial)&&Cnf->var[Abs(Serial)].value==TRUE  /*子句中相应的文字的值为对应的变量正值且CNF中相应变量为真(1)*/
		|| Cnf->clause[i].lit[j].value==-Abs(Serial) && Cnf->var[Abs(Serial)].value==FALSE)  /*子句中相应的文字的值为对应的变量负值且CNF中相应变量为假(0)*/
					{
						/*printf("this is result %d\n",Cnf->result);*/
						Cnf->clause[i].state_of_satisfied=TRUE;  /*子句设为满足条件*/
					}
					else if (Cnf->clause[i].num_unassigned==0)  /*子句中未赋值文字为0*/
							if(Cnf->clause[i].state_of_satisfied==UNCERTAIN)  /*子句是否满足条件不确定*/
							{
								Cnf->clause[i].state_of_satisfied=FALSE;  /*子句设为不满足条件*/
								Cnf->result=FALSE;  /*CNF结果设为假（0）*/
							}
			}
	for(i=0;i<NCLAUSES;i++)  /*在给定的子句数目范围(350)内*/
		if(Cnf->clause[i].state_of_satisfied==FALSE)  /*子句不满足条件*/
		{
			Cnf->result=FALSE;  /*CNF结果设为假（0）*/
			return ;
		}
		else if(Cnf->clause[i].state_of_satisfied==UNCERTAIN)  /*子句是否满足条件不确定 */
		{
			Cnf->result=UNCERTAIN;  /*子句是否满足条件设为不确定*/
			return;
		}
	Cnf->result=TRUE;  /*CNF结果设为真（1）*/
}


/******************************************/ 
/*当我们将一个错误的值赋于一个变量时，我们必须将Cnf转置到可能争取的状态
输入：Cnf一个指向CNF结构的指针，Serial变量的编号
输出：Cnf*/ 
/******************************************/ 
void Reverse(struct CNF * Cnf,int Serial)  /*将CNF从失败信号中恢复出来(参数:CNF式,整型变量)*/
{
	int i,j,k,temp;
	for(i=0;i<NCLAUSES;i++)  /*在给定的子句数目范围(350)内*/
		for(j=0;j<LENGTH_CLAUSE;j++)  /*在给定的子句长度范围(3)内*/
				if (Cnf->clause[i].lit[j].value==Serial)  /*子句中相应的文字的值为对应的变量正值*/
			/*#Serial is in this clause and it is positive*/
				{
			/*judge if this clause can be satisfied*/
					for(k=0;k<LENGTH_CLAUSE;k++)  /*在给定的子句长度范围(3)内*/
						if((temp=Cnf->clause[i].lit[k].value)==Abs(temp) 
							&& Cnf->var[Abs(temp)].value==TRUE  /*子句中相应的文字的值为对应的变量正值且CNF中相应变量为真(1)*/
						||temp==-Abs(temp) && Cnf->var[Abs(temp)].value==FALSE)  /*子句中相应的文字的值为对应的变量负值且CNF中相应变量为假(0)*/
								break;
					if(k==LENGTH_CLAUSE)  /*到达子句末尾*/
	/*if k=LENGTH_CLAUSE then this clause can't be satisfied,so the CNF can't be satisfied*/
					{
						Cnf->clause[i].state_of_satisfied=FALSE;  /*子句是否满足条件设为假（0）*/
						Cnf->result=FALSE;  /*CNF结果设为假（0）*/
					}
				}
				else if (Cnf->clause[i].lit[j].value==-Serial)/*if*/  /*子句中相应的文字的值为对应的变量正值*/
					Cnf->clause[i].state_of_satisfied=TRUE;  /*子句是否满足条件设为真（1）*/
	for(i=0;i<NCLAUSES;i++)  /*在给定的子句数目范围(350)内*/
		if(Cnf->clause[i].state_of_satisfied==FALSE)  /*子句是否满足条件为假（0）*/
		{
			Cnf->result=FALSE;  /*CNF结果设为假（0）*/
			return ;
		}
		else if(Cnf->clause[i].state_of_satisfied==UNCERTAIN)  /*子句是否满足条件为不确定*/
		{
			Cnf->result=UNCERTAIN;  /*CNF结果设为不确定--以后确定*/
			return;
		}
	Cnf->result=TRUE;  /*CNF结果设为真（1）*/
}


/*****************************************/ 
/*该函数返回一个整数的绝对值*/ 
/*****************************************/ 
int Abs(int i)  /*返回变量的绝对值（参数：整型变量）*/
{
	if(i>0) return i;  /*正数情况*/
	return -i;  /*负数情况*/
}


/****************************/ 
/*该函数返回一个整数x的y次方*/ 
/****************************/ 
int Pow(int x,int y)
{
	int i,res=1;
	for(i=0;i<y;i++) res=res*x;
	return res;
}


/******************************************/ 
/*因为CNF结构不是一个MPI类型，当我们要广播它的时候我们必须将其压成另一种形式
输入：Cnf一个CNF结构
输出：一个整数缓冲*/ 
/******************************************/ 
void PackCNF(struct CNF Cnf,int buf[])  /*将CNF打包到整型缓冲--便于MPI广播（参数：CNF式，整型缓存）*/
{
	int i=0,j,k;
	buf[i++]=Cnf.num_uncertain;  /*整型缓冲第一个元素为CNF式不确定变量数*/
	buf[i++]=Cnf.result;  /*整型缓冲第二个元素为CNF式结果*/
	for(j=0;j<NVARS;j++)  /*在给定的变量数目范围(100)内*/
		buf[i++]=Cnf.var[j].value;  /*给整型缓冲其它元素赋CNF式相应变量的值*/
	for(j=0;j<NCLAUSES;j++)  /*在给定的子句数目范围(350)内*/
	{
		buf[i++]=Cnf.clause[j].num_unassigned;  /*整型缓冲接下来第一个元素为子句不确定文字数*/
		buf[i++]=Cnf.clause[j].state_of_satisfied;  /*整型缓冲接下来第二个元素为子句状态*/
		for(k=0;k<LENGTH_CLAUSE;k++)  /*在给定的子句长度范围(3)内*/
			buf[i++]=Cnf.clause[j].lit[k].value;  /*给整型缓冲其它元素赋子句相应文字的值*/
	}
}


/******************************************/ 
/*该函数是PackCNF函数的反函数
输入：buf一个整数缓冲
输出：pCnf一个指向CNF结构的指针*/ 
/******************************************/ 
void UnpackCNF(struct CNF * pCnf,int buf[])  /*将缓冲中的CNF解包（参数：CNF式，整型缓存）*/
{
	int i=0,j,k;
	pCnf->num_uncertain=buf[i++];  /*CNF式不确定变量数为整型缓冲第一个元素*/
	pCnf->result=buf[i++];  /*CNF式结果为整型缓冲第二个元素*/
	for (j=0;j<NVARS;j++)  /*在给定的变量数目范围(100)内*/
		pCnf->var[j].value=buf[i++];  /*给CNF式相应变量赋整型缓冲其它元素的值*/
	for (j=0;j<NCLAUSES;j++)  /*在给定的子句数目范围(350)内*/
	{
		pCnf->clause[j].num_unassigned=buf[i++];  /*子句不确定文字数为整型缓冲接下来第一个元素*/
		pCnf->clause[j].state_of_satisfied=buf[i++];  /*子句状态为整型缓冲接下来第二个元素*/
		for(k=0;k<LENGTH_CLAUSE;k++)  /*在给定的子句长度范围(3)内*/
			pCnf->clause[j].lit[k].value=buf[i++];  /*给子句相应文字赋整型缓冲其它元素的值*/
	}
}


/******************************************/ 
/*该函数将任务数转换为变量的值
输入：x任务
输出：pCnf一个指向CNF结构的指针*/ 
/******************************************/ 
void SetValue(struct CNF * pCnf,unsigned x)  /*在任务中为变量设值并更新CNF（参数：指向CNF式的指针，无符号整型变量--任务数）*/
{
	int i;
	for (i=0;i<DEPTH;i++)  /*在计算深度范围（5）内*/
	{
		pCnf->var[i].value=GetBits(x,i);  /*CNF式相应变量赋值为任务数*/
		UpdateCNF(pCnf,i);  /*为变量赋新值时更新CNF*/
		if(pCnf->result==TRUE)  /*CNF式结果为真*/
			return;
		else if (pCnf->result==FALSE)  /*CNF式结果为假*/
			return;
	}
}


/******************************************/ 
/*从x右边取出NO.n位
输入：x取出位的源
输出：GetBits取值为０或１*/ 
/******************************************/ 
unsigned GetBits(unsigned x,int n)  /*从变量相应位上取值（参数：无符号整型变量，整型变量--取值位置）*/
{
	return (x>>n) & ~(~0 << 1);  /*从变量相应位上取值*/
}


/******************************************/ 
/*该函数由从进程执行执行，计算该任务的结果并将其送回根进程
输入：Cnf一个CNF结构，ｉ任务*/
/******************************************/ 
void SlaveWork(struct CNF Cnf,unsigned i,int BufVar[])  /*从进程的工作--从0进程接受任务,计算,将结果返回0进程*/
{
		int BufResult;
		SetValue(&Cnf,i); /*,BufVar);*/  /*在任务中为变量设值并更新CNF*/
		if( DavisPutnam(Cnf)==TRUE )  /*子句为SAT*/
		{
			BufResult=TRUE;  /*缓存结果为真（1）*/
			MPI_Send(&BufResult,1,MPI_INT,0,0,MPI_COMM_WORLD);  /*MPI--发送缓存结果到0进程*/
		}
		else  /*子句不为SAT*/
		{
			BufResult=FALSE;  /*缓存结果为假（0）*/
			MPI_Send(&BufResult,1,MPI_INT,0,0,MPI_COMM_WORLD);  /*MPI--发送缓存结果到0进程*/
		}
}


/******************************************/
/*该函数从cnf中选取需要的变量
输入：Cnf一个CNF结构
输出：BufVar变量缓冲*/
/******************************************/
void PickVars(struct CNF Cnf,int BufVar[])  /*从CNF中选取相应变量（参数：CNF式，整型缓存）*/
{
	int i,j,k=0,l=0,m;
	for(i=0;i<DEPTH;i++)  /*在计算深度范围（5）内*/
		if(HasUnitClause(Cnf,&j)==TRUE && NotInBuf(BufVar,Abs(j))) /*CNF含有单子句且没有变量在缓冲中*/
		{
			/*printf("\nsingle!");*/
			BufVar[i]=Abs(j);  /*整型缓存中相应的值为单个子句的值*/
		}
		else if (HasPureLiteral(Cnf,&j)==TRUE && NotInBuf(BufVar,Abs(j)))  /*CNF含有纯文字且没有变量在缓冲中*/
		{	
			/*printf("\npure!");*/
			BufVar[i]=Abs(j);  /*整型缓存中相应的值为单个子句的值*/
		}
		else 
		{
			m=Abs(Cnf.clause[k].lit[l].value);  /*临时变量赋值为子句中相应文字的值*/
			while(!NotInBuf(BufVar,m))  /*当临时变量不在整型缓存中时循环*/
			{
				if (l>LENGTH_CLAUSE)  /*超出子句长度范围（3）*/
				{
					l=0;
					k++;
				}
				else l++;  /*子句中文字序号增加1*/
				m=Abs(Cnf.clause[k].lit[l].value);  /*临时变量赋值为子句中相应文字的值*/
				/*printf("\nm=%d",m);*/
			}
			BufVar[i]=m;  /*整型缓存中相应元素的值设为临时变量的值*/
		}
}


/******************************************/
/*该函数检查变量I是否在这个缓冲中
输入：Buf包含变量的缓冲，ｉ整数
输出：NotInBuf取值０或１*/
/******************************************/
int NotInBuf(int Buf[],int i)  /*测试变量是否在缓冲中（参数：整型缓存，整型变量）*/
{
	int j;
	for(j=0;j<DEPTH;j++)  /*在计算深度范围（5）内*/
		if (i==Buf[j]) return 0;  /*变量在缓冲中，返回0--判断时为假*/
	return 1;  /*变量不在缓冲中，返回1--判断时为真*/
}