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

转载请注明出处：http://blog.csdn.net/zhoubin1992/article/details/46453761

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步运算。

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

<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)：http://download.csdn.net/detail/zhoubin1992/8794893

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

参考文献

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

时间： 2024-08-03 15:22:39

模拟退火算法解决3SAT问题(C++实现代码)的相关文章

Lasvegas+回溯算法解决3SAT问题（C++实现代码）

转载请注明出处:http://blog.csdn.net/zhoubin1992/article/details/46507919 1.SAT问题描述 命题逻辑中合取范式 (CNF) 的可满足性问题 (SAT)是当代理论计算机科学的核心问题, 是一典型的NP 完全问题.在定义可满足性问题SAT之前,先引进一些逻辑符号. 一个 SAT 问题是指: 对于给定的 CNF 是否存在一组关于命题变元的真值指派使得A 为真. 显然, 如果A 为真, 则 CNF 的每个子句中必有一个命题变元为 1 (真) .

模拟退火算法解决旅行商问题(matlab)

模拟退火算法解决旅行商问题. 根据概率产生新解主要包含两个途径:二交换和三交换 二交换是在TSP回路中选择两个城市直接交换 三交换是在TSP回路中选择三个点,p1,p2,p3,然后将p1,p2之间的城市直接与p3之前对应长度的城市交换 这里产生新解的方法不唯一,只要能够保证产生的新解可以包含最优解所在的解空间即可 是否接受新解主要包含两种情况: 新解比历史最优解好,则百分百接受新解 新解比当前解好,没历史最优解好,则以一定概率接受新解,并且随着温度的降低.接受的概率也会降低. 如下是TSP代码.

Lasvegas算法解决3SAT问题（C++实现代码）

转载请注明出处:http://blog.csdn.net/zhoubin1992/article/details/46469557 1.SAT问题描述 命题逻辑中合取范式 (CNF) 的可满足性问题 (SAT)是当代理论计算机科学的核心问题, 是一典型的NP 完全问题.在定义可满足性问题SAT之前,先引进一些逻辑符号. 一个 SAT 问题是指: 对于给定的 CNF 是否存在一组关于命题变元的真值指派使得A 为真. 显然, 如果A 为真, 则 CNF 的每个子句中必有一个命题变元为 1 (真) .

【高级算法】遗传算法解决3SAT问题（C++实现）

转载请注明出处:http://blog.csdn.net/zhoubin1992/article/details/46910079 1 SAT问题描写叙述 命题逻辑中合取范式 (CNF) 的可满足性问题 (SAT)是当代理论计算机科学的核心问题, 是一典型的NP 全然问题.在定义可满足性问题SAT之前,先引进一些逻辑符号. 一个 SAT 问题是指: 对于给定的 CNF 是否存在一组关于命题变元的真值指派使A为真. 显然,如A为真,则CNF的每一个子句中必有一个命题变元为1(真). 2 遗传算法

遗传算法解决3SAT问题（C++实现代码）

1 SAT问题描述 命题逻辑中合取范式 (CNF) 的可满足性问题 (SAT)是当代理论计算机科学的核心问题, 是一典型的NP 完全问题.在定义可满足性问题SAT之前,先引进一些逻辑符号. 一个 SAT 问题是指: 对于给定的 CNF 是否存在一组关于命题变元的真值指派使A为真. 显然,如A为真,则CNF的每个子句中必有一个命题变元为1(真). 2 遗传算法 遗传算法类似于自然进化,通过作用于染色体上的基因寻找好的染色体来求解问题.与自然界相似,遗传算法对求解问题的本身一无所知,它所需要的仅是对

模拟退火算法简介

优化算法入门系列文章目录(更新中): 1. 模拟退火算法 2. 遗传算法 一. 爬山算法 ( Hill Climbing ) 介绍模拟退火前,先介绍爬山算法.爬山算法是一种简单的贪心搜索算法,该算法每次从当前解的临近解空间中选择一个最优解作为当前解,直到达到一个局部最优解. 爬山算法实现很简单,其主要缺点是会陷入局部最优解,而不一定能搜索到全局最优解.如图1所示:假设C点为当前解,爬山算法搜索到A点这个局部最优解就会停止搜索,因为在A点无论向那个方向小幅度移动都不能得到更优的解. 图1    

模拟退火算法解析

一. 爬山算法 ( Hill Climbing ) 介绍模拟退火前,先介绍爬山算法.爬山算法是一种简单的贪心搜索算法,该算法每次从当前解的临近解空间中选择一个最优解作为当前解,直到达到一个局部最优解. 爬山算法实现很简单,其主要缺点是会陷入局部最优解,而不一定能搜索到全局最优解.如图1所示:假设C点为当前解,爬山算法搜索到A点这个局部最优解就会停止搜索,因为在A点无论向那个方向小幅度移动都不能得到更优的解. 图1     二. 模拟退火(SA,Simulated Annealing)思想 爬山法

大白话解析模拟退火算法

优化算法入门系列文章目录(更新中): 1. 模拟退火算法 2. 遗传算法 一. 爬山算法 ( Hill Climbing ) 介绍模拟退火前,先介绍爬山算法.爬山算法是一种简单的贪心搜索算法,该算法每次从当前解的临近解空间中选择一个最优解作为当前解,直到达到一个局部最优解. 爬山算法实现很简单,其主要缺点是会陷入局部最优解,而不一定能搜索到全局最优解.如图1所示:假设C点为当前解,爬山算法搜索到A点这个局部最优解就会停止搜索,因为在A点无论向那个方向小幅度移动都不能得到更优的解. 图1    

[Machine Learning]转载:模拟退火算法

From : http://www.cnblogs.com/heaad/archive/2010/12/20/1911614.html 优化算法入门系列文章目录(更新中): 1. 模拟退火算法 2. 遗传算法 一. 爬山算法 ( Hill Climbing ) 介绍模拟退火前,先介绍爬山算法.爬山算法是一种简单的贪心搜索算法,该算法每次从当前解的临近解空间中选择一个最优解作为当前解,直到达到一个局部最优解. 爬山算法实现很简单,其主要缺点是会陷入局部最优解,而不一定能搜索到全局最优解.如图1所示