转载请注明出处：

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

1 SAT问题描写叙述

命题逻辑中合取范式 (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步运算。

    模拟退火算法伪代码例如以下：

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

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

3 C++实现代码

// SA3Sat.cpp : 定义控制台应用程序的入口点。///********************************* ----------------------------------- 模拟退火解决3SAT问题（C++实现代码）----------------------------------- Author:牧之丶  Date：2014年Email:bzhou84@163.com **********************************/  #include "stdafx.h"#include 
     
      #include 
      
       #include 
       
        #include 
        
         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
         
          0.5)		{			ans[i] = 1;		}		else		{			ans[i] = 0;		}		}}int satisfied_ans(int m){	int count = 0;	int i,j;	for (i = 0 ; i
          
           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
           
            0) { if (new_ans[x[i][j]-1]==1) { count++; break; } } } } return count;}void disturb(int n){ for (int j = 0 ; j
            
             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
             
              >n>>m; //3SAT问题 // x = new int*[m];// for (i = 0 ; i
              
               >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
               
                >x[i][j]; } fin>>t; } fin.close(); srand((unsigned)time(NULL)); SA3Sat(n,m); cout<<"可满足的子句个数："<
                
                 <
                
               
              
             
            
           
          
         
        
       
      
     

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

4  实验结果

4.1 參数设置

控制參数初值：t₀=1000。

停止准则：温度达到设置的下限时即停止算法执行或达到最大可满足子句条件。

冷却进度表中的控制參数t的衰减函数：a(t)=0.98*t;

Mapkob链长：定长100*m。

4.2 实验结果

測试用例(1.txt)：

样本为1.txt。变元个数n=30，子句个数m=129时，可满足的子句数为128，执行时间为19.0000秒。结果例如以下：

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

參考文献

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