/* FILE : sat.c*/#include <stdio.h>#include <stdlib.h>/*包含有關時間的函數*/#include <time.h>  /*mpi庫函數*/#include "mpi.h"  #include <math.h>/*變量數目*/#define NVARS 		100/*子句數目*/#define NCLAUSES 	3/*每條子句的長度*/#define LENGTH_CLAUSE 	3/*fgets一行最多讀入的字符數*/#define	MAXLINE		60#define	TRUE		1#define	FALSE		0/*既不是可滿足的也不是不可滿足的*/#define	UNCERTAIN	-1/*變量值為空*/#define	NOVALUE		-1#define	DEPTH		5/*計算pow(x,y)*/int Pow(int x, int y);#define	COUNT		Pow(2,DEPTH)#define	TASKTAG		11 /**************/ /*主要數據結構*//**************//*變量*/struct VARIABLE{/*變量真值為１,假值為０,無值為－１*/	int value;};/*文字*/struct LITERAL{	/*取值為VAR，－VAR和NOVALUE *//* VAR取值從１到NVARS*/	int value;};/*子句*/struct CLAUSE{	struct LITERAL lit[LENGTH_CLAUSE];	int num_unassigned;	/*被滿足狀態取值TRUE，FALSE或UNCERTAIN */int state_of_satisfied;};/*合取范式*/struct CNF{	struct VARIABLE var[NVARS];	struct CLAUSE clause[NCLAUSES];	int num_uncertain;	/*結果取值為TRUE，FALSE或UNCERTAIN*/	int result;};/************//*進一步定義*//************//*測試一個子句是否可滿足*/int DavisPutnam();/*當賦予一個新值時更新結構ＣＮＦ*/void UpdateCNF();/*檢查該ＣＮＦ是否只有單一字句*/int HasUnitClause();/*檢查該ＣＮＦ是否有純文字*/int HasPureLiteral();/*從輸入文件讀數據初始化ＣＮＦ*/void InitCNF();/*從失敗記號恢復ＣＮＦ*/void Reverse();/*返回一個整數的絕對值*/int Abs();/*將ＣＮＦ打包到一個整數緩沖*/void PackCNF();/*將一個整數緩沖釋放到一個ＣＮＦ*/void UnpackCNF();/*根據任務更新該ＣＮＦ*/void SetValue(); /*從Ｘ中取得ｎ位*/unsigned GetBits(); /*從根接收任務然后計算并會送結果*/void SlaveWork();/*從ＣＮＦ中選變量*/void PickVars();/*檢查變量是否在緩沖中*/int NotInBuf(); /*主函數*/int main(int argc,char ** argv)  {   	struct CNF  Cnf;  /*合取范式CNF*/	int length=2+NVARS+NCLAUSES*(2+LENGTH_CLAUSE)+1;  	/*緩沖區長度*/	int buf[length];  /*LENGHT_CLAUSE*NCLAUSE緩沖區*/	MPI_Status status;  /*MPI--狀態*/	int i,j,myrank,size,BufResult;	char* CnfFile;  /*輸入CNF文件名*/	FILE * in;  /*處理文件*/	MPI_Init(&argc,&argv);  /*MPI--初始化*/	MPI_Comm_rank(MPI_COMM_WORLD,&myrank);  /*MPI--次第號*/	MPI_Comm_size(MPI_COMM_WORLD,&size);  /*MPI--數目*/	/*root processor read data and initiate Cnf,then pack it to buff*/	if(myrank==0)  /*進程0(主進程)*/	{		if (argc<2)  /*保證有兩個參數*/		{			printf("You forgot to enter a parametes!\n");  /*參數數目不對*/			MPI_Abort(MPI_COMM_WORLD,99);  /*MPI--退出*/		}		CnfFile=argv[1];  /*讀取CNF文件名*/		if ((in=fopen(CnfFile,"rt"))==NULL)	/*read file*/		{			printf("cannot open the result file\n");  /*文件不存在或沒有相應的屬性*/			MPI_Abort(MPI_COMM_WORLD,99);  /*MPI--退出 */		}		if(myrank==0) printf("NVARS=%d NCLAUSES=%d LENGTH_CLAUSE=%d\n",NVARS,NCLAUSES,LENGTH_CLAUSE);		InitCNF(&Cnf,in);  /*從輸入文件中讀取數據并初始化CNF*/				PackCNF(Cnf,buf);  /*將CNF打包到整型緩沖--便于MPI廣播*/	}	/*broadcast buf to all the processors*/	MPI_Barrier(MPI_COMM_WORLD);	MPI_Bcast(buf,length,MPI_INT,0,MPI_COMM_WORLD);  /*MPI--廣播CNF包*/	MPI_Barrier(MPI_COMM_WORLD);		/*if it is root processor,distribute the task and wait result from slaves*/	if ( myrank == 0)  /*進程0(主進程)*/	{		double start,end;		start=MPI_Wtime();  /*MPI--時間(開始時間)*/		/*send the first bulk of task*/		for(i=0;i<size-1;i++)  /*對每一個從進程都發送消息*/			MPI_Send(&i,1,MPI_INT,i+1,TASKTAG,MPI_COMM_WORLD);  /*發送CNF信息到從進程*/		while (1)  /*一直執行*/		{	             			MPI_Recv(&BufResult,1,MPI_INT,MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&status);  /*從從進程接收結果*/			if ( BufResult==TRUE )  /*SAT算法成功 */			{				end=MPI_Wtime();  /*MPI--時間(結束時間)*/				i=COUNT+10;				printf("\nSatisfied! time%f\n",end-start);  /*運行時間*/				/*send i as the end signal*/				for(j=0;j<size-1;j++)				    MPI_Send(&i,1,MPI_INT,j+1,TASKTAG,MPI_COMM_WORLD);  /*向從進程發送終止信號*/				break;  /*退出執行*/			}			else if(i>COUNT)  /*SAT算法超出規模*/				{					printf("\nUnsatisfied!\n");  /*SAT算法失敗*/					/*send i as the terminal signal*/					for(j=0;j<size-1;j++)						MPI_Send(&i,1,MPI_INT,j+1,TASKTAG,MPI_COMM_WORLD);  /*向從進程發送終止信號*/					break;  /*退出執行*/				}			else			{				int dest=status.MPI_SOURCE;  /*確定消息發送目的地*/				MPI_Send(&i,1,MPI_INT,dest,TASKTAG,MPI_COMM_WORLD);  /*向從進程發送相應CNF包*/				i++;  /*下一步操作*/			}		}	}	else  /*其它進程(從進程)*/	{		unsigned	BufTask;  /*任務數*/		UnpackCNF(&Cnf,buf);  /*將緩沖中的CNF解包*/		while(1)  /*一直執行*/		{		MPI_Recv(&BufTask,1,MPI_INT,0,TASKTAG,MPI_COMM_WORLD,&status);  /*從進程0接受CNF包信息*/			if ( BufTask <= COUNT)  /*未越界*/				SlaveWork(Cnf,BufTask,&BufResult);  /*從0進程接受任務,計算,將結果返回0進程*/			else break;  /*其它情況*/		}	}	MPI_Finalize();  /*MPI--結束*/	return(0);}/******************************************/ /*該函數從輸入文件讀入CNF數據并給Cnf賦值輸入：ｉｎ一包含CNF數據的文件輸出：ｐＣｎｆ一個指向Cnf結構的指針*/ /******************************************/ void InitCNF(struct CNF * pCnf,FILE* in)  /*從輸入文件中讀取數據并初始化CNF(參數:CNF式指針,處理文件)*/{	char prestr[MAXLINE];  /*文件緩存字符數組*/	int i,j,temp;	for(i=0;i<NVARS;i++)  /*在給定的變量數目范圍(100)內*/		pCnf->var[i].value=UNCERTAIN;  /*給CNF式變量賦初值(-1)*/	for (i=0;i<NCLAUSES;i++) {  /*在給定的子句數目范圍(350)內*/		for (j=0;j<LENGTH_CLAUSE;j++) {  /*在給定的子句長度范圍(3)內*/			fscanf(in,"%d",&pCnf->clause[i].lit[j].value);  /*給CNF式文字賦初值*/			/* printf("%d ",&ilauses[c].lit[l]); */		}		fscanf(in,"%d",&temp);  /*其它讀入的值存入臨時變量中*/		/* printf("%d \n",temp); */		pCnf->clause[i].num_unassigned=LENGTH_CLAUSE;  /*子句中未賦值數取為子句長度*/		pCnf->clause[i].state_of_satisfied=UNCERTAIN;  /*子句狀態取為不確定(-1)*/	}	pCnf->num_uncertain=NVARS;  /*CNF中未賦值數取為變量最大數目(100)*/	pCnf->result=UNCERTAIN;  /*CNF結果取為不確定(-1)*/	fclose(in);  /*關閉處理文件*/}/******************************************/ /*該函數計算結果是最主要的函數輸入：Cnf一個CNF結構輸出：DavisPutnam取值TRUE或FALSE*/ /******************************************/ int DavisPutnam(struct CNF  Cnf)  /*測試子句是否為SAT(參數:CNF式)*/{	int Serial;/*number of the var to be signed*/  /*待賦值的變量數*/	/*test if this Cnf has had the result*/	if (Cnf.result==TRUE) return TRUE;  /*如果CNF的一部分的結果取為真,返回真*/	if (Cnf.result==FALSE) return FALSE;  /*如果CNF的一部分的結果取為假,返回假*/	/*test if Cnf has unit clause*/	if (HasUnitClause(Cnf,&Serial)==TRUE )  /*CNF含有單子句*/	{		Cnf.var[Abs(Serial)].value=(Serial>0)?TRUE:FALSE;  /*CNF變量賦值(0或1)*/		printf("\nsingle%d",Serial);		UpdateCNF(&Cnf,Abs(Serial));  /*為變量賦新值時更新CNF*/		if (Cnf.result==TRUE) return TRUE;  /*如果CNF的一部分的結果取為真,返回真*/		if (Cnf.result==FALSE) return FALSE;  /*如果CNF的一部分的結果取為假,返回假*/		if (DavisPutnam(Cnf)==TRUE) return TRUE;  /*如果CNF的一部分測試子句后的結果取為真,返回真*/		else return FALSE;  /*其它情況,返回假*/	}	/*test if Cnf has pure literal*/	else if (HasPureLiteral(Cnf,&Serial)==TRUE )  /*CNF含有純文字*/		{	        Cnf.var[Serial].value=TRUE;  /*CNF變量賦值為真(1)*/			printf("\nPure %d",Serial);			UpdateCNF(&Cnf,Serial);  /*為變量賦新值時更新CNF*/			if (Cnf.result==TRUE) return TRUE;  /*如果CNF的一部分的結果取為真,返回真*/			if (Cnf.result==FALSE) return FALSE;  /*如果CNF的一部分的結果取為假,返回假*/			if (DavisPutnam(Cnf)==TRUE) return TRUE;  /*如果CNF的一部分測試子句后的結果取為真,返回真*/			else return FALSE;  /*其它情況,返回假*/		}		/*pick a var without value*/	     else  /*CNF不只含有單個文字且不含有純文字*/		 {			for(Serial=0;Serial<NVARS;Serial++)  /*在給定的變量數目范圍(100)內*/				if (Cnf.var[Serial].value==NOVALUE)  break;  /*CNF式中變量沒有值,退出*/			printf("\ncommon%d",Serial);			/*first assume this var is TRUE*/			Cnf.var[Serial].value=TRUE;  /*CNF變量賦值為真(1)*/			UpdateCNF(&Cnf,Serial);  /*為變量賦新值時更新CNF*/			if (Cnf.result==TRUE) return TRUE;  /*CNF式中變量值為真(1),返回真(1)*/			else if (Cnf.result==UNCERTAIN)  /*CNF式中變量值不確定*/				if (DavisPutnam(Cnf)==TRUE) return TRUE;  /*如果CNF的一部分測試子句后的結果取為真,返回真*/			/*Else try that #Serial is FALSE*/			Cnf.var[Serial].value=FALSE;  /*CNF變量賦值為真(1)*/			/*update Cnf when #Serial is FALSE*/			Reverse(&Cnf,Serial);  /*將CNF從失敗信號中恢復出來*/			if (Cnf.result==TRUE) return TRUE;  /*如果CNF的一部分的結果取為真,返回真*/			if (Cnf.result==FALSE) 	return FALSE;  /*如果CNF的一部分的結果取為假,返回假*/			if (DavisPutnam(Cnf)==TRUE) return TRUE;  /*如果CNF的一部分測試子句后的結果取為真,返回真*/ 			return FALSE;  /*其它情況,返回假(0)*/		 }}/******************************************/ /*該函數檢查Cnf是否有單元字句輸入：Cnf一個CNF結構，Serial變量的編號輸出：HasUnitClause取值為TRUE或FALSE*/ /******************************************/ int HasUnitClause(struct CNF  Cnf,int *Serial)  /*測試CNF是否含有單子句(參數:CNF式,指向變量的指針)*/{	int i,j,k;	for (i=0;i<NCLAUSES;i++)  /*在給定的子句數目范圍(350)內*/		if (Cnf.clause[i].num_unassigned==1)  /*子句中未賦值數為1*/		{			for(j=0;j<LENGTH_CLAUSE;j++)  /*在給定的子句長度范圍(3)內*/			{				k=Cnf.clause[i].lit[j].value;  /*k暫時存放子句中相應的文字的值*/				if (Cnf.var[Abs(k)].value==NOVALUE)  /*CNF中相應變量沒有值*/				{					*Serial=k;  /*相應變量賦值*/					return TRUE;  /*返回真(1)*/