The Good Old Davis-Putnam Procedure Helps Counting Models

TL;DR

This paper introduces CDP, an algorithm based on the Davis-Putnam procedure, for counting models of propositional formulas, with theoretical analysis and experimental evaluation demonstrating its practical performance.

Contribution

It presents a novel model counting algorithm derived from Davis-Putnam, providing theoretical complexity bounds and empirical performance data.

Findings

Average running time is O(nm^d) with d=-1/log(1-p).

Practical performance is validated through experiments on various formulas.

The algorithm effectively computes exact model counts for CNF and DNF 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, 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.