正在学习DPLL算法。
这款软件用于我们学校的实验课。
可图图像化逻辑的表达。寻求合取范式 的解。
详情可见:
http://www-sr.informatik.uni-tuebingen.de/~sinz/DPvis/DPvis.html
11月 14, 2009
DPLL算法软件–DPvis
7月 22, 2009
DPLL 算法
DPLL/Davis-Putnam-Logemann-Loveland 算法 是一种完备的,基于回溯算法的决定CNF型命题逻辑的满足性的算法,即CNF-SAT问题。
它在1962年由Martin Davis, Hilary Putnam, George Logemann 和 Donald W. Loveland 提出,作为早期Davis-Putnam 算法的一种改进。Davis-Putnam 算法是Davis 与 Putnam在1960年发展的一种算法。
尤其是在旧的出版物中,Davis-Logemann-Loveland 算法常常被称为“Davis-Putnam method”或“DP algorithm”。其他常见的名称是DLL和DPLL。DPLL是一种高效的程序,并且经过40多年还是最有效的SAT解法,以及很多一阶逻辑的自动定理证明的基础。