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具有非常強的跳出區域性最優解的能力。而且簡單通用，健壯性強。但是待定的引數很多，而且計算速度比較慢。選擇，雜交，變異運算元的選取也很關鍵。

參考文獻