转载请注明出处：——————————————————
命题逻辑中合取范式 (CNF)的可满足性问题 (SAT)是当代理论计算机科学的核心问题,是一典型的NP完全问题.在定义可满足性问题SAT之前，先引进一些逻辑符号。
——————————————————
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 //随机的选择一个初始解X0give an initial temperature T0 , X ← X0, T ← T0 //初始化温度T0while 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++实现代码
<span style="font-size:14px;">// SA3Sat.cpp : 定义控制台应用程序的入口点。//#include "stdafx.h"#include <iostream>#include <time.h>#include <fstream>#include <math.h>using namespace std;#define ANSSIZE 100int 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;}</span>——————————————————
4 实验结果
4.1 参数设置
控制参数初值：t0=1000；
停止准则：温度达到设置的下限时即停止算法运行或达到最大可满足子句条件。
冷却进度表中的控制参数t的衰减函数：a(t)=0.98*t;
Mapkob链长：定长100*m。
4.2 实验结果
测试用例(1.txt)：
样本为1.txt，变元个数n=30，子句个数m=129时，可满足的子句数为128，运行时间为19.0000秒，结果如下：
对于旅行，从来都记忆模糊。记不得都去了哪些地方，
