nandaro

今年度も折り返しだなあとか思いつつ書いてる。(どうでもいい挨拶)

今回は推論の続きということで、BCP 及び監視リテラルの話。
今の BCP の実装は監視リテラルと密接にかかわってるので一緒のトピックでいいやという判断。

BCP とは現在の割当における単位節を真にするような割当を繰り返すというシンプルなアルゴリズム。
で、監視リテラルはBCPの実装方式の話。「BCP を実装するときは、節に見なした配列の 2 つの要素 (リテラルと見なす) だけ見てれば十分じゃん」ということで、この方式が生まれた。
例によって例のごとく MiniSat2.2 のBCPに関する部分のソースを載せる。独断と偏見で本質とは関係なさそうな箇所を除外してるので注意

CRef Solver::propagate()
{
    CRef    confl     = CRef_Undef;

    while (qhead < trail.size()){                //割り当て済みのリテラルは配列trailに格納されてる
        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
        vec<Watcher>&  ws  = watches[p];         //0番目か1番目のリテラルが~pを含む節、即ち監視リテラルに~pを持つ節を順になめていく
        Watcher        *i, *j, *end;             //構造体 Watcher は節みたいなもの

        for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
            // Make sure the false literal is data[1]:
            CRef     cr        = i->cref;
            Clause&  c         = ca[cr];         //c はリテラルの配列、すなわち節
            Lit      false_lit = ~p;             //p は常にtrueなので、逆に~pは常にfalse
            if (c[0] == false_lit)               //絶対に1番目のリテラルがfalseになるようにする
                c[0] = c[1], c[1] = false_lit;
            assert(c[1] == false_lit);
            i++;

//----     この時点で、1番目のリテラル (監視リテラルの片方) はfalseになっている(仕様)       ---

            // If 0th watch is true, then clause is already satisfied.
            Lit     first = c[0];
            Watcher w     = Watcher(cr, first);
            if (value(first) == l_True){          //0番目のリテラルがtrueなら節も当然true
                *j++ = w; continue; }

//---      1番目のリテラルがfalseで、0番目のリテラルもtrueでない場合      ---

            // Look for new watch:
            //falseになった片割れ(1番目のリテラル)の代わりに新たな監視リテラルを探す
            for (int k = 2; k < c.size(); k++)    //当然2番目からリテラルを見ていく
                if (value(c[k]) != l_False){      //未定リテラルを見つけたら
                    c[1] = c[k]; c[k] = false_lit;//  1番目のリテラルと交換
                    watches[~c[1]].push(w);       //k番目のリテラルを監視する節の配列に加える
                    goto NextClause; }

//---      1番目のリテラルがfalseで、0番目のリテラルもtrueでなく、代わりのリテラルも見つからなかった場合 ---

            // Did not find watch -- clause is unit under assignment:
            *j++ = w;
            if (value(first) == l_False){         //0番目のリテラルもfalseだと、その節は空節となり矛盾を引き起こす
                confl = cr;
                qhead = trail.size();
                // Copy the remaining watches:
                while (i < end)
                    *j++ = *i++;
            }else                                 //0番目のリテラルが未定なら、それをtrueにするような変数割当を行う
                uncheckedEnqueue(first, cr);

        NextClause:;
        }
        ws.shrink(i - j);                         //trueになった節は邪魔なので配列から除く
    }

    return confl;                                 //矛盾を引き起こす節を返す。勿論null (CRef_Undef) の場合もある
}

割と長いけれど、SATソルバの処理時間の8割をこの propagate 関数が占めるという報告もあり、重要なところである。
あんまり深い意味はないが、トピックを分けるために強引に Block Literal に関する記述を消してる。後述するので許して欲しい

ごちゃごちゃ書いてある割にわかりにくいという事態になってることに気付いてしまった。なんか補足を入れるかも