LBDはリスタートに利用できるのか

学習節の平均 LBD は大きく揺れすぎ。節削減の影響もあるので節の持つ数値は使いにくい気がする。 そんなこともあって、統計処理したからといって探索パラメータとしては使いにくいのではないだろうか。 むしろ個々の学習節の生データで戦略を決定した方がいいかもしれない。ともあれ、データを取ってみよう。

まずは、枝刈り（悪い状態からの離脱）の効果に関して。

A. CHB branch から普通のやつ

v360-c1530: 9 SATs + 1 UNS

T56.2.0.cnf                                3145220,10854665 |time:   721.82
 #conflict:     319339, #decision:      1751376, #propagate:      965031514
  Assignment|#rem:   748607, #fix:     7573, #elm:  2389040, prg%:  76.1986
 Clause Kind|Remv:   105560, LBD2:    35076, Binc:    19760, Perm:  5453978
     Restart|#BLK:     1721, #RST:     1409, eASG:   0.0169, eLBD:   0.6303
    Conflict|aLBD:     4.70, bjmp:     9.00, cnfl:    40.03 |#stg:        0
   Clause DB|#rdc:       12, #sce:      463 |blkR:   1.4000, frcK:   0.7000
    Strategy|mode: Non-Specific-Instance using generic settings

B. そこから force_restart における ema_lbd による起動条件を抜いたもの

v360-c1530: 6 SATs + 3 UNSs

T56.2.0.cnf                                3145220,10854665 |time:   944.43
 #conflict:     341071, #decision:      2311368, #propagate:     1254204513
  Assignment|#rem:   697575, #fix:    32350, #elm:  2415295, prg%:  77.8211
 Clause Kind|Remv:    48361, LBD2:    34735, Binc:    21108, Perm:  4918971
     Restart|#BLK:      620, #RST:     4765, eASG:   0.0195, eLBD:   0.5683
    Conflict|aLBD:     4.92, bjmp:    10.17, cnfl:    51.10 |#stg:        0
   Clause DB|#rdc:       13, #sce:      623 |blkR:   1.5000, frcK:   0.7000
    Strategy|mode: Non-Specific-Instance using generic settings

C. block_restart における ema_asgによる封鎖条件を抜いたもの

n360-v1560: 9 SATs + 1 UNS

T56.2.0.cnf                                3145220,10854665 |time:   605.01
 #conflict:     320514, #decision:      1747366, #propagate:      781715799
  Assignment|#rem:   694683, #fix:    35089, #elm:  2415448, prg%:  77.9131
 Clause Kind|Remv:    74302, LBD2:    34334, Binc:    19331, Perm:  5006638
     Restart|#BLK:     5739, #RST:      662, eASG:   0.0147, eLBD:   0.6291
    Conflict|aLBD:     4.94, bjmp:     9.16, cnfl:    52.13 |#stg:        0
   Clause DB|#rdc:       12, #sce:      395 |blkR:   1.3000, frcK:   0.7000
    Strategy|mode: Non-Specific-Instance using generic settings

わかったこと：

と言うことで悪い状態から脱出する方法はかなり重要。不確実な未来予測（deep search）よりもこちらを優先すべきのようだ。 つまり'measure for forcing blocking'をどう設計するかが問題。そしてコーディングレベルではblock_restartよりもforce_restartの実装がより重要である。EMA of VAD を考えるべきだろうか。。。

そしてなぜ矛盾が発生していない（節にも変数活性度にも影響が及ばない）パスの中に force＿restart が埋め込まれているんだろうか？ 学習節が追加されたら 1 度はpropagateさせる必要がある。だから、そのタイミングで 3 方向分岐すればいいのでは。

なぜ force_restart は無矛盾パスに埋め込まれているか

これは矛盾が起きなくても変化する特徴量＝割り当て率を即時に反映させたいからだろう。 これを backjump level などに置き換えるとリアルタイム性を失ってしまう。 最大到達決定レベル、すなわちc_lvlとの比較なら同等の即時性を持たせることができる。

T56.2 で実験しよう。

using a weighed sum of variable activities in a clause, or weighted SVA.

変数活性度の変化から求解状況の特徴量を抽出しようとして、色々と試したがよい結果にならなかったのでアイデアに戻す(CHB3)。なお、CHB4(decay rate の変更とコードレベルの最適化) からの知見を back port してみたが同じ。

Published at 2019-07-15