命题逻辑中合取范式 (CNF) 的可满足性问题 (SAT)是当代理论计算机科学的核心问题, 是一典型的NP 完全问题.在定义可满足性问题SAT之前，先引进一些逻辑符号。
一个 SAT 问题是指: 对于给定的 CNF 是否存在一组关于命题变元的真值指派使A为真. 显然,如A为真,则CNF的每个子句中必有一个命题变元为1(真)。
遗传算法类似于自然进化，通过作用于染色体上的基因寻找好的染色体来求解问题。与自然界相似，遗传算法对求解问题的本身一无所知，它所需要的仅是对算法所产生的每个染色体进行评价，并基于适应值来选择染色体，使适应性好的染色体有更多的繁殖机会。在遗传算法中，通过随机方式产生若干个所求解问题的数字编码，即染色体，形成初始群体；通过适应度函数给每个个体一个数值评价，淘汰低适应度的个体，选择高适应度的个体参加遗传操作，经过遗传操作后的个体集合形成下一代新的种群。对这个新种群进行下一轮进化。
下面就是遗传算法思想：
(1) 初始化群体;
(2) 计算群体上每个个体的适应度值;
(3) 按由个体适应度值所决定的某个规则选择将进入下一代的个体;
(4) 按概率Pc进行交叉操作;
(5) 按概率Pc进行突变操作;
(6) 没有满足某种停止条件，则转第(2)步，否则进入(7)。
(7) 输出种群中适应度值最优的染色体作为问题的满意解或最优解。
程序的停止条件最简单的有如下二种：完成了预先给定的进化代数则停止；种群中的最优个体在连续若干代没有改进或平均适应度在连续若干代基本没有改进时停止。
样本为1.txt，变元个数n=30，子句个数m=129时，可满足的子句数为127，运行时间为00.0000秒，结果如下：
// GA3SAT.cpp : 定义控制台应用程序的入口点。
//
/*********************************
-----------------------------------
遗传算法解决3SAT问题（C++实现代码）
-----------------------------------
Author:牧之丶 Date：2014年
Email:bzhou84@163.com
**********************************/
#include "stdafx.h"
#include <iostream>
#include <fstream>
#include <time.h>
#include <math.h>
using namespace std;
#define ANSSIZE 100 //sat子句最大长度
#define POPUSIZE 40 //种群大小
#define GENERATE 100 //进化代数
#define PM 0.02 //编译概率
int bestGenes_sat;
int bestGenes[ANSSIZE];
int satGenes[POPUSIZE][ANSSIZE];
int score[POPUSIZE];
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 j = 0 ; j<POPUSIZE ; j++)
{
for (int i = 0 ; i<n ; i++)
{
if ((double)rand()/(RAND_MAX)>0.5)
{
satGenes[j][i] = 1;
}
else
{
satGenes[j][i] = 0;
}
}
}
}
void satisfied(int m)
{
int count = 0;
int i,j,k;
for (k = 0 ; k<POPUSIZE ; k++)
{
count = 0;
for (i = 0 ; i<m ; i++)
{
for (j = 0 ; j<3 ; j++)
{
if (x[i][j]<0)
{
int temp= (-1)*x[i][j];
if (satGenes[k][temp-1]==0)
{
count++;
break;
}
}
else if (x[i][j]>0)
{
if (satGenes[k][x[i][j]-1]==1)
{
count++;
break;
}
}
}
}
score[k] = count;
}
}
void findbestGene(int n)
{
int bestnum;
int bestscore = INT_MIN;
int i;
for (i = 0 ; i<POPUSIZE ; i++)
{
if (bestscore<score[i])
{
bestnum = i;
bestscore = score[i];
}
}
bestGenes_sat = bestscore;
for (i = 0 ; i<n ;i++)
{
bestGenes[i] = satGenes[bestnum][i];
}
}
void adapt(int n)
{
int imax,temp,i,j,k;
for (i = 0 ; i<POPUSIZE/2 ; i++)
{
imax = i;
for (j = i+1;j<POPUSIZE;j++)
{
if (score[j]>score[imax])
{
imax = j;
}
}
temp=score[i];
score[i]=score[imax];
score[imax]=temp;
for (int k = 0 ; k<n ; k++)
{
temp = satGenes[i][k];
satGenes[i][k]=satGenes[imax][k];
satGenes[imax][k]=temp;
}
}
for (i = 0 ;i<POPUSIZE/2;i++)
{
score[POPUSIZE/2+i] = score[i];
for (k = 0 ; k<n ;k++)
{
satGenes[POPUSIZE/2+i][k]=satGenes[i][k];
}
}
}
void cross(int n)
{
int croType,start,length,i,j,k,t;
int temp;
for (k = 0 ; k<POPUSIZE/2 ; k++)
{
i = rand()%(POPUSIZE/2);
j = rand()%(POPUSIZE/2);
while(i == j)
{
j = rand()%(POPUSIZE/2);
}
start = rand()%n;
length = rand()%(n-start);
croType = rand()%3;
switch(croType)
{
case 0:
case 1:
for (t = start;t<(start+length);t++)
{
temp = satGenes[i][t];
satGenes[i][t] = satGenes[j][t];
satGenes[j][t] = temp;
}
break;
case 2:
for (t = start ;t<(start+length);t++)
{
if (satGenes[i][t]+satGenes[j][t] == 1)
{
satGenes[i][t] = 0;
satGenes[j][t] = 1;
}
else
{
satGenes[i][t] = 1;
satGenes[j][t] = 0;
}
}
break;
}
}
}
void mutate(int n)
{
int i,j;
for (i = 0 ;i<POPUSIZE;i++)
{
for (j = 0 ;j<n;j++)
{
if (randomf(0,1)<PM)
{
satGenes[i][j] = 1-satGenes[i][j];
}
}
}
}
bool isbetter()
{
int max_temp = INT_MIN;
for (int i = 0 ;i<POPUSIZE ; i++)
{
if (score[i]>max_temp)
{
max_temp = score[i];
}
}
if (max_temp>=bestGenes_sat)
{
return 1;
}
return 0;
}
void GA3Sat(int n,int m)
{
int genaration = 0; //第几代种群
Johnson(n); //初始化种群
satisfied(m); //计算基因的好坏
findbestGene(n);
ofstream fout;
fout.open("output.txt");
fout<<"第"<<genaration<<"代种群中的最优解是："<<bestGenes_sat<<endl;
while((bestGenes_sat!=m)&&genaration<GENERATE)
{
adapt(n); //选择
cross(n); //杂交
mutate(n); //变异
satisfied(m); //计算基因的好坏
if (!isbetter())
{
int temp = rand()%POPUSIZE;
score[temp] = bestGenes_sat;
for (int i = 0 ;i<n ; i++)
{
satGenes[temp][i] = bestGenes[i];
}
}
genaration++;
findbestGene(n);
fout<<"第"<<genaration<<"代种群中的最优解是："<<bestGenes_sat<<endl;
}
// if (bestGenes_sat==m)
// {
// cout<<"Yes";
// }
// else
// {
// cout<<"No";
// }
fout.close();
}
int _tmain(int argc, _TCHAR* argv[])
{
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));
GA3Sat(n,m);
end = clock();
run_time = (end - start)/CLOCKS_PER_SEC;
printf("运行时间为 : %f\n", run_time);
system("pause");
return 0;
}
GA比起SA ，最大的优势在于对个初始解，而且存在杂交和变异，让SA具有非常强的跳出局部最优解的能力。而且简单通用，健壮性强。但是待定的参数很多，而且计算速度比较慢。选择，杂交，变异算子的选取也很关键。
[1] 张德富.算法设计与分析（高级教程）[M].国防工业出版社，2007.
[2] 模拟退火算法求解旅行商问题 http://blog.csdn.net/lalor/article/details/7688329.2011.
我的其他解决3SAT问题的相关方法
Lasvegas+回溯算法解决3SAT问题（C++实现代码）：
http://blog.csdn.net/zhoubin1992/article/details/46507919
Lasvegas算法解决3SAT问题（C++实现代码）：
http://blog.csdn.net/zhoubin1992/article/details/46469557
模拟退火算法解决3SAT问题(C++实现代码)：
http://blog.csdn.net/zhoubin1992/article/details/46453761
禁忌搜索算法解决3SAT问题(C++代码实现)：
http://blog.csdn.net/zhoubin1992/article/details/46440389
版权声明：本文为博主原创文章，未经博主允许不得转载。
原文地址：http://blog.csdn.net/zhoubin1992/article/details/46910079
