Good old Davis-Putman procedure helps counting models

111Citations
Citations of this article
24Readers
Mendeley users who have this article in their library.

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, 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(mdn), where d = [-1/log2(1-p)]. The practical performance of CDP has been estimated in a series of experiments on a wide variety of CNF formulas.

Cite

CITATION STYLE

APA

Birnbaum, E., & Lozinskii, E. L. (1999). Good old Davis-Putman procedure helps counting models. Journal of Artificial Intelligence Research, 10, 457–477. https://doi.org/10.1613/jair.601

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free