CNFSATからHornSATへの変換手法について
スポンサーリンク
概要
- 論文の詳細を見る
本発表では CNFSAT を HornSAT に帰着させる手法について述べる.HornSAT は P 完全問題であり,その充足可能性に関して項どうしが半順序構造を持つという優れた特長を持つ.そのため,HornSAT の各項の影響は局所的となり,コンピュータなどでの取扱いが容易となっている.しかし,CNFSAT は NP 完全問題であり,(CNF の構成によっては) CNF の充足可能性について,ある項が他の項と相互に依存するという構造を持つことがある.そのため,CNFSAT の各項の影響は局所的にはならない.その影響は CNF 全体に及ぶこともあり,結果として CNFSAT を HornSAT に置き換えることを難しくしている.本発表では CNFSAT の構造を HornSAT に置き換えるために,CNF の項どうしの関係に着目した.項どうしの関係は,大きく 2 つに分けることができる.1 つは同じ肯否を持つ変数を共有する関係であり,もう 1 つは異なる肯否となる同じ変数を共有する関係である.これら 2 つの関係それぞれに対応する HornSAT の項を作成し,その制約で CNFSAT の項の関係を構築することで CNFSAT から HornSAT への帰着を実現する.
- 2011-09-22