[4K2-OS-16b] AI における離散構造処理と制約充足(2)

[4K2-OS-16b-01] 決定レベルを用いた二つの学習節評価尺度の動的組合せ

〇楢崎 修二¹ (1. 長崎大学)

キーワード：制約充足、論理、SAT

CDCL SATソルバにおいて実行中に獲得される学習節の管理は重要な課題である．多くのソルバでは
削減の基準として節長，活性度，Literal Block Distance(LBD)などの節の評価尺度を導入している．LBDは節
を構成するリテラルの決定レベル数を基にしたもので，よい成果を挙げたた
め，広く使われるようになった．一方，LBDの妥当性に対する異論も存在する．
本稿ではまず、節を構成するリテラルの決定レベルを基にするのではなく，節が依存する全ての決定の個数を尺度として導入する．この尺度は実験ではLBDより悪い性能しか示さないが，LBDを補うものであると考えられる。
そこでソルバの求解中の決定レベルの遷移を考慮して両者を併用する動的な節評価手法を提案する。実験ではこの手法によりLBDを超える結果を得ることができた。