

![0_image_2.png](0_image_2.png)

## Research Note

# The Good Old Davis-Putnam Procedure Helps Counting Models

Institute of Computer Science The Hebrew University 91904 Jerusalem, Israel Elazar Birnbaum elazar@cs.huji.ac.il Eliezer L. Lozinskii lozinski@cs.huji.ac.il

## Abstract

![0_Image_0.Png](0_Image_0.Png)

![0_Image_3.Png](0_Image_3.Png)

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(md n),

where d = d 1 log2 (1p)
e. The practical performance of CDP has been estimated in a series of experiments on a wide variety of CNF formulas.

## 1. Introduction

Given propositional formula F in CNF or DNF, one may want to know what is the number

![0_image_1.png](0_image_1.png)

 F of its models, that is, assignments of truth values to its variables that satisfy F This problem of counting models has numerous applications (Roth, 1996). Many important problem. Among these problems are: (a) Computing degree of belief in propositional statement s with respect to propositional knowledge base KB as conditional probability of s given KB In the absence of sucient statistics this probability can be estimated by KB [ fsg  KB (b) Inference in Bayesian belief networks. As Roth (1996) showed,

![0_image_4.png](0_image_4.png)

c 1999 AI Access Foundation and Morgan Kaufmann Publishers. All rights reserved.