SATソルバを作る会 (1) - ひとり勉強会

適当にまったりと。今回は下準備みたいなものだけです。

入力

せっかくなのでデータ形式は SAT Competitions の形式と揃えておこうかと思いました。出せるようなものはとても作れないですけど、比較する時にその方が便利そう。

まず、入力はConjunctive Normal Formの論理式で与えるとのこと。

(x1 or !x5 or x4) and (!x1 or x5 or x3 or x4) and (!x3 or !x4)

こういう、『「変数か変数の否定 (= リテラル)」をorで繋いだもの (= 選言節)』をandで繋いだもの、という形の式です。ファイル形式としては、DIMACS形式というので与えられるらしい。こんなテキストファイルです。

c
c コメント〜
c
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

最初に何行かコメント (c XXXXX)
次にヘッダ的なもの (p cnf 変数の個数選言節の数)
以下、一行に一個の選言節。スペース区切りの整数列で、
- 正の数はnotがついてない変数
- 負の数はnotがついてる変数
- ゼロは選言節の終わり

出力

出力は、論理式を true にすることができる場合は

s SATISFIABLE
v 1 -2 3 -4 -5 0

のようにして、たとえば x1,x3 をtrueにして x2,x4,x5 をfalseにすればOK、という例を標準出力に出します。複数のtrueにしかたがある場合、どれか１つ出せばよいです。同時に、実行ファイルの終了コードとして 10 を返します。

出力は、論理式を true にすることができない場合は、

s UNSATISFIABLE

だけでいい。実行ファイルの終了コードとして 20 を返す。

コンテストのように時間制限がある場合、時間切れ等でどちらともわからなかった場合は、

s UNKNOWN

で、終了コードとして 0 を返す。とりあえずこれは自分には関係ないかな。

Take 1 : 完全に全探索

まずはウォームアップとして、全ての変数割り当てパターンを総当たりで試してみるソルバを書いてみました。今のところD言語を使っています。

import std.stdio;
import std.stream, std.cstream;
import std.string;
import std.conv;

class SAT
{
private:
  alias int Literal; /// 非ゼロ整数。+n は xn、-n は !xn を表す
  int  varOf( Literal lit )      { return (lit>0 ? lit-1 : -lit-1); }
  bool isPositive( Literal lit ) { return (lit>0); }

  alias Literal[] Clause; /// [-1,+2,+3] が !x1|x2|x3 を表す
  alias Clause[]     CNF; /// [[-1,+2],[+3,-2]] で (!x1|x2)&(x3|!x2) を表す

private:
  int numVar; /// 変数の個数
  CNF cnf;    /// 論理式

public:
  /// DIMACS format の入力ストリームから適当に読み込み
  this( InputStream sin )
  {
    foreach(char[] s; sin)
      if( s.length && s[0]!='c' )
        if( s[0] == 'p' )
          numVar = to!(int)( (s.idup.split)[2] );
        else
          cnf ~= to!(int[])( (s.idup.split)[0..$-1] );
  }

  /// ビットベクトルで変数への値割り当てを与えて評価
  bool eval(BitVec)( BitVec bv )
  {
    bool be = true;
    foreach(clause; cnf)
    {
      bool bc = false;
      foreach(lit; clause)
      {
        static if( is(bv[0]) )
          bool bl = bv[varOf(lit)];
        else
          bool bl = !!((bv>>varOf(lit))&1);
        bc |= isPositive(lit) ? bl : !bl;
      }
      be &= bc;
    }
    return be;
  }
}

bool solve( SAT s )
{
  long MASK = (1L << s.numVar) - 1;

  B_LOOP:
  for(long B=0; B<=MASK; ++B)
    if( s.eval(B) )
    {
      // Satisfied
      writeln("s SATISFIABLE");
      write("v");
      for(int i=0; i<s.numVar; ++i)
        write(" ", (B>>i)&1 ? i+1 : -i-1);
      writeln(" ", 0);
      return true;
    }

  // Not satisfied
  writeln("s UNSATISFIABLE");
  return false;
}

int main()
{
  auto s = new SAT(din);
  return solve(s) ? 10 : 20;
}

さて、これが最低ラインのパフォーマンスと言うことになります。どのくらいのスピードかなー。

20変数85節の3-CNF（各選言説のリテラル数が全部3のもの）ランダムデータを作って試してみました。色々試してみたところ、節数をこれより減らすとSATISFIABLEだらけ、これより増やすとUNSATISFIABLEだらけになってしまうようなので。比較対象はPicoSATです。

<picosat>
s SATISFIABLE
v -1 2 3 -4 -5 6 7 8 9 -10 11 12 13 -14 15 -16 17 -18 19 20 0
[10] : 99 ms

<hzkrsat>
s SATISFIABLE
v 1 2 -3 -4 5 -6 7 8 -9 10 -11 12 -13 14 -15 16 -17 -18 19 -20 0
[10] : 5977 ms

といったところ。もちろん、もっと大きい入力を喰わせるとどんどん差は開いていきました。25変数105節だと…

<picosat>
s SATISFIABLE
v 1 -2 3 -4 5 6 7 -8 -9 -10 11 -12 -13 -14 -15 -16 -17 18 19 20 -21 22 -23 -24
v 25 0
[10] : 105 ms

<hzkrsat>
s SATISFIABLE
v -1 2 -3 4 5 6 -7 -8 -9 10 -11 -12 -13 -14 -15 -16 17 18 19 -20 21 -22 -23 24 -
25 0
[10] : 222315 ms

というわけで、次回から色々試して改善していけたらいいなーと思います。

雑談

そういえば、変数と節数の比が4.4898を超えるとほぼ確実にUNSATISFIABLEという論文を前に読んで「へー！」と思っていたのを思い出しました。確かに自分で手で実験してみるとその辺りに境がありますね。面白かったです。

ググってみると、イマドキのSATソルバは基本的に DPLL という枠組みで解いているらしい。次はこの辺りをちょっと調べてみようかと思います。予定は未定です。