转载请注明出处：http://blog.****.net/zhoubin1992/article/details/46453761
------------------------------------------------------
1 SAT问题描写叙述
命题逻辑中合取范式 (CNF)的可满足性问题 (SAT)是当代理论计算机科学的核心问题,是一典型的NP全然问题.在定义可满足性问题SAT之前，先引进一些逻辑符号。
watermark/2/text/aHR0cDovL2Jsb2cuY3Nkbi5uZXQvemhvdWJpbjE5OTI=/font/5a6L5L2T/fontsize/400/fill/I0JBQkFCMA==/dissolve/70/gravity/Center" alt="">
------------------------------------------------------
2 模拟退火算法
模拟退火算法来源于固体退火原理，将固体加温至充分高。再让其徐徐冷却，加温时。固体内部粒子随温升变为无序状，内能增大，而徐徐冷却时粒子渐趋有序，在每一个温度都达到平衡态。最后在常温时达到基态，内能减为最小。用固体退火模拟组合优化问题，将内能E模拟为目标函数值f，温度T演化成控制參数t，即得到解组合优化问题的模拟退火算法：由初始解i和控制參数初值t開始。对当前解反复“产生新解→计算目标函数差→接受或舍弃”的迭代，并逐步衰减t值，算法终止时的当前解即为所得近似最优解，这是基于蒙特卡罗迭代求解法的一种启示式随机搜索过程。
模拟退火算法能够分解为解空间、目标函数和初始解3部分。其基本思想是：
(1)初始化：初始温度T(充分大)，初始解状态s(是算法迭代的起点)。每一个T值的迭代次数L(Markov链长)，衰减准则α，停止准则。
(2)对k=1，……，L做第(3)至第(6)步。
(3)产生新解s′。
(4)计算增量cost=cost(s′)-cost(s)，当中cost(s)为评价函数；
(5)若t′＜0则接受s′作为新的当前解，否则以概率exp(-t′/T)接受s′作为新的当前解。
(6)假设满足终止条件则输出当前解作为最优解，结束程序。否则T逐渐降低，并转第2步运算。
模拟退火算法伪代码例如以下：
<span style="font-size:14px;">choose an initial solution X0 randomly //随机的选择一个初始解X0
give an initial temperature T0 , X ← X0, T ← T0 //初始化温度T0
while the stop criterion is not yet satisfied do //停止准则不满足则
{ for i ← 1 to L do //Markov 链的长度 L
{ pick a solution X'∈N(X) randomly //随机选择临域内一个解X'
Δf ← f(X')-f(X)
if Δf<0 then X ← X'
else X ← X' with probability exp(- Δf/T) }
// 以exp(- Δf/T)的接受概率接受X'
T← g(T) //generally, T ← aT } //温度下降
return X
</span>
------------------------------------------------------
3 C++实现代码
// SA3Sat.cpp : 定义控制台应用程序的入口点。
//
/*********************************
-----------------------------------
模拟退火解决3SAT问题（C++实现代码）
-----------------------------------
Author:牧之丶 Date：2014年
Email:bzhou84@163.com
**********************************/
#include "stdafx.h"
#include <iostream>
#include <time.h>
#include <fstream>
#include <math.h>
using namespace std; #define ANSSIZE 100 int ans[ANSSIZE];
int new_ans[ANSSIZE];
int **x;
int n=100;
int m=430;
int randomi(int a, int b)
{
int c=rand()%(b-a+1)+a;
return c;
} double randomf(double a, double b)
{ double c = (double)(rand()%((int)b-(int)a)) + a + (double)(rand()/(RAND_MAX + 1.0));
return c;
} void Johnson(int n)
{
for (int i = 0 ; i<n ; i++)
{
if ((double)rand()/(RAND_MAX)>0.5)
{
ans[i] = 1;
}
else
{
ans[i] = 0;
}
}
} int satisfied_ans(int m)
{
int count = 0;
int i,j;
for (i = 0 ; i<m ; i++)
{
for (j = 0 ; j<3 ; j++)
{
if (x[i][j]<0)
{
int temp= (-1)*x[i][j];
if (ans[temp-1]==0)
{
count++;
break;
}
}
else if (x[i][j]>0)
{
if (ans[x[i][j]-1]==1)
{
count++;
break;
}
}
}
}
return count;
} int satisfied_new_ans(int m)
{
int count = 0;
int i,j;
for (i = 0 ; i<m ; i++)
{
for (j = 0 ; j<3 ; j++)
{
if (x[i][j]<0)
{
int temp= (-1)*x[i][j];
if (new_ans[temp-1]==0)
{
count++;
break;
}
}
else if (x[i][j]>0)
{
if (new_ans[x[i][j]-1]==1)
{
count++;
break;
}
}
}
}
return count;
} void disturb(int n)
{
for (int j = 0 ; j<n ;j++)
{
new_ans[j] = ans[j];
}
int i = rand()%n;
new_ans[i] = 1-new_ans[i];
} bool accept(int deta,float T)
{
if (deta>0)
{
return 1;
}
else if(((deta<0)&&(exp(deta/T)>randomf(0,1))))
{
return 1;
}
return 0;
} void SA3Sat(int n,int m)
{
int i;
Johnson(n); //初始解
float T = 1000; //初始温度
int L = 100*n;
float T_time=0.001;
while(T>T_time&&satisfied_ans(m)!=m)
{
for (i= 0 ; i<L ; i++)
{
disturb(n);
// for (i = 0 ; i<n ; i++)
// {
// cout<<ans[i]<<" ";
// }
int deta = satisfied_new_ans(m)-satisfied_ans(m);
if (accept(deta,T))
{
for (int j = 0 ; j<n ; j++)
{
ans[j] = new_ans[j];
}
}
}
T = 0.98*T;
}
} int _tmain(int argc, _TCHAR* argv[])
{
// int n,m,i,j;
// cin>>n>>m; //3SAT问题
// x = new int*[m];
// for (i = 0 ; i<m ; i++)
// {
// x[i] = new int[3];
// }
// for (i = 0 ; i<m ; i++) //子句
// {
// for (j = 0 ; j<3 ; j++)
// {
// cin>>x[i][j];
// }
// }
double run_time = 0.0; //执行时间
time_t start,end;
start = clock();
ifstream fin;
fin.open("10.txt");
int i,j,t;
x = new int*[m];
for (i = 0 ; i<m ; i++)
{
x[i] = new int[3];
}
for (i = 0 ; i<m ; i++)
{
for (j = 0 ; j<3 ; j++)
{
fin>>x[i][j];
}
fin>>t;
}
fin.close(); srand((unsigned)time(NULL));
SA3Sat(n,m);
cout<<"可满足的子句个数："<<satisfied_ans(m)<<endl;
cout<<"变元的终于取值为：";
for (i = 0 ; i<n ; i++)
{
cout<<ans[i]<<" ";
}
// if (satisfied_ans(m)==m)
// {
// cout<<"Yes";
// }
// else
// {
// cout<<"No";
// }
end = clock();
run_time = (end - start)/CLOCKS_PER_SEC;
printf("执行时间为 : %f\n", run_time);
system("pause");
return 0;
}
------------------------------------------------------
4 实验结果
4.1 參数设置
控制參数初值：t0=1000。
停止准则：温度达到设置的下限时即停止算法执行或达到最大可满足子句条件。
冷却进度表中的控制參数t的衰减函数：a(t)=0.98*t;
Mapkob链长：定长100*m。
4.2 实验结果
測试用例(1.txt)：http://download.****.net/detail/zhoubin1992/8794893
样本为1.txt。变元个数n=30，子句个数m=129时，可满足的子句数为128，执行时间为19.0000秒。结果例如以下：
------------------------------------------------------
參考文献
[1] 张德富.算法设计与分析（高级教程）[M].国防工业出版社，2007.