Davis-Putnam程序有助于计算模型
The Good Old Davis-Putnam Procedure Helps Counting Models
摘要：
正如最近所示，许多重要的人工智能问题需要计算命题公式的模型数量。根据目前的知识，在最坏的情况下，计算这种公式的模型的问题是难以解决的。基于Davis-Putnam过程，我们提出了一个算法CDP，它可以计算命题CNF或DNF公式F的精确模型数。设m和n分别为F的子句数和变量数，p表示F的文字l出现在F的子句C中的概率，则CDP的平均运行时间为O（nm^d），其中d=-1/log（1-p）. CDP的实际性能已经在一系列实验中对各种CNF公式进行了估计。
英文摘要：
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, computationally intractable in a worst case. Based on the Davis-Putnam procedure, we present an algorithm, CDP, that computes the exact number of models of a propositional CNF or DNF formula F. Let m and n be the number of clauses and variables of F, respectively, and let p denote the probability that a literal l of F occurs in a clause C of F, then the average running time of CDP is shown to be O(nm^d), where d=-1/log(1-p). The practical performance of CDP has been estimated in a series of experiments on a wide variety of CNF formulas.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
