轉載請注明出處：http://blog.csdn.net/zhoubin1992/article/details/46507919
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;
else
for i = to do
x[t] = i;
if (Place(t))
if (BackTrack(t+)) return true;
if(i == ) return false;
Place(k)
for i = to n do
t =
for j = to do
if(M[i][j]>k)
t = t+;
else
t = t+!(sign[i*+j]^x[M[i][j]] );
if(t<)
return false;
return true;
SAT_True(x[],success)
k = ;
count = ;
while( k < stopST ) dos
count = ;
for i = to do
x[k] = i;
if( Place(k))
ok[count] = i;
count ++;
if( count == ) return false;
i = ok[rand() % count];
x[k] = i;
k++;
return BackTrack(stopST);
stopST起着關鍵性的作用，當随機确定的變元真值越多，成功的機率也就越小，就需要多次執行。當随機确定的變元真值越少時，就将大多數時間用在了回溯算法上，stopST到底應該選擇一個什麼樣的值，需要經過多次測試。
代碼：
// lasvegasBT3SAT.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=;
const int m=;
int stopST;
int M[n][];
int sign[*n+];
int x[],y[];
int ok[];
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 = ; i < n; i++)
{
temp=;
for(int j = ; j < ; j++)
{
if(M[i][j]>k)
temp = temp+; //未産生的變量在子式中出現都作為真
else
temp = temp+!(sign[i*+j]^x[M[i][j]] ); //變量在子式中的符号與變量本身取值 異或取反
}
if(temp<)
return false;
}
return true;
}
bool BackTrack(int t)
{
int i;
if (t > m)
return true;
else
{
for(i = ; i < ; i++)
{
x[t] = i;
if (Place(t))
{
if (BackTrack(t+))
return true;
}
}
if(i == )
return false;
}
}
bool SAT_True(int x[])
{
int k = ;
int count = ;
int i;
while( k < stopST )
{
count = ;
for( i = ; i <= ; i++ )
{
x[k] = i;
if( Place(k))
{
ok[count] = i;
count ++;
}
}
if( count == ) return false;
i = ok[rand() % count];
x[k] = i;
k++;
}
return BackTrack(stopST);
}
int _tmain(int argc, _TCHAR* argv[])
{
srand(time());
for(int i=;i<n;i++)
for(int j=;j<;j++)
M[i][j] = rand()%m+;
for(int i=;i<=*n;i++)
sign[i] = rand()%;
memset(x,,(m+)*sizeof(int));
int k;
double run_time = ; //執行時間
for( int i = ; i <= ; i++)
{
time_t start = clock();
k = ;
stopST = i;
while(!SAT_True(x) )
{
k++;
if(k > )
{
printf("failed!\n");
break;
}
}
if(k <= )
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 ;
}
4. 實驗結果
經測試stopST=60時執行次數和執行時間均較為理想。
這裡我給出m= 50,n=200時的結果：
【進階算法】Lasvegas+回溯算法解決3SAT問題（C++實作）