情報処理学会 第79回全国大会講演要旨

近年の高速化により命題論理式の充足可能性判定器であるSATソルバーは制約問題として解釈できる様々な問題へと応用されている。その基盤となっているのが、論理制約伝播による問題空間の探索と矛盾からの学習による非時間順序バックトラックとを組み合わせたCDCLアルゴリズムである。現在の主な研究は、データ構造や探索ヒューリスティックス、並列処理、強化学習といった観点からの改良をこの枠組に加えるものである。本論文では、そのような試みの一つとして、矛盾の検出によるバックトラックの実行条件を緩和する手法を提案する。これによりCDCL SATソルバーにどのような性能の変化が期待できるかを説明する。