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

摘要

近年，高速な充足可能性判定ツール（SATソルバ）の開発が進んでいる．これらのツールでは，変数値を次々に推論するBCPという演算がSATソルバの実行時間の大半を占めていることが多く，その処理を効率化できればSATソルバの高速化が可能となる．本論文では，「n個の変数のうち，ちょうどk個が真」という基本対称関数を導入することにより入力する論理式の大きさが減少することに注目し，SATソルバの効率化を目指す．実際にSATソルバでよく用いられるDLLアルゴリズムを基本対称関数を持つCNFに拡張し，その有効性を実験により確かめた．