转载请注明出处：http://blog.csdn.net/zhoubin1992/article/details/46469557
1.SAT问题描写叙述
命题逻辑中合取范式 (CNF) 的可满足性问题 (SAT)是当代理论计算机科学的核心问题, 是一典型的NP 全然问题.在定义可满足性问题SAT之前。先引进一些逻辑符号。
一个 SAT 问题是指: 对于给定的 CNF 是否存在一组关于命题变元的真值指派使得A 为真. 显然, 假设A 为真, 则 CNF 的每一个子句中必有一个命题变元为 1 (真) 。
2.Las Vegas算法
Las Vegas 算法是利用随机值做出随机选择的一种概率算法，而且不会产生不对的答案。在计算过程中所做出的随机选择，可能使算法比其它算法更快地得到所要求的解。
拉斯维加斯算法不会得到不对的解。一旦用拉斯维加斯算法找到一个解，这个解就一定是正确解。但有时用拉斯维加斯算法找不到解。与蒙特卡罗算法相似，拉斯维加斯算法找到正确解的概率随着它所用的计算时间的添加而提高。
对于所求解问题的任一实例，用同一拉斯维加斯算法反复对该实例求解足够多次，可使求解失败的概率随意小。
Las Vegas 算法用来搜索包括目标结点的解空间。它用一些随机选择来移动，而不须要在每一个结点都计算一个新的结点。假设成功结点的比例在解空间中相当高，则找到目标结点的概率可能非常高。
当下一个结点的计算比較困难或者系统化地搜索没有什么必要时。採用Las Vegas 算法，会提高计算的效率。当然，下一个结点的随机选择有可能导致找不到成功的结点，可是我们能够反复多次运行，来提高目标结点的效率。
拉斯维加斯算法的一个显著特征是它所作的随机性决策有可能导致算法找不到所需的解，可是通过反复多次运行来克服，在求解NP难问题时，用它往往会收到奇效。
3.C++实现代码
// lasvegas3SAT.cpp : 定义控制台应用程序的入口点。
//
/*********************************
-----------------------------------
Lasvegas算法解决3SAT问题（C++实现代码）
-----------------------------------
Author:牧之丶 Date：2014年
Email:[email protected]
**********************************/
#include "stdafx.h"
#include <stdlib.h>
#include <string.h>
#include <time.h>
#include <iostream>
const int n=250;
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 t;
/*for( int j = 1; j <= k - 1; j++)
{
y[j]=~x[j];
}*/
for(int i = 0; i < n; i++)
{
t=0;
for(int j = 0; j < 3; j++)
{
if(M[i][j]>k)
t = t+1;
else
t = t+!(sign[i*3+j]^x[M[i][j]] );
}
if(t<1)
return false;
}
return true;
}
bool SAT_True(int x[])
{
int k = 1;
int count = 0;
int i;
while( k <= 100 )
{
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 true;
}
int _tmain(int argc, _TCHAR* argv[])
{ //反复运行20次
//int ncase = 20;
double run_time = 0.0; //运行时间
double run_num = 0.0; //运行次数
time_t start,end;
srand(time(0));
//while(ncase--)
//{
start = clock();
for(int i=0;i<n;i++)
for(int j=0;j<3;j++)
M[i][j] = rand()%100+1;
for(int i=1;i<=3*n;i++)
sign[i] = rand()%2;
memset(x,0,101*sizeof(int));
int k=1;
while(!SAT_True(x) )
{
k++;
if(k > 100000)
{
printf("failed!\n");
break;
}
}
end = clock();
run_num = k;
run_time += (end - start)/CLOCKS_PER_SEC;
if(k <= 100000)
std::cout << "运行了" << run_num << "次" << std::endl;
//}
printf("the running time is : %f\n", run_time);
system("pause");
return 0;
}
4.实验结果及分析
为了測试Las Vegas 的计算效果, 我们用随机产生的3-SAT 模型(每一个子句的长度 l= 3, 且子句里的变元两两不同) 做实例。每种取值运行20次。考虑有可能找不到解的情况，当搜索次数超过十万次，觉得此例子不可满足。
得到的结果为：
參考文献
[1] 张德富.算法设计与分析（高级教程）[M].国防工业出版社，2007.