乱択アルゴリズムに挑む(その 3)

アルゴリズム Java

k-CNF の充足可能な(つまり、全ての clause が真になるような真偽値の)割り当てを求める問題は k-SAT(Satisfiability Problem)と呼ばれる。同書にならって 3-SAT を考える。

問題としては、これまた同書でユーリが「僕」に示した問題で行ってみよう。まず変数を 4 個用意し、それぞれ以下の意味とする。

  • x[0] : 強い
  • x[1] : 正しい
  • x[2] : 美しい
  • x[3] : 優しい

これを用いて、同問題の P1 〜 P8 を書き下してみよう。なお、配列の index が 0 から始まる都合上、p[0] 〜 p[7] に変えておく。

boolean [] x = new boolean[4];
boolean [] p = new boolean[8];

p[0] = x[0] || x[1] || x[2];
p[1] = x[3] || x[1] || !x[2];
p[2] = !x[0] || x[3] || x[2];
p[3] = !x[0] || !x[3] || x[1];
p[4] = !x[3] || !x[1] || x[2];
p[5] = !x[0] || !x[1] || !x[2];
p[6] = x[0] || !x[3] || !x[2];
p[7] = x[0] || x[3] || !x[1];

p[0] 〜 p[7] が全て真であるかどうか確認するには以下のようにすればよい。

boolean sat = p[0];
for(int i = 1; i < p.length; i++) {
    sat = sat && p[i];
}

これで sat が true であれば、全ての p[i] が真であることが確認できる。