[数理]第2回組合せ問題
2006年10月05日（木）17:30｜谷口
前回、簡単にSATについて説明しましたが、今回はSATを解こうとしてみます。実際、有用な解法は現時点では存在しないのですが、本当に有用でないかどうかを推し量るため、一般的な計算量の見積もりと、 問題のクラスという概念を紹介したいと思います。 とりあえず、今回は計算量のお話から。
おさらい
SATとは 論理式の集合が与えられ、 すべての式に対して真を返す変数の組があるかないかを判定する問題。
例題
a,b,cはそれぞれtrue or falseの2値変数とする。
(a ∨ b), (￢a ∨ c), (b ∨ ￢c)という論理式の
すべてで真を返すa, b, cの組が存在するか。
∧：AND（論理積）∨：OR（論理和）￢：NOT（否定）
SATを解いてみる
誰でも思いつくような方法で解こうとしてみます。 1. すべての変数の組に対して、各式が成立するかどうかを検証。
- すべての式を成立させる変数の組が、一つでも見つかれば終了。
変数の数をn, 式の数をmとすると、変数列の組合せは2n通りあり、それぞれの組合せで多くともm回検証すればよい。
例題ですと、変数の数はa,b,cの3つ式の数も(a ∨ b), (￢a ∨ c), (b ∨ ￢c)の3つです。
つまり、変数列の組合せは2n=8通り。すべて示すと
(a,b,c) = (true, true, true)
(a,b,c) = (true, true, false)
(a,b,c) = (true, false, true)
(a,b,c) = (true, false, false)
(a,b,c) = (false, true, true)
(a,b,c) = (false, true, false)
(a,b,c) = (false, false, true)
(a,b,c) = (false, false, false)
となります。
では、この方法は実際有用なのでしょうか？ （普通のプログラマであれば、こんな方法は実用的でないことが容易に想像できると思います。）
一般的な計算量の見積もり
アルゴリズムの計算量（= 時間）はオーダー(O(x))という概念を用いて考えます。
ある定数c、n0が存在し、
n > n0 ⇒ f(n) =< cg(n) (1) が成り立つとき、
f(n) = O(g(n))と定義されます。
例えば、 f(n) = n2 + 13n + 30 とすると、
c = 2, n0 = 15, g(n) = n2 で(1)式が成立するので、
f(n) = O(n2) となります。
ここで、f(n)はプログラムの実行時間と思っていただいて構いません。
例えば、ソートのアルゴリズムを考えてみます。 シンプルにバブルソートで。 sort[n]={s1, s2, ･･･, sn};
for(i=0; i < n; ++i){
for(j=i+1; j < n; ++j){
if(sort[i] > sort[j]){
tmp = sort[i];
sort[i] = sort[j];
sort[j] = tmp;
}
}
}
このとき、if文の条件判定を行う回数を計算してみましょう。
i = 0のとき：n-1回
i = 1のとき：n-2回
･･･
i = n-1のとき:0回
となります。つまり、 k=0∑n-1k = n(n-1) / 2 回
また、毎回条件判定でtrueが返ってくるとすると、 if文の中で行われている代入の回数は 3 * n(n-1) / 2 回 となります。
（何回かはfalseが返ってくることもありますので、 実際は3 * n(n-1) / 2以下ですが、オーダーの概念では最悪のケースで考えます。）
これを合計すると、2n(n-1) 回。 他にもfor文で++iされる回数だとかありますが、せいぜいn2に比例した回数になるので、オーダーの概念からすると無視して良いのです。
ここで、オーダーの定義に戻ると、c=2, n0, g(n)=n2で(1)式が成立しますので、 バブルソートの計算量f(n)は
f(n) = O(n2)
となります。
多項式時間と指数時間
また、もう少しおおざっぱにした多項式時間という括りがあります。 入力となる問題の規模をnとしたとき、任意の自然数kを使って、
多項式時間
O(nk)で時間を見積もることができるもの。 n回繰り返されるループ文の入れ子がk回ある感じ。
指数時間（k > 1）
O(kn)で時間を見積もることができるもの。 k回数繰り返されるループ文の入れ子がn回ある感じ。
上述のSATの解法は、O(2n)かかることになります。 実際どれくらい増加に差があるか、k=2としてざっと示します。
| n | 2 | 10 | 50 |
| n2 | 4 | 100 | 2500 |
| 2n | 4 | 1024 | 1125899906842624 |
nが50くらいでも、かなりの差が出ます。仮に上の数字を秒とすると、約3570万年かかる計算になります。
おわりに
今回提示したSATの解法の計算量は指数オーダーとなります。 次回はその説明と問題のクラスという概念を紹介いたします。
