转载请注明出处：
1.SAT问题描述
命题逻辑中合取范式 (CNF) 的可满足性问题 (SAT)是当代理论计算机科学的核心问题, 是一典型的NP 完全问题.在定义可满足性问题SAT之前，先引进一些逻辑符号。
一个 SAT 问题是指: 对于给定的 CNF 是否存在一组关于命题变元的真值指派使得A 为真. 显然, 如果A 为真, 则 CNF 的每个子句中必有一个命题变元为 1 (真) 。
2.Las Vegas算法
Las Vegas 算法是利用随机值做出随机选择的一种概率算法，并且不会产生不正确的答案。在计算过程中所做出的随机选择，可能使算法比其他算法更快地得到所要求的解。 拉斯维加斯算法不会得到不正确的解。一旦用拉斯维加斯算法找到一个解，这个解就一定是正确解。但有时用拉斯维加斯算法找不到解。与蒙特卡罗算法类似，拉斯维加斯算法找到正确解的概率随着它所用的计算时间的增加而提高。对于所求解问题的任一实例，用同一拉斯维加斯算法反复对该实例求解足够多次，可使求解失败的概率任意小。 Las Vegas 算法用来搜索包含目标结点的解空间。它用一些随机选择来移动，而不需要在每个结点都计算一个新的结点。如果成功结点的比例在解空间中相当高，则找到目标结点的概率可能很高。当下一个结点的计算比较困难或者系统化地搜索没有什么必要时，采用Las Vegas 算法，会提高计算的效率。当然，下一个结点的随机选择有可能导致找不到成功的结点，但是我们可以重复多次运行，来提高目标结点的效率。拉斯维加斯算法的一个显著特征是它所作的随机性决策有可能导致算法找不到所需的解，但是通过重复多次运行来克服，在求解NP难问题时，用它往往会收到奇效。
3. Las Vegas +回溯法
正如我们可以将快速排序和插入排序相结合一样，也可以将回溯法和随机算法结合。当未确定变元的个数较多时，则随机确定的真值是可行的概率较大，，随着未确定的变元变少，可能的概率越小，这时就可以使用确定性算法（回溯法）。下面介绍这个混合算法： 先随机确定前k个变元的真值，然后用回溯法来确定后面n-k个变元的真值。其算法描述如下：
BackTrack(int t)int i;if (t > m) return true;dox[t] = i;if (Place(t))if (BackTrack(t+1)) return true;if(i == 2) return false;Place(k)for i = 0 to n dot = doif(M[i][j]>k)t = t+1;elset = t+!(sign[i*3+j]^x[M[i][j]] );if(t<1)return false; return true; SAT_True(x[],success)k = 0;count = 0;while( k < stopST ) doscount = 0;dox[k] = i;if( Place(k))ok[count] = i;count ++;if( count == 0 ) return false;i = ok[rand() % count];x[k] = i;k++; return BackTrack(stopST);
stopST起着关键性的作用，当随机确定的变元真值越多，成功的概率也就越小，就需要多次执行。当随机确定的变元真值越少时，就将大多数时间用在了回溯算法上，stopST到底应该选择一个什么样的值，需要经过多次测试。
代码：// lasvegasBT3SAT.cpp : 定义控制台应用程序的入口点。///********************************* ———————————– Lasvegas+回溯算法解决3SAT问题（C++实现代码）———————————– Author:牧之丶 Date：2014年Email:bzhou84@163.com **********************************/ n=250;const int m=100;int stopST;int M[n][3];int sign[3*n+1];int x[101],y[101];int ok[2];bool Place( int k) {//memset(y,1,101);int temp;/*for( int j = 1; j <= k – 1; j++){y[j]=~x[j];}*/for(int i = 0; i < n; i++){temp=0;for(int j = 0; j < 3; j++){if(M[i][j]>k)temp = temp+1;//未产生的变量在子式中出现都作为真elsetemp = temp+!(sign[i*3+j]^x[M[i][j]] ); //变量在子式中的符号与变量本身取值 异或取反}if(temp<1)return false;}return true; } bool BackTrack(int t){int i;if (t > m)return true;else{for(i = 0; i < 2; i++){x[t] = i;if (Place(t)){if (BackTrack(t+1))return true;}}if(i == 2)return false;}}bool SAT_True(int x[]){int k = 1;int count = 0;int i;while( k < stopST ){count = 0;for( i = 0; i <= 1 ; i++ ){x[k] = i;if( Place(k)){ok[count] = i;count ++;}}if( count == 0 ) return false;i = ok[rand() % count];x[k] = i;k++;}return BackTrack(stopST); }int _tmain(int argc, _TCHAR* argv[]){srand(time(0));for(int i=0;i<n;i++)for(int j=0;j<3;j++)M[i][j] = rand()%m+1;for(int i=1;i<=3*n;i++)sign[i] = rand()%2;memset(x,0,(m+1)*sizeof(int));int k;double run_time = 0.0; //执行时间for( int i = 60; i <= 60; i++){time_t start = clock();k = 1;stopST = i;while(!SAT_True(x) ){k++;if(k > 100000){printf(“failed!\n”);break;}}if(k <= 10000)std::cout << “执行了” << k << “次” << std::endl;time_t end = clock();run_time += (end – start)/CLOCKS_PER_SEC;}printf(“the running time is : %f\n”,run_time);system(“pause”);return 0;}4. 实验结果而消极的人则在每个机会都看到某种忧患。
