模拟退火算法解决3SAT问题(C++实现代码),退火3sat

来源:金属材料及热处理作者:叶卫平

模拟退火算法解决3SAT问题(C++实现代码),退火3sat

转载请注明出处: ------------------------------------------------------

1 SAT问题描述

命题逻辑中合取范式 (CNF)的可满足性问题 (SAT)是当代理论计算机科学的核心问题,是一典型的NP完全问题.在定义可满足性问题SAT之前,先引进一些逻辑符号。

模拟退火算法解决3SAT问题(C++实现代码),退火3sat

------------------------------------------------------

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++实现代码

<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 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; } </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秒,结果如下:

模拟退火算法解决3SAT问题(C++实现代码),退火3sat

------------------------------------------------------

参考文献

[1]  张德富.算法设计与分析(高级教程)[M].国防工业出版社,2007.