DPLLアルゴリズム
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 10:10 UTC 版)
Davis-Putnam-Logemann-Lovelandアルゴリズム（DPLLアルゴリズム、英: Davis-Putnam-Logemann-Loveland algorithm）とは、数理論理学および計算機科学において、論理式の充足可能性を調べるアルゴリズムである。連言標準形で表現された命題論理式を対象とし、論理式を真（True）にできるかどうかを判定する。この判定問題はCNF-SATと呼ばれる。
- ^ a b c Davis, Martin; Logemann, George, and Loveland, Donald (1962). “A Machine Program for Theorem Proving”. Communications of the ACM 5 (7): 394–397.
- ^ a b 例えば、馬野洋平, 他. 基本対象関数に基づく節を持つCNF論理式の充足可能性判定, 電子情報通信学会論文誌D, Vol.J-93-D, No. 1, pp.1-9, 2010. 参照
- ^ Michael Alekhnovich, Edward A. Hirsch, Dmitry Itsykson. Exponential lower bounds for the running time of DPLL algorithms. Journal of Automated Reasoning, Volume35 , Issue1-3 , pp.51-72, 2001.
- ^ Davis Martin. The Early History of Automated Deduction. in Handbook of Automated Reasoning, Volume I, Alan Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498.
[続きの解説]
「DPLLアルゴリズム」の続きの解説一覧
- 1 DPLLアルゴリズムとは
- 2 DPLLアルゴリズムの概要
- 3 歴史
- 4 参考文献
- DPLLアルゴリズムのページへのリンク
