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

命題論理式の充足可能性を判定するSATソルバの高速化を支える技術の1つにリスタートがある。
見込みのない探索を打ち切り、新たな探索を始めるリスタートは有効性が認められているが、その起動間隔の制御が問題となる。
近年では、高速SATソルバGulcoseで導入された、探索の進行状況を基にした制御戦略が成果を上げている。
Biereらは指数平滑移動平均を用いて実装する手法を示した。
本論文ではこの手法の分析を行い、我々が開発中のSATソルバへ導入するための検討を行う。