BriefGPT.xyz
Jun, 2011
Davis-Putnam 程序在计数模型中的应用
The Good Old Davis-Putnam Procedure Helps Counting Models
HTML
PDF
E. Birnbaum, E. L. Lozinskii
TL;DR
通过使用 Davis-Putnam 算法，提出了一种算法 CDP，用于计算 CNF 或 DNF 公式的模型的准确数量，该算法的平均运行时间是O(nm^d)，在大量的 CNF formulas 实验中的实际表现已经被估计。
Abstract
As was shown recently, many important
ai problems
require counting the number of models of
propositional formulas
. The problem of counting models of such formulas is, according to present knowledge, computational
→