kivantium活動日記

プログラムを使っていろいろやります

SATをサッと解く 〜乱択アルゴリズムで遊んだ話〜

ミレニアム問題と呼ばれる数学の7つの難問がある。各分野で重要かつ難しい問題が選ばれており、解決するとクレイ研究所から100万ドルの賞金を得ることができるということで有名だ。そのうちの1つポアンカレ予想は解決済みだが、残りの6つは未解決である。その中でもコンピュータ科学で非常に重要な問題が「P≠NP予想」である

P≠NP予想とは

コンピュータで問題を解決するときには一定の手続き(アルゴリズム)に従って問題を処理することになる。例えば数の集合の中からある特定の数字を見つけるという問題を考える。一番単純な解決方法は集合の要素を1つずつ調べていって値が求めたい数字になっているかどうかチェックすることだろう。この場合、集合がN個の数字からなるとすればおおよそNに比例する時間で求めたい数字の検索が終わることが予想できる。このようにだいたいNに比例する時間で終わるようなアルゴリズムについて、計算時間のオーダーはO(N)であるという。(もちろんここで述べたのはおおまかなのイメージであって正確な定義が別にきちんと存在する。)集合の中から任意に選んだ2つの数の和がある値に等しくなるかを調べるために、全ての2つの組み合わせを順番に調べていくとしたら、2つの選び方はN(N-1)通りあるのでこのアルゴリズムの計算量はおおよそO(N^2)である。このようにOの中身はアルゴリズムによっていろいろあるが、Oの中身が多項式になるようなアルゴリズム多項式時間アルゴリズムと呼び、多項式時間アルゴリズムで解ける判定問題の集合をクラスPと呼ぶ。

それに対して、集合の中から好きなだけ数を選んでその和がある数に等しいかという問題は、数の選び方が2^N通りを1つ1つ試していくとすると計算時間はO(2^N)となる。これは指数関数なので多項式時間アルゴリズムではない。しかし、一度正しい組み合わせが与えられるとそれらを足し合わせるだけでその答えが正しいかどうかは簡単に判定することができる。このような、答えが与えられた時にその答えが正しいかどうかを多項式時間で判定することができる判定問題の集合をクラスNPと呼ぶ。

クラスPはクラスNPに含まれるが、クラスPとクラスNPが等しいかどうかは証明されていない。おそらくクラスPはクラスNPの真部分集合だろうと言われている。クラスPとクラスNPが等しくないとする予想がP≠NP予想である。

この前読んだ、P≠NP予想の一般向けの入門書「P≠NP予想とはなんだろう」が面白かったのでここに紹介しておく。

P≠NP予想とはなんだろう  ゴールデンチケットは見つかるか?

P≠NP予想とはなんだろう ゴールデンチケットは見つかるか?

SATとは

クラスNPに属する問題のうち「最も難しいもの」をNP完全と呼ぶ。「最も難しい」というのはクラスNPに属する全ての問題が多項式時間でその問題に帰着できることを言う。どのNP完全な問題でもいいからその1つを多項式時間アルゴリズムで解くことができれば、すべてのクラスNPの問題が多項式時間で解けることになりP=NPが示される。今のところそのようなアルゴリズムは見つかっておらず、P≠NP予想を支持する根拠となっている。

NP完全な問題は数千個見つかっているが、その中でも有名なものがSAT(充足可能性問題)である。SATはある論理式が与えられた時にそれを真にするような組み合わせが存在するか?というような問題である。例えば、 (x_0 \lor x_1) \land (x_1 \lnot x_2) という論理式に対しては例えば順に真・真・偽とすれば論理式全体が真になる。 x_0のような一つの項をリテラルと呼び、リテラル3つのORをとったもの(節)をANDでつないだ論理式に対するSATを3-SATと呼び、これもNP完全であることが知られている。

乱択アルゴリズムとは

3-SATを解く場合に一番最初に思いつくアルゴリズムは真と偽の全ての組み合わせ2^Nを順に調べていく方法であろう。しかし、この方法では指数関数的に時間が増大していってうまく行かない。そこで偽となった節をランダムに一つ選び、さらにその節を構成するリテラルの中から1つ選んで反転させるという操作を繰り返すことで正解に近づこうとする「乱択アルゴリズム」が考案された。この方法を取ると1.334^nのオーダーで正解を得ることができることが知られている。この計算は「数学ガール 乱択アルゴリズム」で紹介されている。

数学ガール 乱択アルゴリズム (数学ガールシリーズ 4)

数学ガール 乱択アルゴリズム (数学ガールシリーズ 4)

この記事では数学ガールで紹介されていた乱択アルゴリズムと単純な全探索プログラムを比較してみることにする。

全探索プログラム

ビット全探索を行って最初の解が見つかるまで探しつづける。

#include <cstdlib>
#include <random>
#include <vector>
#include <iostream>
#include <cmath>

using namespace std;

random_device rd;
mt19937 mt(rd());

