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

1 SAT问题描述

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

一个 SAT 问题是指: 对于给定的 CNF 是否存在一组关于命题变元的真值指派使A为真. 显然,如A为真,则CNF的每个子句中必有一个命题变元为1(真)。

2 遗传算法

遗传算法类似于自然进化，通过作用于染色体上的基因寻找好的染色体来求解问题。与自然界相似，遗传算法对求解问题的本身一无所知，它所需要的仅是对算法所产生的每个染色体进行评价，并基于适应值来选择染色体，使适应性好的染色体有更多的繁殖机会。在遗传算法中，通过随机方式产生若干个所求解问题的数字编码，即染色体，形成初始群体；通过适应度函数给每个个体一个数值评价，淘汰低适应度的个体，选择高适应度的个体参加遗传操作，经过遗传操作后的个体集合形成下一代新的种群。对这个新种群进行下一轮进化。

下面就是遗传算法思想：

　　(1) 初始化群体;

　　(2) 计算群体上每个个体的适应度值;

　　(3) 按由个体适应度值所决定的某个规则选择将进入下一代的个体;

　　(4) 按概率Pc进行交叉操作;

　　(5) 按概率Pc进行突变操作;

　　(6) 没有满足某种停止条件，则转第(2)步，否则进入(7)。

　　(7) 输出种群中适应度值最优的染色体作为问题的满意解或最优解。

　　程序的停止条件最简单的有如下二种：完成了预先给定的进化代数则停止；种群中的最优个体在连续若干代没有改进或平均适应度在连续若干代基本没有改进时停止。

　　

3 实验结果

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

4 C++实现

// GA3SAT.cpp : 定义控制台应用程序的入口点。
//
/*********************************
-----------------------------------
遗传算法解决3SAT问题（C++实现代码）
-----------------------------------
Author:牧之丶  Date：2014年
Email:[email protected]
**********************************/
#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

版权声明：本文为博主原创文章，未经博主允许不得转载。

时间： 2024-08-26 16:56:17

遗传算法解决3SAT问题（C++实现代码）的相关文章

【高级算法】遗传算法解决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++实现代码)

转载请注明出处:http://blog.csdn.net/zhoubin1992/article/details/46453761 1 SAT问题描述 命题逻辑中合取范式 (CNF)的可满足性问题 (SAT)是当代理论计算机科学的核心问题,是一典型的NP完全问题.在定义可满足性问题SAT之前,先引进一些逻辑符号. 2  模拟退火算法 模拟退火算法来源于固体退火原理,将固体加温至充分高,再让其徐徐冷却,加温时,固体内部粒子随温升变为无序状,内能增大,而徐徐冷却时粒子渐趋有序,在每个温度都达到平衡态

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

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

禁忌搜索算法解决3SAT问题(C++代码实现)

最近梳理,翻出了当年高级算法课程做的题目,禁忌搜索. 吐槽:数学符号如何在编辑器里打出来啊,为了保留符号,我直接截图了. 1 SAT问题描述 定理4.4.1: 赋值v为使CNF可满足的充要条件是f(x1,x2,-,xm)达到最小值0. 2  禁忌搜索算法 禁忌搜索算法是在局部搜索的过程中引进了贪心选择机制,并利用禁忌表修改邻域,通过构造的候选邻域来控制解得选择和接受过程.在搜索的过程中,禁忌搜索算法从上一步计算解的候选邻域里选择一个最好的解,即使这个解比上一步得到的解还差,也接受它,同时修改禁忌

【高级算法】禁忌搜索算法解决3SAT问题(C++实现)

转载请注明出处:http://blog.csdn.net/zhoubin1992/article/details/46440389 近期梳理,翻出了当年高级算法课程做的题目.禁忌搜索算法解决3SAT问题. 吐槽:数学符号怎样在编辑器里打出来啊,为了保留符号,我直接截图了. 1 SAT问题描写叙述 定理4.4.1: 赋值v为使CNF可满足的充要条件是f(x1,x2,-,xm)达到最小值0. 2  禁忌搜索算法 禁忌搜索算法是在局部搜索的过程中引进了贪心选择机制.并利用禁忌表改动邻域,通过构造的候选

解决Socket沾包问题——C#代码

解决Socket沾包问题——C#代码 前天晚上,曾经的一个同事问我socket发送消息如果太频繁接收方就会有消息重叠,因为当时在外面,没有多加思考 第一反应还以为是多线程导致的数据不同步导致的,让他加个线程锁搞定.后来回到家慢慢思考感觉这个和加锁没啥关系,如果是多线程导致的,消息只会被覆盖呀.后来就上网搜索socket 消息重叠,后来了解到这属于socket沾包. 简单以自己的理解介绍下Socket沾包. Socket沾包简单说就是:Socket发送方 发送消息很频繁导致接收方接收到的消息是之前

Android开发--解决AndroidADT开发工具不能代码提示的问题

google android的新的开发工具,打开以后没有代码自动提示功能,下面对ADT工具的一些配置: 1.设置代码的字体 设置JAVA文件代码的字体:我这里设置的14 常规. 2.设置XML文件中代码的字体: 3.设置代码编辑器的背景颜色 色调85.饱和度90.亮度205 RGB:199.237.204 自定义: 4.设置代码提示功能: 快捷方式:Alt + /    可以出现代码提示. 默认的只有输入“ .” 以后才会有代码补全提示,可作如下设置: java->content Assist-

Window8.1 64位无法使用Debug命令的解决方法[附牛人代码]

偶然看到网上一篇文章,讲的是世界黑客编程大赛第一名的一个非常酷的程序,大小仅有4KB,使用debug命令运行. 悲催的是win8.1的debug命令不能使用. 错误如下: 解决方法如下: 1. 下载DOSBox 和Debug.exe 下载地址1:http://download.csdn.net/detail/ljgstudy/7557693(PS:需要1积分,积分多的大神高抬贵手哈~) 下载地址2:http://pan.baidu.com/s/1iwkGY(免积分) 2.安装DOSBox并启动,

tsp问题——遗传算法解决

TSP问题最简单的求解方法是枚举法.它的解是多维的.多局部极值的.趋于无穷大的复杂解的空间,搜索空间是n个点的所有排列的集合,大小为(n-1)!.可以形象地把解空间看成是一个无穷大的丘陵地带,各山峰或山谷的高度即是问题的极值.求解TSP,则是在此不能穷尽的丘陵地带中攀登以达到山顶或谷底的过程. 这一篇将用遗传算法解决TSP问题. 1)评价.这个评价算法应该比较简单了,就是找计算总距离,小的为优.目标函数转化为适应度函数可以取倒数. 2)突变.为了防止重复访问,不能随机的进行突变.因为每个城市只能