抄録

○楢崎修二（長崎大）

近年のSATソルバの高速化によりSAT問題への変換による制約問題の解法が注目されて
いる。その高速化手法の一つであるリスタートは、定められた間隔で探索を打切り、
最初からやり直すというものであり、多くのSATソルバで使用されている。この手法の
有効性はリスタート間隔の妥当性による。静的な制御手法としてはバックトラック回
数に基づくLubyアルゴリズムが広く知られている。我々は問題の持つ特徴量からの動
的な制御に注目をした。特徴量として、CDCLアルゴリズムにおける決定レベルとそれ
に基づくバックトラック率に注目をした。本発表では、これらを用いたリスタート制
御アルゴリズムについて述べる。