int main(int argc, char *argv[]) {
    const int N = 50;
    const int len = 60;
    uniform_int_distribution<> rand(0, N-1);
    uniform_int_distribution<> bin(0, 1);
    int X[N];
    int CNF[3*len];
    for(int i=0; i<3*len; ++i){
        CNF[i] = rand(mt);
    }
    int TF[3*len];
    for(int i=0; i<3*len; ++i){
        TF[i] = bin(mt);
    }
    for(int i=0; i<3*len; ++i){
        if(i%3==0){
            cout << "(";
            if(TF[i]==0) cout << "(NOT " << "X" << CNF[i] << ") OR ";
            else cout << "X" << CNF[i] << " OR ";
        } else if(i%3==1){
            if(TF[i]==0) cout << "(NOT " << "X" << CNF[i] << ") OR ";
            else cout << "X" << CNF[i] << " OR ";
        } else{
            if(TF[i]==0) cout << "(NOT " << "X" << CNF[i] << "))";
            else cout << "X" << CNF[i] << ")";
            if(i!=3*len-1) cout << " AND ";
        }
    }
    cout << endl;
    for(int64_t binary=0; binary<((int64_t)1<<(N)); ++binary){
        bool isClear = true;
        for(int i=0; i<N; ++i){
            if(binary&((int64_t)1<<i)) X[i] = 1;
            else X[i] = 0;
        }
        for(int i=0; i<len; ++i){
            if(X[CNF[3*i]] != TF[3*i] &&
               X[CNF[3*i+1]] != TF[3*i+1] &&
               X[CNF[3*i+2]] != TF[3*i+2]){
                isClear = false;
            }
        }
        if(isClear) {
            for(int i=0; i<N; ++i){
                if(X[i] == 1) cout << "T";
                else cout << "F";
            }
            cout << endl;
            break;
        }
    }
}

乱択アルゴリズム

乱択アルゴリズムで最初の解が見つかるまで探しつづける。

#include <cstdlib>
#include <random>
#include <vector>
#include <iostream>
#include <cmath>

using namespace std;

random_device rd;
mt19937 mt(rd());

int main(int argc, char *argv[]) {
    const int N = 50;
    const int len = 60;
    uniform_int_distribution<> rand(0, N-1);
    uniform_int_distribution<> bin(0, 1);
    int X[N];
    int CNF[3*len];
    for(int i=0; i<3*len; ++i){
        CNF[i] = rand(mt);
    }
    int TF[3*len];
    for(int i=0; i<3*len; ++i){
        TF[i] = bin(mt);
    }
    for(int i=0; i<3*len; ++i){
        if(i%3==0){
            cout << "(";
            if(TF[i]==0) cout << "(NOT " << "X" << CNF[i] << ") OR ";
            else cout << "X" << CNF[i] << " OR ";
        } else if(i%3==1){
            if(TF[i]==0) cout << "(NOT " << "X" << CNF[i] << ") OR ";
            else cout << "X" << CNF[i] << " OR ";
        } else{
            if(TF[i]==0) cout << "(NOT " << "X" << CNF[i] << "))";
            else cout << "X" << CNF[i] << ")";
            if(i!=3*len-1) cout << " AND ";
        }
    }
    cout << endl;
    for(int R=0; R<10000000; ++R){
        for(int i=0; i<3*len; ++i) X[i] = bin(mt);
        for(int count=0; count<3*N; ++count){
            bool isClear = true;
            uniform_int_distribution<> three(0, 2);
            vector<int> unsat={};
            for(int i=0; i<len; ++i){
                if(X[CNF[3*i]] != TF[3*i] &&
                        X[CNF[3*i+1]] != TF[3*i+1] &&
                        X[CNF[3*i+2]] != TF[3*i+2]){
                    isClear = false;
                    unsat.push_back(len);
                }
            }
            if(isClear) {
                for(int i=0; i<N; ++i){
                    if(X[i] == 1) cout << "T";
                    else cout << "F";
                }
                cout << endl;
                goto END;
            }else{
                uniform_int_distribution<> choice(0, unsat.size()-1);
                int change = choice(mt)+three(mt);
                X[change] = ~X[change];
            }
        }
    }
END:
    cout << "solved!" << endl;
}

比較

N(出現するリテラルの種類,x0-xN)とlen(節の数)を変えていって最初の解が見つかるまでの実行時間の変化を調べた。実行時間はtimeコマンドのrealで10回調べたものの平均である。

全探索
N len 時間(s)
30 40 4.27
40 50 43.4974
50 60 ---

N=50, len=60については実行時間が1時間を超えたケースがあったためそこで調査を打ち切ることにした。

乱択アルゴリズム
N len 時間(s)
30 40 0.12
40 50 0.91
50 60 3.23
60 70 14.25

もちろんtimeコマンドでの荒い評価なので定量的な比較はできないが、それでも全探索によるものと比べると圧倒的に速くなっていることが分かる。乱択アルゴリズムによってSATがサッと解けることが明らかになった。

さらに速いアルゴリズムを求めて

乱択アルゴリズムの速度が1.334^nのオーダーであることを示した論文は1999年のものなので当然現在ではより良い方法が存在する。10^6-10^7くらいまでは高速に解けるようである。Vol.28 No.2 (2013/03) SAT ソルバー | 人工知能学会 (The Japanese Society for Artificial Intelligence)
あのお姉さんの悲劇を繰り返さないためにも新たなアルゴリズムの研究が必要である
『フカシギの数え方』 おねえさんといっしょ! みんなで数えてみよう! - YouTube