|
===================================== 〔語彙分解〕的な部分一致の検索結果は以下の通りです。
Davis-Putnam-Logemann-Lovelandアルゴリズム（DPLLアルゴリズム、）とは、数理論理学および計算機科学において、論理式の充足可能性を調べるアルゴリズムである。連言標準形で表現された命題論理式を対象とし、論理式を真（True）にできるかどうかを判定する。この判定問題はCNF-SATと呼ばれる。 このアルゴリズムは、1960年に発表されたデービス・パトナムのアルゴリズム（）の改良版として、1962年にMartin Davis、George Logemann、Donald W. Lovelandが発表した 〔 〕。 なお、文献によってはDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し〔、正確には異なる。 == 概要 == DPLLアルゴリズムは、その前身であるデービス・パトナムのアルゴリズムと同様、一階述語論理での定理自動証明で必要だった、命題論理式の充足可能/不能のチェックを効率的に行うために考案されたアルゴリズムである。いくつかの規則を用いることで充足可能であることが分かっている論理式を効率的に削除し、無駄な判定を省いている。 その効率性のため、現在でも命題論理式の充足可能性問題を扱う多くのツールでDPLLアルゴリズムは基本アルゴリズムとして用いられている〔例えば、馬野洋平, 他. ''基本対象関数に基づく節を持つCNF論理式の充足可能性判定'', 電子情報通信学会論文誌D, Vol.J-93-D, No. 1, pp.1-9, 2010. 参照〕。 1960年に提案されたデービス・パトナムのアルゴリズムとの違いは、''原子論理式除去規則''（'）と呼ばれる規則の代わりに、使用メモリの削減のため''分割規則''と呼ばれる規則を使用することである。通常、この規則はバックトラックを用いて実行される。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「DPLLアルゴリズム」の詳細全文を読む スポンサード リンク
|