SAT(命題論理の充足可能性)問題を解くアルゴリズムに関する研究

点击翻译按钮获取中文摘要

今日ではSATソルバーは、回路の等価性検証、モデル検査など、幅広い分野で探索エンジンとして用いられている。それらの実用性の高い問題に対して用いられるSATソルバーの殆んどはDPLLアルゴリズムをベースにしている。DPLLアルゴリズムには、この10年ほどの間に多種多様なアイデアが付加されている。近年のDPLLベースの探索アルゴリズムでは、仮定に仮定を重ね、探索中に矛盾を導いては、それを回避するための制約条件を積極的に学習することによって探索範囲を狭める仕組みになっている。DPLLでは、ある種の制約条件を学習する際に、今までの探索をすべて放棄して、rootまで戻ることになっている。本年度の研究では、まず実用的にはその状況の際に、いつもrootまで戻るのが良いとは限らないことを明らかにした。学習内容が重要であることは言うまでもないが、それに至る探索過程もそれなりに尊重しても良い、ということである。その上で、rootまで遡るのではなく、ある簡単なヒューリスティックスに従って途中まで探索を戻す手法を提案した。提案手法の有効性の実験的確認として、SATの世界最大規模のコンペティションである、SAT Race 2006の問題に対して適用し、若干ながら提案手法の優位性が認められた。提案手法は、ここで問題としている、ある種の制約条件の学習という状況が発生しなければ、従来法と全く同じ振る舞いになるので、従来法に比べて大きな欠点はない。