基本対称関数を付加したCNF論理式の充足可能性判定

摘要

近年，高速な充足可能性判定ツール（SATソルバ）の開発が進んでいる．これらのツールでは，変数値を次々に推論するBCPという演算がSATソルバの実行時間の大半を占めていることが多く，その処理を効率化できればSATソルバの高速化が可能となる．本論文では，「n個の変数のうち，ちょうどた個が真」という基本対称関数を導入することにより入力する論理式の大きさが減少することに注目し，SATソルバの効率化を目指す．実際にSATソルバでよく用いられるDLLアルゴリズムを基本対称関数を持つCNFに拡張し，その有効性を実験により確かめた．%In recent years, several efficient SAT solvers, which decide satisfiability of boolean formulas, have been developed. Since BCP module, which propagates variable values in succession, often consumes most of running time of SAT solvers, the total efficiency will be improved if we succeed in reducing the process of BCP. In this paper, we attempt to improve the efficiency of SAT solvers from the observation that the number of clauses of a CNF formula is decreased by introducing the notion of elementary symmetric functions. We incorporated the notion into the DLL algorithm, implemented a SAT solver based on the extended algorithm and confirmed its effectiveness from experiments.