开通博客赚积分
发布资源赚积分
分类

源码开发语言/平台
当前位置：首页 > 源码/资料 > 并行计算 > 查看源码
sat.c
资源名称：mpisourceprogram.rar　[点击查看]
上传用户：jsljixie
上传日期：2013-08-15
资源大小：827k
文件大小：19k
源码类别：

并行计算

开发平台：

Visual C++

sat.c：源码内容
  1. /* FILE : sat.c*/
  2. #include <stdio.h>
  3. #include <stdlib.h>
  4. /*包含有关时间的函数*/
  5. #include <time.h>  
  6. /*mpi库函数*/
  7. #include "mpi.h"  
  8. #include <math.h>
  10. /*变量数目*/
  11. #define NVARS  100
  12. /*子句数目*/
  13. #define NCLAUSES  3
  14. /*每条子句的长度*/
  15. #define LENGTH_CLAUSE  3
  16. /*fgets一行最多读入的字符数*/
  17. #define MAXLINE 60
  18. #define TRUE 1
  19. #define FALSE 0
  20. /*既不是可满足的也不是不可满足的*/
  21. #define UNCERTAIN -1
  22. /*变量值为空*/
  23. #define NOVALUE -1
  24. #define DEPTH 5
  25. /*计算pow(x,y)*/
  26. int Pow(int x, int y);
  27. #define COUNT Pow(2,DEPTH)
  28. #define TASKTAG 11 
  31. /**************/ 
  32. /*主要数据结构*/
  33. /**************/
  34. /*变量*/
  35. struct VARIABLE{
  36. /*变量真值为１,假值为０,无值为－１*/
  37. int value;
  38. };
  39. /*文字*/
  40. struct LITERAL{
  41. /*取值为VAR，－VAR和NOVALUE */
  42. /* VAR取值从１到NVARS*/
  43. int value;
  44. };
  45. /*子句*/
  46. struct CLAUSE{
  47. struct LITERAL lit[LENGTH_CLAUSE];
  48. int num_unassigned;
  49. /*被满足状态取值TRUE，FALSE或UNCERTAIN */
  50. int state_of_satisfied;
  51. };
  52. /*合取范式*/
  53. struct CNF{
  54. struct VARIABLE var[NVARS];
  55. struct CLAUSE clause[NCLAUSES];
  56. int num_uncertain;
  57. /*结果取值为TRUE，FALSE或UNCERTAIN*/
  58. int result;
  59. };
  62. /************/
  63. /*进一步定义*/
  64. /************/
  65. /*测试一个子句是否可满足*/
  66. int DavisPutnam();
  67. /*当赋予一个新值时更新结构ＣＮＦ*/
  68. void UpdateCNF();
  69. /*检查该ＣＮＦ是否只有单一字句*/
  70. int HasUnitClause();
  71. /*检查该ＣＮＦ是否有纯文字*/
  72. int HasPureLiteral();
  73. /*从输入文件读数据初始化ＣＮＦ*/
  74. void InitCNF();
  75. /*从失败记号恢复ＣＮＦ*/
  76. void Reverse();
  77. /*返回一个整数的绝对值*/
  78. int Abs();
  79. /*将ＣＮＦ打包到一个整数缓冲*/
  80. void PackCNF();
  81. /*将一个整数缓冲释放到一个ＣＮＦ*/
  82. void UnpackCNF();
  83. /*根据任务更新该ＣＮＦ*/
  84. void SetValue(); /*从Ｘ中取得ｎ位*/
  85. unsigned GetBits(); /*从根接收任务然后计算并会送结果*/
  86. void SlaveWork();
  87. /*从ＣＮＦ中选变量*/
  88. void PickVars();
  89. /*检查变量是否在缓冲中*/
  90. int NotInBuf(); 
  92. /*主函数*/
  93. int main(int argc,char ** argv)  
  94. {   
  95. struct CNF  Cnf;  /*合取范式CNF*/
  96. int length=2+NVARS+NCLAUSES*(2+LENGTH_CLAUSE)+1;   /*缓冲区长度*/
  97. int buf[length];  /*LENGHT_CLAUSE*NCLAUSE缓冲区*/
  98. MPI_Status status;  /*MPI--状态*/
  99. int i,j,myrank,size,BufResult;
  100. char* CnfFile;  /*输入CNF文件名*/
  101. FILE * in;  /*处理文件*/
  103. MPI_Init(&argc,&argv);  /*MPI--初始化*/
  104. MPI_Comm_rank(MPI_COMM_WORLD,&myrank);  /*MPI--次第号*/
  105. MPI_Comm_size(MPI_COMM_WORLD,&size);  /*MPI--数目*/
  107. /*root processor read data and initiate Cnf,then pack it to buff*/
  108. if(myrank==0)  /*进程0(主进程)*/
  109. {
  110. if (argc<2)  /*保证有两个参数*/
  111. {
  112. printf("You forgot to enter a parametes!n");  /*参数数目不对*/
  113. MPI_Abort(MPI_COMM_WORLD,99);  /*MPI--退出*/
  114. }
  115. CnfFile=argv[1];  /*读取CNF文件名*/
  116. if ((in=fopen(CnfFile,"rt"))==NULL) /*read file*/
  117. {
  118. printf("cannot open the result filen");  /*文件不存在或没有相应的属性*/
  119. MPI_Abort(MPI_COMM_WORLD,99);  /*MPI--退出 */
  120. }
  122. if(myrank==0) printf("NVARS=%d NCLAUSES=%d LENGTH_CLAUSE=%dn",NVARS,NCLAUSES,LENGTH_CLAUSE);
  123. InitCNF(&Cnf,in);  /*从输入文件中读取数据并初始化CNF*/
  124. PackCNF(Cnf,buf);  /*将CNF打包到整型缓冲--便于MPI广播*/
  125. }
  127. /*broadcast buf to all the processors*/
  128. MPI_Barrier(MPI_COMM_WORLD);
  129. MPI_Bcast(buf,length,MPI_INT,0,MPI_COMM_WORLD);  /*MPI--广播CNF包*/
  130. MPI_Barrier(MPI_COMM_WORLD);
  132. /*if it is root processor,distribute the task and wait result from slaves*/
  133. if ( myrank == 0)  /*进程0(主进程)*/
  134. {
  135. double start,end;
  136. start=MPI_Wtime();  /*MPI--时间(开始时间)*/
  137. /*send the first bulk of task*/
  138. for(i=0;i<size-1;i++)  /*对每一个从进程都发送消息*/
  139. MPI_Send(&i,1,MPI_INT,i+1,TASKTAG,MPI_COMM_WORLD);  /*发送CNF信息到从进程*/
  140. while (1)  /*一直执行*/
  141. {              
  142. MPI_Recv(&BufResult,1,MPI_INT,MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&status);  /*从从进程接收结果*/
  143. if ( BufResult==TRUE )  /*SAT算法成功 */
  144. {
  145. end=MPI_Wtime();  /*MPI--时间(结束时间)*/
  146. i=COUNT+10;
  147. printf("nSatisfied! time%fn",end-start);  /*运行时间*/
  148. /*send i as the end signal*/
  149. for(j=0;j<size-1;j++)
  150.     MPI_Send(&i,1,MPI_INT,j+1,TASKTAG,MPI_COMM_WORLD);  /*向从进程发送终止信号*/
  151. break;  /*退出执行*/
  152. }
  153. else if(i>COUNT)  /*SAT算法超出规模*/
  154. {
  155. printf("nUnsatisfied!n");  /*SAT算法失败*/
  156. /*send i as the terminal signal*/
  157. for(j=0;j<size-1;j++)
  158. MPI_Send(&i,1,MPI_INT,j+1,TASKTAG,MPI_COMM_WORLD);  /*向从进程发送终止信号*/
  159. break;  /*退出执行*/
  160. }
  161. else
  162. {
  163. int dest=status.MPI_SOURCE;  /*确定消息发送目的地*/
  164. MPI_Send(&i,1,MPI_INT,dest,TASKTAG,MPI_COMM_WORLD);  /*向从进程发送相应CNF包*/
  165. i++;  /*下一步操作*/
  166. }
  167. }
  168. }
  169. else  /*其它进程(从进程)*/
  170. {
  171. unsigned BufTask;  /*任务数*/
  172. UnpackCNF(&Cnf,buf);  /*将缓冲中的CNF解包*/
  173. while(1)  /*一直执行*/
  174. {
  175. MPI_Recv(&BufTask,1,MPI_INT,0,TASKTAG,MPI_COMM_WORLD,&status);  /*从进程0接受CNF包信息*/
  176. if ( BufTask <= COUNT)  /*未越界*/
  177. SlaveWork(Cnf,BufTask,&BufResult);  /*从0进程接受任务,计算,将结果返回0进程*/
  178. else break;  /*其它情况*/
  179. }
  180. }
  181. MPI_Finalize();  /*MPI--结束*/
  182. return(0);
  183. }
  186. /******************************************/ 
  187. /*该函数从输入文件读入CNF数据并给Cnf赋值
  188. 输入：ｉｎ一包含CNF数据的文件
  189. 输出：ｐＣｎｆ一个指向Cnf结构的指针*/ 
  190. /******************************************/ 
  191. void InitCNF(struct CNF * pCnf,FILE* in)  /*从输入文件中读取数据并初始化CNF(参数:CNF式指针,处理文件)*/
  192. {
  193. char prestr[MAXLINE];  /*文件缓存字符数组*/
  194. int i,j,temp;
  196. for(i=0;i<NVARS;i++)  /*在给定的变量数目范围(100)内*/
  197. pCnf->var[i].value=UNCERTAIN;  /*给CNF式变量赋初值(-1)*/
  199. for (i=0;i<NCLAUSES;i++) {  /*在给定的子句数目范围(350)内*/
  200. for (j=0;j<LENGTH_CLAUSE;j++) {  /*在给定的子句长度范围(3)内*/
  201. fscanf(in,"%d",&pCnf->clause[i].lit[j].value);  /*给CNF式文字赋初值*/
  202. /* printf("%d ",&ilauses[c].lit[l]); */
  203. }
  204. fscanf(in,"%d",&temp);  /*其它读入的值存入临时变量中*/
  205. /* printf("%d n",temp); */
  206. pCnf->clause[i].num_unassigned=LENGTH_CLAUSE;  /*子句中未赋值数取为子句长度*/
  207. pCnf->clause[i].state_of_satisfied=UNCERTAIN;  /*子句状态取为不确定(-1)*/
  208. }
  209. pCnf->num_uncertain=NVARS;  /*CNF中未赋值数取为变量最大数目(100)*/
  210. pCnf->result=UNCERTAIN;  /*CNF结果取为不确定(-1)*/
  211. fclose(in);  /*关闭处理文件*/
  212. }
  215. /******************************************/ 
  216. /*该函数计算结果是最主要的函数
  217. 输入：Cnf一个CNF结构
  218. 输出：DavisPutnam取值TRUE或FALSE*/ 
  219. /******************************************/ 
  220. int DavisPutnam(struct CNF  Cnf)  /*测试子句是否为SAT(参数:CNF式)*/
  221. {
  222. int Serial;/*number of the var to be signed*/  /*待赋值的变量数*/
  223. /*test if this Cnf has had the result*/
  224. if (Cnf.result==TRUE) return TRUE;  /*如果CNF的一部分的结果取为真,返回真*/
  225. if (Cnf.result==FALSE) return FALSE;  /*如果CNF的一部分的结果取为假,返回假*/
  226. /*test if Cnf has unit clause*/
  227. if (HasUnitClause(Cnf,&Serial)==TRUE )  /*CNF含有单子句*/
  228. {
  229. Cnf.var[Abs(Serial)].value=(Serial>0)?TRUE:FALSE;  /*CNF变量赋值(0或1)*/
  230. printf("nsingle%d",Serial);
  231. UpdateCNF(&Cnf,Abs(Serial));  /*为变量赋新值时更新CNF*/
  232. if (Cnf.result==TRUE) return TRUE;  /*如果CNF的一部分的结果取为真,返回真*/
  233. if (Cnf.result==FALSE) return FALSE;  /*如果CNF的一部分的结果取为假,返回假*/
  234. if (DavisPutnam(Cnf)==TRUE) return TRUE;  /*如果CNF的一部分测试子句后的结果取为真,返回真*/
  235. else return FALSE;  /*其它情况,返回假*/
  236. }
  237. /*test if Cnf has pure literal*/
  238. else if (HasPureLiteral(Cnf,&Serial)==TRUE )  /*CNF含有纯文字*/
  239. {
  240.         Cnf.var[Serial].value=TRUE;  /*CNF变量赋值为真(1)*/
  241. printf("nPure %d",Serial);
  242. UpdateCNF(&Cnf,Serial);  /*为变量赋新值时更新CNF*/
  243. if (Cnf.result==TRUE) return TRUE;  /*如果CNF的一部分的结果取为真,返回真*/
  244. if (Cnf.result==FALSE) return FALSE;  /*如果CNF的一部分的结果取为假,返回假*/
  245. if (DavisPutnam(Cnf)==TRUE) return TRUE;  /*如果CNF的一部分测试子句后的结果取为真,返回真*/
  246. else return FALSE;  /*其它情况,返回假*/
  247. }
  248. /*pick a var without value*/
  249.      else  /*CNF不只含有单个文字且不含有纯文字*/
  250.  {
  251. for(Serial=0;Serial<NVARS;Serial++)  /*在给定的变量数目范围(100)内*/
  252. if (Cnf.var[Serial].value==NOVALUE)  break;  /*CNF式中变量没有值,退出*/
  253. printf("ncommon%d",Serial);
  254. /*first assume this var is TRUE*/
  255. Cnf.var[Serial].value=TRUE;  /*CNF变量赋值为真(1)*/
  256. UpdateCNF(&Cnf,Serial);  /*为变量赋新值时更新CNF*/
  257. if (Cnf.result==TRUE) return TRUE;  /*CNF式中变量值为真(1),返回真(1)*/
  258. else if (Cnf.result==UNCERTAIN)  /*CNF式中变量值不确定*/
  259. if (DavisPutnam(Cnf)==TRUE) return TRUE;  /*如果CNF的一部分测试子句后的结果取为真,返回真*/
  260. /*Else try that #Serial is FALSE*/
  261. Cnf.var[Serial].value=FALSE;  /*CNF变量赋值为真(1)*/
  262. /*update Cnf when #Serial is FALSE*/
  263. Reverse(&Cnf,Serial);  /*将CNF从失败信号中恢复出来*/
  264. if (Cnf.result==TRUE) return TRUE;  /*如果CNF的一部分的结果取为真,返回真*/
  265. if (Cnf.result==FALSE)  return FALSE;  /*如果CNF的一部分的结果取为假,返回假*/
  266. if (DavisPutnam(Cnf)==TRUE) return TRUE;  /*如果CNF的一部分测试子句后的结果取为真,返回真*/
  267.   return FALSE;  /*其它情况,返回假(0)*/
  268.  }
  269. }
  272. /******************************************/ 
  273. /*该函数检查Cnf是否有单元字句
  274. 输入：Cnf一个CNF结构，Serial变量的编号
  275. 输出：HasUnitClause取值为TRUE或FALSE*/ 
  276. /******************************************/ 
  277. int HasUnitClause(struct CNF  Cnf,int *Serial)  /*测试CNF是否含有单子句(参数:CNF式,指向变量的指针)*/
  278. {
  279. int i,j,k;
  280. for (i=0;i<NCLAUSES;i++)  /*在给定的子句数目范围(350)内*/
  281. if (Cnf.clause[i].num_unassigned==1)  /*子句中未赋值数为1*/
  282. {
  283. for(j=0;j<LENGTH_CLAUSE;j++)  /*在给定的子句长度范围(3)内*/
  284. {
  285. k=Cnf.clause[i].lit[j].value;  /*k暂时存放子句中相应的文字的值*/
  286. if (Cnf.var[Abs(k)].value==NOVALUE)  /*CNF中相应变量没有值*/
  287. {
  288. *Serial=k;  /*相应变量赋值*/
  289. return TRUE;  /*返回真(1)*/
  290. }
  291. }
  292. }
  293. *Serial=0;  /*变量指针格式化*/
  294. return FALSE;  /*其它情况,返回假(0)*/
  295. }
  298. /******************************************/ 
  299. /*该函数检查Cnf是否有纯文字
  300. 输入：Cnf一个CNF结构，Serial变量的编号
  301. 输出：HasPureLiteral取值TRUE或FALSE*/ 
  302. /******************************************/ 
  303. int HasPureLiteral(struct CNF  Cnf,int* Serial)  /*测试CNF是否含有纯文字(参数:CNF式,指向变量的指针)*/
  304. {
  305. int i,j,k,in_flag=FALSE;  /*标记初始设为假*/
  306. for(i=0;i<NVARS;i++)  /*在给定的变量数目范围(100)内*/
  307. if (Cnf.var[i].value==NOVALUE)  /*CNF中相应变量没有值*/
  308. {
  309. for(j=0;j<NCLAUSES;j++)  /*在给定的子句数目范围(350)内*/
  310. {
  311. for(k=0;k<LENGTH_CLAUSE;k++)  /*在给定的子句长度范围(3)内*/
  312. if (Cnf.clause[j].lit[k].value==-i) break;  /*子句中相应的文字的值为对应的负值,退出*/
  313. else if (Cnf.clause[j].lit[k].value==i) in_flag=TRUE;  /*子句中相应的文字的值为对应的正值,标记设为真*/
  314. if( k < LENGTH_CLAUSE ) break;  /*子句长度小于其最大值(3),退出循环*/
  315. }
  316. if(in_flag && j==NCLAUSES)  /*标记为真且在给定的子句数目范围(350)内*/
  317. {
  318. *Serial=i;  /*相应变量赋值*/
  319. return TRUE;  /*返回真(1)*/
  320. }
  321. }
  322. *Serial=0;  /*变量指针格式化*/
  323. return FALSE;  /*其它情况,返回假(0)*/
  324. }
  327. /******************************************/ 
  328. /*该函数根据变量NO.Serial设置Cnf的值
  329. 输入：Cnf一个CNF结构，Serial变量编号*/ 
  330. /******************************************/ 
  331. void UpdateCNF(struct CNF  * Cnf,int Serial)  /*为变量赋新值时更新CNF(参数:CNF式,整型变量)*/
  332. {
  333. int i,j;
  334. Cnf->num_uncertain--;  /*CNF式中未赋值数减1*/
  335. for(i=0;i<NCLAUSES;i++)  /*在给定的子句数目范围(350)内*/
  336. for(j=0;j<LENGTH_CLAUSE;j++)  /*在给定的子句长度范围(3)内*/
  337. if (Cnf->clause[i].lit[j].value==Serial || Cnf->clause[i].lit[j].value==-Serial)  /*子句中相应的文字的值为对应的变量正值或负值*/
  338. {
  339. Cnf->clause[i].num_unassigned--;  /*子句中未赋值数减1*/
  340. if(Cnf->clause[i].lit[j].value==Abs(Serial)&&Cnf->var[Abs(Serial)].value==TRUE  /*子句中相应的文字的值为对应的变量正值且CNF中相应变量为真(1)*/
  341. || Cnf->clause[i].lit[j].value==-Abs(Serial) && Cnf->var[Abs(Serial)].value==FALSE)  /*子句中相应的文字的值为对应的变量负值且CNF中相应变量为假(0)*/
  342. {
  343. /*printf("this is result %dn",Cnf->result);*/
  344. Cnf->clause[i].state_of_satisfied=TRUE;  /*子句设为满足条件*/
  345. }
  346. else if (Cnf->clause[i].num_unassigned==0)  /*子句中未赋值文字为0*/
  347. if(Cnf->clause[i].state_of_satisfied==UNCERTAIN)  /*子句是否满足条件不确定*/
  348. {
  349. Cnf->clause[i].state_of_satisfied=FALSE;  /*子句设为不满足条件*/
  350. Cnf->result=FALSE;  /*CNF结果设为假（0）*/
  351. }
  352. }
  353. for(i=0;i<NCLAUSES;i++)  /*在给定的子句数目范围(350)内*/
  354. if(Cnf->clause[i].state_of_satisfied==FALSE)  /*子句不满足条件*/
  355. {
  356. Cnf->result=FALSE;  /*CNF结果设为假（0）*/
  357. return ;
  358. }
  359. else if(Cnf->clause[i].state_of_satisfied==UNCERTAIN)  /*子句是否满足条件不确定 */
  360. {
  361. Cnf->result=UNCERTAIN;  /*子句是否满足条件设为不确定*/
  362. return;
  363. }
  364. Cnf->result=TRUE;  /*CNF结果设为真（1）*/
  365. }
  368. /******************************************/ 
  369. /*当我们将一个错误的值赋于一个变量时，我们必须将Cnf转置到可能争取的状态
  370. 输入：Cnf一个指向CNF结构的指针，Serial变量的编号
  371. 输出：Cnf*/ 
  372. /******************************************/ 
  373. void Reverse(struct CNF * Cnf,int Serial)  /*将CNF从失败信号中恢复出来(参数:CNF式,整型变量)*/
  374. {
  375. int i,j,k,temp;
  376. for(i=0;i<NCLAUSES;i++)  /*在给定的子句数目范围(350)内*/
  377. for(j=0;j<LENGTH_CLAUSE;j++)  /*在给定的子句长度范围(3)内*/
  378. if (Cnf->clause[i].lit[j].value==Serial)  /*子句中相应的文字的值为对应的变量正值*/
  379. /*#Serial is in this clause and it is positive*/
  380. {
  381. /*judge if this clause can be satisfied*/
  382. for(k=0;k<LENGTH_CLAUSE;k++)  /*在给定的子句长度范围(3)内*/
  383. if((temp=Cnf->clause[i].lit[k].value)==Abs(temp) 
  384. && Cnf->var[Abs(temp)].value==TRUE  /*子句中相应的文字的值为对应的变量正值且CNF中相应变量为真(1)*/
  385. ||temp==-Abs(temp) && Cnf->var[Abs(temp)].value==FALSE)  /*子句中相应的文字的值为对应的变量负值且CNF中相应变量为假(0)*/
  386. break;
  387. if(k==LENGTH_CLAUSE)  /*到达子句末尾*/
  388. /*if k=LENGTH_CLAUSE then this clause can't be satisfied,so the CNF can't be satisfied*/
  389. {
  390. Cnf->clause[i].state_of_satisfied=FALSE;  /*子句是否满足条件设为假（0）*/
  391. Cnf->result=FALSE;  /*CNF结果设为假（0）*/
  392. }
  393. }
  394. else if (Cnf->clause[i].lit[j].value==-Serial)/*if*/  /*子句中相应的文字的值为对应的变量正值*/
  395. Cnf->clause[i].state_of_satisfied=TRUE;  /*子句是否满足条件设为真（1）*/
  396. for(i=0;i<NCLAUSES;i++)  /*在给定的子句数目范围(350)内*/
  397. if(Cnf->clause[i].state_of_satisfied==FALSE)  /*子句是否满足条件为假（0）*/
  398. {
  399. Cnf->result=FALSE;  /*CNF结果设为假（0）*/
  400. return ;
  401. }
  402. else if(Cnf->clause[i].state_of_satisfied==UNCERTAIN)  /*子句是否满足条件为不确定*/
  403. {
  404. Cnf->result=UNCERTAIN;  /*CNF结果设为不确定--以后确定*/
  405. return;
  406. }
  407. Cnf->result=TRUE;  /*CNF结果设为真（1）*/
  408. }
  411. /*****************************************/ 
  412. /*该函数返回一个整数的绝对值*/ 
  413. /*****************************************/ 
  414. int Abs(int i)  /*返回变量的绝对值（参数：整型变量）*/
  415. {
  416. if(i>0) return i;  /*正数情况*/
  417. return -i;  /*负数情况*/
  418. }
  421. /****************************/ 
  422. /*该函数返回一个整数x的y次方*/ 
  423. /****************************/ 
  424. int Pow(int x,int y)
  425. {
  426. int i,res=1;
  427. for(i=0;i<y;i++) res=res*x;
  428. return res;
  429. }
  432. /******************************************/ 
  433. /*因为CNF结构不是一个MPI类型，当我们要广播它的时候我们必须将其压成另一种形式
  434. 输入：Cnf一个CNF结构
  435. 输出：一个整数缓冲*/ 
  436. /******************************************/ 
  437. void PackCNF(struct CNF Cnf,int buf[])  /*将CNF打包到整型缓冲--便于MPI广播（参数：CNF式，整型缓存）*/
  438. {
  439. int i=0,j,k;
  440. buf[i++]=Cnf.num_uncertain;  /*整型缓冲第一个元素为CNF式不确定变量数*/
  441. buf[i++]=Cnf.result;  /*整型缓冲第二个元素为CNF式结果*/
  442. for(j=0;j<NVARS;j++)  /*在给定的变量数目范围(100)内*/
  443. buf[i++]=Cnf.var[j].value;  /*给整型缓冲其它元素赋CNF式相应变量的值*/
  444. for(j=0;j<NCLAUSES;j++)  /*在给定的子句数目范围(350)内*/
  445. {
  446. buf[i++]=Cnf.clause[j].num_unassigned;  /*整型缓冲接下来第一个元素为子句不确定文字数*/
  447. buf[i++]=Cnf.clause[j].state_of_satisfied;  /*整型缓冲接下来第二个元素为子句状态*/
  448. for(k=0;k<LENGTH_CLAUSE;k++)  /*在给定的子句长度范围(3)内*/
  449. buf[i++]=Cnf.clause[j].lit[k].value;  /*给整型缓冲其它元素赋子句相应文字的值*/
  450. }
  451. }
  454. /******************************************/ 
  455. /*该函数是PackCNF函数的反函数
  456. 输入：buf一个整数缓冲
  457. 输出：pCnf一个指向CNF结构的指针*/ 
  458. /******************************************/ 
  459. void UnpackCNF(struct CNF * pCnf,int buf[])  /*将缓冲中的CNF解包（参数：CNF式，整型缓存）*/
  460. {
  461. int i=0,j,k;
  462. pCnf->num_uncertain=buf[i++];  /*CNF式不确定变量数为整型缓冲第一个元素*/
  463. pCnf->result=buf[i++];  /*CNF式结果为整型缓冲第二个元素*/
  464. for (j=0;j<NVARS;j++)  /*在给定的变量数目范围(100)内*/
  465. pCnf->var[j].value=buf[i++];  /*给CNF式相应变量赋整型缓冲其它元素的值*/
  466. for (j=0;j<NCLAUSES;j++)  /*在给定的子句数目范围(350)内*/
  467. {
  468. pCnf->clause[j].num_unassigned=buf[i++];  /*子句不确定文字数为整型缓冲接下来第一个元素*/
  469. pCnf->clause[j].state_of_satisfied=buf[i++];  /*子句状态为整型缓冲接下来第二个元素*/
  470. for(k=0;k<LENGTH_CLAUSE;k++)  /*在给定的子句长度范围(3)内*/
  471. pCnf->clause[j].lit[k].value=buf[i++];  /*给子句相应文字赋整型缓冲其它元素的值*/
  472. }
  473. }
  476. /******************************************/ 
  477. /*该函数将任务数转换为变量的值
  478. 输入：x任务
  479. 输出：pCnf一个指向CNF结构的指针*/ 
  480. /******************************************/ 
  481. void SetValue(struct CNF * pCnf,unsigned x)  /*在任务中为变量设值并更新CNF（参数：指向CNF式的指针，无符号整型变量--任务数）*/
  482. {
  483. int i;
  484. for (i=0;i<DEPTH;i++)  /*在计算深度范围（5）内*/
  485. {
  486. pCnf->var[i].value=GetBits(x,i);  /*CNF式相应变量赋值为任务数*/
  487. UpdateCNF(pCnf,i);  /*为变量赋新值时更新CNF*/
  488. if(pCnf->result==TRUE)  /*CNF式结果为真*/
  489. return;
  490. else if (pCnf->result==FALSE)  /*CNF式结果为假*/
  491. return;
  492. }
  493. }
  496. /******************************************/ 
  497. /*从x右边取出NO.n位
  498. 输入：x取出位的源
  499. 输出：GetBits取值为０或１*/ 
  500. /******************************************/ 
  501. unsigned GetBits(unsigned x,int n)  /*从变量相应位上取值（参数：无符号整型变量，整型变量--取值位置）*/
  502. {
  503. return (x>>n) & ~(~0 << 1);  /*从变量相应位上取值*/
  504. }
  507. /******************************************/ 
  508. /*该函数由从进程执行执行，计算该任务的结果并将其送回根进程
  509. 输入：Cnf一个CNF结构，ｉ任务*/
  510. /******************************************/ 
  511. void SlaveWork(struct CNF Cnf,unsigned i,int BufVar[])  /*从进程的工作--从0进程接受任务,计算,将结果返回0进程*/
  512. {
  513. int BufResult;
  514. SetValue(&Cnf,i); /*,BufVar);*/  /*在任务中为变量设值并更新CNF*/
  515. if( DavisPutnam(Cnf)==TRUE )  /*子句为SAT*/
  516. {
  517. BufResult=TRUE;  /*缓存结果为真（1）*/
  518. MPI_Send(&BufResult,1,MPI_INT,0,0,MPI_COMM_WORLD);  /*MPI--发送缓存结果到0进程*/
  519. }
  520. else  /*子句不为SAT*/
  521. {
  522. BufResult=FALSE;  /*缓存结果为假（0）*/
  523. MPI_Send(&BufResult,1,MPI_INT,0,0,MPI_COMM_WORLD);  /*MPI--发送缓存结果到0进程*/
  524. }
  525. }
  528. /******************************************/
  529. /*该函数从cnf中选取需要的变量
  530. 输入：Cnf一个CNF结构
  531. 输出：BufVar变量缓冲*/
  532. /******************************************/
  533. void PickVars(struct CNF Cnf,int BufVar[])  /*从CNF中选取相应变量（参数：CNF式，整型缓存）*/
  534. {
  535. int i,j,k=0,l=0,m;
  536. for(i=0;i<DEPTH;i++)  /*在计算深度范围（5）内*/
  537. if(HasUnitClause(Cnf,&j)==TRUE && NotInBuf(BufVar,Abs(j))) /*CNF含有单子句且没有变量在缓冲中*/
  538. {
  539. /*printf("nsingle!");*/
  540. BufVar[i]=Abs(j);  /*整型缓存中相应的值为单个子句的值*/
  541. }
  542. else if (HasPureLiteral(Cnf,&j)==TRUE && NotInBuf(BufVar,Abs(j)))  /*CNF含有纯文字且没有变量在缓冲中*/
  543. {
  544. /*printf("npure!");*/
  545. BufVar[i]=Abs(j);  /*整型缓存中相应的值为单个子句的值*/
  546. }
  547. else 
  548. {
  549. m=Abs(Cnf.clause[k].lit[l].value);  /*临时变量赋值为子句中相应文字的值*/
  550. while(!NotInBuf(BufVar,m))  /*当临时变量不在整型缓存中时循环*/
  551. {
  552. if (l>LENGTH_CLAUSE)  /*超出子句长度范围（3）*/
  553. {
  554. l=0;
  555. k++;
  556. }
  557. else l++;  /*子句中文字序号增加1*/
  558. m=Abs(Cnf.clause[k].lit[l].value);  /*临时变量赋值为子句中相应文字的值*/
  559. /*printf("nm=%d",m);*/
  560. }
  561. BufVar[i]=m;  /*整型缓存中相应元素的值设为临时变量的值*/
  562. }
  563. }
  566. /******************************************/
  567. /*该函数检查变量I是否在这个缓冲中
  568. 输入：Buf包含变量的缓冲，ｉ整数
  569. 输出：NotInBuf取值０或１*/
  570. /******************************************/
  571. int NotInBuf(int Buf[],int i)  /*测试变量是否在缓冲中（参数：整型缓存，整型变量）*/
  572. {
  573. int j;
  574. for(j=0;j<DEPTH;j++)  /*在计算深度范围（5）内*/
  575. if (i==Buf[j]) return 0;  /*变量在缓冲中，返回0--判断时为假*/
  576. return 1;  /*变量不在缓冲中，返回1--判断时为真*/
  577. }