\documentstyle[jair,twoside,11pt,theapa]{article}

\input epsf %% at top of file

\jairheading{10}{1999}{457-477}{11/98}{6/99}

\ShortHeadings{Davis-Putnam Procedure Helps Counting Models}
{Birnbaum \& Lozinskii}

\firstpageno{457}


\begin{document}

\title{The Good Old Davis-Putnam Procedure Helps \\
       Counting Models}

\author{\name Elazar Birnbaum \email elazar@cs.huji.ac.il \\
        \name Eliezer L. Lozinskii \email lozinski@cs.huji.ac.il \\
        \addr Institute of Computer Science \\
        The Hebrew University \\
        91904 Jerusalem, Israel}

% For research notes, remove the comment character in the line below.
\researchnote

\maketitle

\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}


\begin{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 {\it F\/}. Let {\it m\/}
and {\it n\/} be the number of clauses and variables of {\it F\/}, 
respectively, and let {\it p\/} denote the probability that a 
literal {\it l\/} of {\it F\/} occurs in a clause {\it C\/} of {\it F\/}, 
then the average running time of CDP is shown to be $O(m^dn)$, 
where $d=\lceil\frac{-1}{\log_2(1-p)}\rceil$. The practical performance
of CDP has been estimated in a series of experiments on a wide variety of
CNF formulas.

\end{abstract}


\section{Introduction}

Given a propositional formula {\it F\/} in CNF or DNF, one may want to know 
what is the number $\mu(F)$ of its models, that is, assignments of
truth values to its variables that satisfy {\it F\/}. This problem of {\em
counting models\/} has numerous applications \cite{roth}.
Many important AI problems require
counting models of propositional formulas or are reducible to this problem.
Among these problems are:
(a) Computing degree of belief in a propositional statement $s$ with respect
to a propositional knowledge base $KB$ as a conditional probability of $s$
given $KB$. In the absence of a sufficient statistics this probability can
be estimated by
$|\mu(KB \cup \{s\})| \hspace*{0.5mm} / \hspace*{0.5mm} |\mu(KB)|$.
(b) Inference in Bayesian belief networks. As \citeA{roth} showed, the problem
of counting models of a propositional formula can be reduced to the problem
of computing the probability that a node in a Bayesian belief network is true.
(c)~Computing the number of solutions of a constraint satisfaction problem.
A CNF formula $F$ on $n$ variables $x_1, \ldots ,x_n$ may be regarded as a
constraint satisfaction problem in which the domain of each variable is
$\{0,1\}$, and each clause $C$ is a relation $R \subseteq \{0,1\}^n$
of all n-tuples for which at least one literal of $C$ assumes the value 1.
Then the problem of computing the number of solutions of such problems is
the one of computing $\mu(F)$.
(d) Estimating the utility of reasoning with approximate theory $AT$
instead of the original theory $T$. This utility depends on the size
of $|\mu(AT)|-|\mu(T)|$ \cite{roth}.

Another important application is to reasoning with incomplete information
\shortcite{grove,lozinskii1,lozinskii3}.
Indeed, if {\it F\/} describes a real world {\it W\/} faithfully, then 
given a formula $\phi$ such that neither $\phi$ nor $\neg\phi$ is a 
logical consequence of {\it F}, a reasonable assumption is that the more 
models of {\it F\/} assert $\phi$, the more likely is that $\phi$ is true 
in {\it W}. 

The problem of counting models is \#P-complete in general 
\cite{valiant}, and so, according to the present state of the art in the
field, computationally intractable in the worst case. 
\citeA{dubois} introduced an algorithm that
for any formula {\it F\/} of $n$ variables and $m$ clauses, each clause
containing $r$ literals, counts models of {\it F\/} in time
$O(m \alpha_r^n)$, $\alpha_r$ being the positive root of
the polynomial $y^r - y^{r-1} - \cdots-1$
($\alpha_2 \approx 1.62, \alpha_3 \approx 1.84, \alpha_4 \approx 1.93, 
\ldots$ and $\lim_{r \rightarrow \infty} \alpha_r = 2$). Recently, 
\citeA{zhang} presented an algorithm based on similar ideas and with similar
time complexity. The time complexity achieved by these algorithms is an 
important improvement over that of a naive algorithm which checks all
assignments of truth values to the variables of a formula {\it F\/}
in time $O(m2^n)$.

To satisfy practical applications, one has 
either to resort to a good {\em approximation\/} of $\mu(F)$, or use an 
algorithm for computing $\mu(F)$ {\em exactly\/} with a reasonable 
{\em average\/} time complexity.

Regarding the first alternative, \citeA{luby} 
presented a deterministic algorithm for approximating the proportion of truth 
assignments that satisfy a DNF formula {\it F}. Let $Pr[F]$ denote 
this proportion ($Pr[F] = \mu(F) / 2^n$ where {\it n\/} is the number of 
variables of {\it F}).  
Given small numbers $\epsilon, \delta > 0$, 
the algorithm computes an estimate {\it Y\/} of $Pr[F]$ which satisfies 
$$(1-\delta) Pr[F] - \epsilon \leq Y \leq Pr[F] + \epsilon.$$ 

Let {\it m\/} and {\it n\/} be the number of clauses and variables of 
{\it F}, respectively. The running time of the algorithm is estimated 
by a polynomial in {\it n\/} and {\it m\/} multiplied by 
$$n^{O(\frac{1}{\delta}(\log^2m+\log^2\frac{1}{\epsilon})
(\log\log m+\log\frac{1}{\epsilon}+\log\frac{1}{\delta}))}.$$
So, the running time of the algorithm grows fast with the 
precision required.

\citeA{linial} studied the  problem of computing the size 
of a union of a given family of sets $S_1 \cup S_2 \cup \cdots \cup S_m$ 
by means of the Inclusion-Exclusion formula
$$|\bigcup_{i=1}^{m} S_i| \ = \sum_{1 \leq i \leq m} |S_i| \ -
\sum_{1 \leq  i < j  \leq  m} |S_i \cap S_j| \ + 
\sum_{1 \leq i < j < k \leq m} |S_i \cap S_j \cap S_k| \ - \cdots$$
\begin{equation} + (-1)^{m+1} |S_1 \cap \cdots \cap S_m|.
\label{incexc}
\end{equation}

They showed that the size of the union can be 
approximated accurately when the sizes of only part of the set intersections
are known. Suppose the intersection sizes are known for all subfamilies 
containing at  most {\it k\/} sets. If $k \geq \Omega (\sqrt{m})$, then the
union size can be approximated with a  relative error of 
$O(e^{-2k/\sqrt{m}})$.

As \citeA{linial} pointed out, this result can be
applied to approximating the number of models of a DNF formula {\it F} ---
each clause of {\it F\/} has its set of models, and $\mu(F)$ is equal to
the size of the union of all those sets. Thus, only the first {\it k\/}
terms of the formula (\ref{incexc}) are needed for a good approximation,
where $\sqrt{m} \leq k \leq m$. However, for a high precision, {\it k\/} 
approaches {\it m}. For instance, for $m=100$ and an error of $10^{-3}$, 
$k \approx 34.$

\citeA{iwama} introduced an algorithm for testing satisfiability
of a CNF formula {\it F\/} over $n$ variables by counting the truth
assignments falsifying {\it F\/} and checking if their number is less
than $2^n$. The counting is accomplished through an Inclusion-Exclusion
process, where the size of the set of truth assignments falsifying
{\it F\/} is computed with the aid of the observation that this set is the
union of the sets of truth assignments falsifying each clause of {\it F\/}.
Iwama analyzed the average running time of his algorithm on the
same framework as we did for the algorithm we present in the sequel.
He showed that for a CNF formula satisfying the condition that for a
constant $c$, such that $\ln c \geq \ln m - p^2n$, where $n$ is the number
of variables, $m$ is the number of clauses, and $p$ is the probability that
a given literal appears in a clause (the same for all literals), the
average running time of the algorithm is $O(m^{c+1})$.

\citeA{lozinskii2} employed an algorithm which is similar to that
presented by \citeA{iwama}, for counting models. He showed
that under reasonable assumptions, the average running time of computing
the exact number of models of a formula with {\it m\/} clauses on {\it n\/}
variables is $O(m^cn)$, where $c=O(\log m)$.

In the sequel we present an algorithm which we call CDP (Counting
by Davis-Putnam) for computing $\mu(F)$ precisely.
Algorithm CDP is based on the Davis-Putnam procedure (DPP) \cite{davis}
for solving the satisfiability problem (SAT). We study features of DPP, and
show how its rules can be modified, resulting in an algorithm for counting
models. An analysis shows that for a formula {\it F\/} with {\it m\/} clauses
on {\it n\/} variables, the average running time of CDP is
$O(m^dn)$, where $d=\lceil\frac{-1}{\log_2(1-p)}\rceil$, and {\it p\/} is
the probability that any literal occurs in a given clause. 

Section \ref{experiments} describes numerous experiments with CDP showing
that its actual average time complexity is significantly lower than the
upper bounds provided by mathematical analysis in Section \ref{average}
and in previous works \cite{dubois,iwama,lozinskii2,zhang}. We also point
out advantages of this new algorithm over the ones presented in these
previous works.
Finally, we estimated CDP performance on formulas with 3-literal clauses,
and compared the results to those of checking the satisfiability of such
formulas by DPP presented by \shortciteA{mitchell}.


\section{Algorithm for Counting Models}

In the sequel we consider propositional formulas over a set 
$V = \{ x_1, \ldots, x_n \}$ of variables, {\it l\/} denotes a literal 
($l \in \{ x_1, \ldots, x_n, \bar{x}_1, \ldots, \bar{x}_n \}$), and
$\bar{l}$ stands for the negation of {\it l\/}. 


\subsection{The Davis-Putnam Procedure}
\label{dpp}

The Davis-Putnam procedure (DPP) \cite{davis} is intended for deciding 
satisfiability of a propositional CNF formula {\it F\/} (regarded as a set 
of clauses), and can be presented as a recursive boolean function 
(assuming that no clause of {\it F\/} is a tautology):

\vspace{2mm}
\noindent \hspace*{3.7mm} function DPP ({\it F\/}: propositional CNF formula);
\vspace*{-3pt}
\begin{enumerate}
\item if $F$ is empty then\\
      \hspace*{1em} return {\it true};
\vspace*{-7pt}
\item if {\it F\/} contains an empty clause then\\ 
      \hspace*{1em} return {\it false};
\vspace*{-7pt}
\item (* The pure literal rule  *) \\
      if there exists a pure literal {\it l\/} in {\it F\/} (* such that 
      $\bar{l}$ does not appear in {\it F\/} *) then\\
      \hspace*{1em} $F_1 = \{ C \ | \ C \in F, l \not\in C \}$; 
      (* delete from {\it F\/} all clauses containing {\it l\/} *)\\
      \hspace*{1em} return DPP($F_1$); 
      (* {\it F\/} is satisfiable iff $F_1$ is so *)
\vspace*{-7pt}
\item (* The unit clause rule *) \\
      if {\it F\/} contains a unit clause $\{ l \}$ (* a clause consisting 
      of a single literal *) then\\
      \hspace*{1em} $F_1 = \{ C - \{ \bar{l} \} \ | \ C \in F , l \not\in C \}$; 
      (* delete from {\it F\/} $\bar{l}$ and all clauses containing {\it l\/} *) \\ 
      \hspace*{1em} return  DPP($F_1$); 
      (* {\it F\/} is satisfiable iff $F_1$ is so *)
\vspace*{-7pt}
\item (* The splitting rule *) \\
      choose a variable {\it x\/} of {\it F\/};\\ 
      $F_1 = \{ C - \{ \bar{x} \} \ | \ C \in F , x \not\in C \}$;\\
      $F_2 = \{ C - \{ x \} \ | \ C \in F , \bar{x} \not\in C \}$;\\
      return (DPP$(F_1) \ \lor$ DPP$(F_2)$). (* {\it F\/} is satisfiable
      iff $(F_1  \lor   F_2)$ is so *) 
\end{enumerate}

It can be seen that the pure literal rule and the unit clause rule are 
actually particular cases of the splitting rule. If there exists a pure 
literal {\it l\/} in {\it F}, and the splitting rule chooses {\it l\/}, 
then $F_1 \subseteq F_2$, and hence $(F_1 \lor F_2)$ is satisfiable iff 
$F_1$ is so. According to the splitting rule, {\it F\/} is satisfiable
iff $(F_1 \lor F_2)$ is so, and hence, {\it F\/} is satisfiable iff
$F_1$ is so. This is exactly the pure literal rule.

If {\it F\/} contains a unit clause $\{ l \}$, and the splitting rule 
chooses {\it l}, then $F_2$ contains an empty clause (the unit clause 
without its only literal), and so, is unsatisfiable. So, {\it F\/} is 
satisfiable iff $F_1$ is so. This is the unit clause rule. 
(Incidentally, the splitting rule treats well tautological clauses too. 
If a clause {\it C\/} of {\it F\/} contains a literal {\it l\/} and its
complement $\bar{l}$, and the splitting rule is applied to {\it l}, then 
{\it C\/} will be erased from both $F_1$ and $F_2$.)

Thus, we may consider DPP as being based on the splitting rule only, while 
the two other rules serve as guides for choosing a literal efficiently. 
Indeed, if {\it F\/} contains a unit clause $\{ l \}$ or a pure literal 
{\it l}, then applying the splitting rule to {\it l\/} 
yields only {\em one\/} formula, but choosing a non-pure 
and non-unit-clause literal leaves two formulas for further processing. 

If {\it F\/} contains neither a unit clause nor a  pure literal, then the 
literal for the splitting rule should be chosen in such a way that produces 
sets $F_1$ and $F_2$ that are as small as possible. We address this issue
in the sequel.


\subsection{Counting Models}

Thinking of counting models of a propositional formula {\it F}, we notice that
by choosing a variable {\it x}, the splitting rule actually splits the set of 
models of {\it F\/} into two disjoint subsets: one in which {\it x\/} is true 
(namely, the models of $F_1$), and the other (models of $F_2$) in which 
{\it x} is false. The chosen variable {\it x\/} appears neither in $F_1$ nor 
in $F_2$, and there may be other variables that appear in {\it F} but not 
in $F_1$ (or not in $F_2$). These are the variables which belong only to 
the clauses that contain the literal {\it x\/} (or $\bar{x}$, respectively). 
Hence, every model of $F_1$ ($F_2$) can be completed to a model of {\it F\/} 
by assigning {\it true\/} ({\it false}, respectively) to {\it x},
and {\it true\/} or {\it false\/} arbitrarily to every variable of {\it F\/} 
that does not appear in $F_1$ ($F_2$, respectively). Let $\mu(F)$ stand for 
the number of models of {\it F}, and $n_1 \ (n_2)$ denote the number of 
variables (other than {\it x}) which occur in {\it F\/} but not in 
$F_1 \ (F_2)$, then $\mu(F) = 2^{n_1}\mu(F_1) + 2^{n_2}\mu(F_2)$.

As it has been shown in Section \ref{dpp}, if checking satisfiability is the goal, 
and a pure literal (which is not a unit clause) is chosen for splitting, 
then only $F_1$ should be processed further, while $F_2$ may be disregarded. 
However, for counting models both $F_1$ and $F_2$ matter. Note that in this 
case $F_2$ contains the same number of clauses as {\it F}. So, in contrast 
to checking satisfiability, the pure literal rule turns out to be 
inefficient for counting models. 

Based on these observations, the following function CDP counts models of
a formula {\it F\/} over {\it n\/} variables.

\vspace{2mm}
\noindent \hspace*{3.7mm} function CDP
({\it F\/}: propositional CNF formula; {\it n\/}: integer);
\vspace*{-3pt}
\begin{enumerate}
\item if $F$ is empty then\\
      \hspace*{1em} return $2^n$;
\vspace*{-7pt}
\item if {\it F\/} contains an empty clause then\\
      \hspace*{1em} return 0;
\vspace*{-7pt}
\item if {\it F\/} contains a unit clause $\{ l \}$ then\\
      \hspace*{1em} $F_1 = \{ C - \{ \bar{l} \} \ | \ C \in F ,
      l \not\in C \}$;\\
      \hspace*{1em} return  CDP($F_1,n-1$);
\vspace*{-7pt}
\item choose a variable {\it x\/} of {\it F};\\ 
      $F_1 = \{ C - \{ \bar{x} \} \ | \ C \in F , x \not\in C \}$;\\
      $F_2 = \{ C - \{ x \} \ | \ C \in F , \bar{x} \not\in C \}$;\\
      return CDP$(F_1,n-1)$ + CDP$(F_2,n-1)$.
\end{enumerate}

Any iteration of CDP deletes the chosen variable, and so, reduces 
the number of variables of {\it F\/} by at least one. This guarantees that 
CDP terminates (either on step 1 or on step 2).
 

\section{Average Running Time}
\label{average}

In the analysis of the average running time of the function CDP we 
follow \citeA{goldberg1} and \shortciteA{goldberg2}, who studied
the average running time of DPP.

\subsection{The Recurrence Equation}

Let {\it m\/} and {\it n\/} denote the number of clauses and variables of
{\it F}, respectively. Assume that all the literals have the same
probability {\it p\/} to appear in each clause {\it C\/} of {\it F}.  
(To simplify the analysis we allow {\it F\/} to contain duplicate 
clauses and tautologies.) Assume also that there is no dependency among 
the occurrences of different variables and among
the occurrences of the same variable in different clauses. For a given 
distribution of {\it p}, let $T(m,n)$ denote the average 
running time of CDP$(F,n)$ with {\it F\/} containing {\it m\/} clauses.

If {\it F\/} contains {\it m\/} clauses on {\it n\/} variables, then {\it mn\/}
bounds the size of {\it F}. Each step of function CDP can be accomplished 
during at most two passes over {\it F}. 

\begin{lemma}
If {\it F\/} contains {\it m\/} clauses on {\it n\/} variables, then there 
is a constant {\it c\/} such that {\it cmn} bounds the time of executing 
one iteration of function CDP.
\label{cmn}
\end{lemma}

It might be thought, that in order to obtain a good bound on the average
running time of function CDP, one must show that the
unit clause rule is applied frequently, since the splitting rule is the
one that introduces the possibility of exponentially long computations.
We show that even if only the splitting rule is applied, low bounds are 
obtained. Therefore, we assume that no use of the unit clause rule is made,
and analyze a variant of CDP, in which step 3 is omitted. Obviously, this 
change does not affect Lemma \ref{cmn}. We also assume that the literal
for the splitting rule is chosen randomly.

Let {\it l\/} be the literal that has been chosen for the splitting rule.
Since the probability that {\it l\/} occurs in a clause is {\it p}, the
probability that {\it k\/} out of {\it m\/} clauses contain {\it l\/} is 
$(_k^m)p^k(1-p)^{m-k}$. The same holds for $\bar{l}$. The number of clauses 
of formulas $F_1$, $F_2$ produced by splitting {\it F\/} is equal to the 
number of all clauses of {\it F\/} minus the number of clauses of {\it F\/} 
which contain the literal {\it l}, $\bar{l}$, respectively.

\begin{lemma}
Each of formulas $F_1$, $F_2$ produced by splitting {\it F\/} contains 
$m-k$ clauses with probability $(_k^m)p^k(1-p)^{m-k}$. 
\end{lemma}

Since each of $F_1$, $F_2$ contains at most $n-1$ variables, the following 
recurrence inequality for $T(m,n)$ holds.
\begin{equation}
T(m,n) \leq \left\{
\begin{array}{ll}
cmn +\\
\sum_{k=1}^m (_k^m) p^k (1-p)^{m-k} T(m-k,n-1) +\\  
\sum_{k=0}^m (_k^m) p^k (1-p)^{m-k} T(m-k,n-1) &  \ \ \ \ n,m \geq 1 \\
\\
1  & n=0 \ or \ m=0
\end{array} \right.
\label{tmn}
\end{equation}
The first term $(cmn)$ is the time needed for one iteration of CDP. The 
second and third terms are the expected times needed for computing the 
number of models of $F_1$ and $F_2$, respectively. Since the literal {\it l} 
appears in {\it F}, it is impossible that the number of clauses in which 
{\it l\/} occurs is 0, and so, the summation of the second term starts at 1.
The literal $\bar{l}$ may not appear at all in {\it F\/} (if {\it l\/} 
is pure). Consequently, the summation of the third term begins at 0. 

The right-hand side of (\ref{tmn}) overestimates $T(m,n)$ since, first, the 
number of 
variables of $F_1$, $F_2$ is {\em at most} $n-1$, and, second, function 
CDP may stop when {\it F\/} contains an empty clause, even before 
{\it m\/} or {\it n\/} becomes 0.

To estimate $T(m,n)$, we show, first, that for $p=1/3$, 
$T(m,n) = O(m^2n)$, and, second, that for any {\it p}, 
$T(m,n) = O(m^dn)$ where $d=\lceil\frac{-1}{\log_2(1-p)}\rceil.$


\subsection{The Average Running Time for $p=1/3$}

Following \citeA{goldberg1}, we start with the analysis of the 
average running time for $p=1/3$. In this case, each variable occurs 
in each clause positively, negatively or not at all with the same probability 
$(1/3)$. So, recurrence (\ref{tmn}) takes the form
\begin{equation}
T(m,n) \leq \left\{
\begin{array}{ll}
cmn +\\
(\frac{2}{3})^m  T(m,n-1) +\\
2\sum_{k=1}^m (_k^m) (\frac{1}{3})^k (\frac{2}{3})^{m-k} T(m-k,n-1) 
&  \ \ \ \ m,n \geq 1\\  
\\
1  & n=0 \ or \ m=0
\end{array} \right.
\end{equation}
\begin{theorem}
For $p = \frac{1}{3}$, $T(m,n) = O(m^2n).$ 
\end{theorem}
Proof is given in Appendix A.


\subsection{The Average Running Time for Any {\it p\/}}

The assumption of $p=1/3$ is commonly adopted in probabilistic analysis of 
algorithms handling CNF or DNF formulas \cite{franco,goldberg1,goldberg2}, 
which means that for each variable, its occurrence in a clause with or 
without negation or non-occurrence, all have the same probability.
However, in real cases this may not hold, so we analyze 
the average running time of CDP for any probability {\it p} of a literal
occurrence in a clause of {\it F}.

Before analyzing the recurrence equation let us make the following estimation.
The function CDP (without the unit clause rule) may be regarded as an 
algorithm which scans a binary tree. The root of the tree represents the 
input formula {\it F}; The children of each internal node represent the 
formulas obtained as a result of applying the splitting rule to the formula 
at that internal node, and the leaves of the tree represent empty formulas 
and formulas which contain an empty clause. 

If an internal node represents a formula with {\it k\/} clauses, the 
expected number of clauses in each of its children is $k(1-p)$. 
The expected height of the tree {\it h\/} is therefore about $\log _b m$ where 
$b = \frac{1}{1-p}$. The number of nodes in a complete binary tree of height 
{\it h\/} is about $2 \cdot 2^h$, and this is the expected number $\eta$ 
of iterations of the function CDP. So, $\eta = 2 \cdot 2^h = 2m^d$, where 
$d = \frac{-1}{\log_2(1-p)}$. The running time of each iteration is 
$O(\tilde{m}\tilde{n})$ where $\tilde{m}$ is the number of clauses 
and $\tilde{n}$ is the number of variables of the formula that is 
treated at that iteration.
\vspace*{-7pt}
\begin{theorem}
$T(m,n)=O(m^dn)$, where $d = \lceil \frac{-1}{\log_2(1-p)} \rceil$.
\label{tmntheorem}
\end{theorem}
\vspace*{-7pt}
Proof is given in Appendix A.

A few remarks are in order. First, we assumed that the probability of
occurring in a clause is the same for all literals. If this is not the case,
then Theorem \ref{tmntheorem} holds for {\it p\/} being the lowest
occurrence probability among all literals of {\it F}. Second, if {\it p\/}
is assumed constant, then the size of clauses, which is of order $2pn$,
is proportional to the number of variables, and hence, is supposed to
change with {\it n}. 


\section{Refining the CDP}

This section describes some refinements to CDP improving its performance.

\subsection{Choosing a Variable for the Splitting Rule}

The function CDP, like the Davis-Putnam procedure, gives no recommendation 
how to choose a variable for a split. However, a good choice of this 
variable may reduce the running time of the function. By `good choice' we 
mean one that causes the formulas $F_1$ and $F_2$ to be as small as possible. 

The size of these formulas is determined by both {\it m\/} and {\it n}.
As minimizing the number of variables in $F_1$, $F_2$ causes an unjustified 
computation overhead, we concentrated on reducing the number of clauses $m_1$,
$m_2$ in $F_1$, $F_2$, either by minimizing $m_1+m_2$ (by means of choosing
a variable appearing in a maximal number of clauses of {\it F}), or by 
minimizing $max(m_1,m_2)$. The latter can be achieved by maximizing over 
{\it x\/} the quantity $min(pos(x),neg(x))$, where $pos(x)$ ($neg(x)$) denotes
the number of clauses  of {\it F\/} in which {\it x\/} occurs unnegated 
(negated, respectively). These two approaches may be combined. Indeed, 
experiments reported in Section \ref{experiments} showed best performance
if the split variable has been chosen due to $min(m_1+m_2)$, but if there
have been more than one such variable, then a further choice among the
competing variables has been made due to $minmax(m_1,m_2)$. 

As has been suggested by an anonymous reviewer, by using proper data
structures, the computation of $pos(x)$ and $neg(x)$ for all variables
{\it x\/} can be done efficiently, causing only a small computation overhead.


\subsection{Handling Small Formulas}

The function CDP stops when {\it F\/} contains an empty clause or when 
{\it F\/} is empty. What if {\it F\/} consists of only one clause 
containing {\it k\/} literals? The splitting rule will be applied to 
{\it F\/}, creating $F_1$ and $F_2$ such that one of them may be empty,
but the other still consists of one clause involving just one variable less 
than {\it F}. So, splitting of the single clause of {\it F\/} will be 
repeated $k$ times. 

A similar process of inefficient splitting takes place also on formulas
consisting of relatively few clauses. It turns out that the algorithm
presented by \citeA{lozinskii2} is more efficient for handling
small sets of clauses. Experiments on randomly chosen formulas showed that
for formulas with less than 6 clauses the algorithm of 
\citeA{lozinskii2} performs better than function CDP in its original form.
Therefore, when the number of clauses of a formula being processed is reduced
under 6, CDP runs the algorithm of \citeA{lozinskii2}.


\section{Experiments}
\label{experiments}

Algorithm CDP presented in the previous sections
has been programmed in {\sc Turbo-Pascal}, and run on PC, with the
purpose of determining an efficient way of choosing a variable for the
splitting rule, finding an appropriate number of clauses in a
formula for switching the function CDP to the algorithm of 
\citeA{lozinskii2}, and assessing the actual running time of CDP.

In the experiments, CDP has been applied to randomly produced
sets of clauses with the following parameters: $10 \leq m \leq 200$, 
$10 \leq n \leq 80$ and $p_1,p_2 \in \{ 0.1,0.2,0.3 \}$, where $p_1$, $p_2$ 
denote the probability of a variable to occur in a clause unnegated or 
negated, respectively ($p_1$ and $p_2$ are not necessarily the same).
For each combination of the parameters, 100 random instances of
{\it F\/} have been processed. Performance of CDP has been measured by its
running time and by the number of recursive calls to the main function.

We have observed that for each pair of probabilities $p_1, p_2$, there is
a threshold number of clauses $\bar{m}$, such that for $m \geq \bar{m}$
the hard cases lie around a corresponding number of variables. For instance,
the hard cases for $p_1=p_2=0.1$ and $\bar{m}=60$ are located around $n=50$.
Figures \ref{avecalls1} and \ref{avecalls2} present the average number
of recursive calls performed by CDP in the hard cases. More data are given
in Tables 1-6 of Appendix B. Following a suggestion
of one of the reviewers, we checked the standard deviation in all cases
(see Table \ref{stdev} in Appendix B).
All the experiments ran on a pentium based PC (266 MHz). The actual
running time of CDP ranged from less than one second to 5 hours.
\vspace*{20pt}
\begin{figure}[ht]
\begin{center}
\epsfxsize=225pt \epsfbox{fig1.eps}
\caption{Average number of recursive calls for different values of $p1,p2$}
\label{avecalls1}
\end{center}
\end{figure}
\vspace*{-10pt}
\begin{figure}[ht]
\begin{center}
\makebox[0.9\textwidth]{\epsfxsize=225pt \epsfbox{fig2.eps}}
\caption{Average number of recursive calls for different values of $p1,p2$
(continued)}
\label{avecalls2}
\end{center}
\end{figure}

Following the discovery of hard cases for SAT \cite{mitchell}, we ran
CDP on a series of random sets of 3-literal clauses with the 
ratio of $m/n$ from 0.2 to 8.0. For each combination of $m$ and $n$,
200 instances were considered.
Figure \ref{threeliterals} gives the median number of recursive calls
performed by CDP for a sample of $n = 20,40,50$. More data in Table
\ref{threetable} of Appendix B. \cite<Median number
is shown to enable comparison with the results presented by>{mitchell}.
\vspace*{15pt}
\begin{figure}[ht]
\begin{center}
\epsfxsize=225pt \epsfbox{fig3.eps}
\end{center}
\vspace*{-5pt}
\caption{Median number of recursive calls for 3-literal formulas.}
\label{threeliterals}
\end{figure}

In all experiments with counting models we have observed a phenomenon akin
to that characteristic of checking satisfiability, namely, for a
given length of clauses $r$, the running time of algorithm CDP reaches its
maximum at a certain value of the clauses-to-variables ratio. For $r=3$
(Figure \ref{threeliterals}) this ``hard" ratio is 1.2, while it has
been reported in many works (e.g., Mitchell et al., 1992) that hard
cases of 3-SAT lie around $m/n = 4.3$. This shift of the maximum
running time to the left (from $m/n = 4.3$ to $m/n = 1.2$) can be
explained by the fact that when a program for SAT discovers a satisfying
assignment, it stops processing, while counting models has to go on
over all satisfying assignments. So, the higher is the probability that
a formula is satisfiable, and the more models it is likely to have
(and this is what happens if the ratio $m/n$ decreases), the longer
model counting takes compared to checking satisfiability.


\section{Concluding Remarks}

We have presented an algorithm (CDP) for counting models of a
propositional formula {\it F\/}. The previous sections considered
CNF formulas, however, it is easy to construct a dual algorithm for
DNF formulas.

Comparing algorithm CDP with that of \citeA{iwama} and \citeA{lozinskii2},
we note that both have a common central feature: the more variables have both
negated and unnegated occurrences in the clauses of a given formula, 
the better is the performance of the algorithms. This feature is
also common to the algorithms presented by \citeA{dubois} and by \citeA{zhang}.
In contrast to checking satisfiability, pure literals slow down counting
models by these algorithms.

The experiments made with algorithm CDP have shown that it performs better
than that of \citeA{lozinskii2}. However the main advantage
of CDP is in the amount of storage it requires. In the experiments that
have been performed by \citeA{lozinskii2} for $m \leq 100$
and $n \leq 30$, there were cases with thousands of clauses stored during
the run of the algorithm.
Since algorithm CDP performs a depth-first search of the split tree,
and by each split at least one variable is deleted, the maximal number 
of stored clauses is bounded by $mn$.

During the experiments we checked also the maximal number {\it M\/} of stored
clauses. The results showed that {\it M\/} does almost not depend on {\it n},
such that $M \leq sm^t$, where $t \leq 1.3$ is not depending on $p_1$ and $p_2$, 
while {\it s\/} depends on $p_1$ and $p_2$. Table \ref{sfunc} displays
{\it s\/} as a function of $p_1$ and $p_2$. Figure \ref{aveM} in 
Appendix B shows average values of $M$ for $n=50, p_1=p_2=0.1,0.2,0.3$.
The maximum of $M$ in all our experiments was 1491 (for $n=50, m=200$).

\begin{table}[h]
\begin{center}
\begin{tabular}{|c|c||c|} \hline
$p_1$ & $p_2$ & {\it s} \\ \hline 
0.1 & 0.1 & 1.54 \\ 
0.1 & 0.2 & 0.82 \\ 
0.1 & 0.3 & 0.57 \\ 
0.2 & 0.2 & 0.74 \\ 
0.2 & 0.3 & 0.50 \\ 
0.3 & 0.3 & 0.46 \\ \hline
\end{tabular} 
\end{center}
\caption{{\it s\/} as a function of $p_1$ and $p_2$}
\label{sfunc}
\end{table}

The analysis of the running time of CDP follows the method developed by
\citeA{goldberg1} and by \citeA{goldberg2}. This method was used
also by \citeA{iwama}. The well known criticisms by \citeA{franco},
and by \citeA{mitchell} points out that the instances generated by this
method are mostly satisfiable,
and that is indeed the reason for the good performance of satisfiability
checking algorithms: the algorithms find rapidly one model of the formula.
This point does not apply when we seek not only just one model but all
the models.

Finally, it should be noted that the algorithms for counting models
developed so far are designed for {\em propositional\/} formulas. As 
it has been mentioned in the introduction, one application of counting 
models is in reasoning with incomplete information in logic systems usually 
expressed in {\em predicate calculus\/}. Therefore, developing counting 
algorithms for predicate calculus formulas is a next challenge of a great 
importance.


\acks{We are grateful to the anonymous referees for their most apt and
inspiring comments.
This research has been partly supported by the Israel Science
Foundation administrated by the Israel Academy of Sciences and Humanities.}


\newpage
\appendix

\setcounter{equation}{0}
\setcounter{lemma}{0}
\setcounter{theorem}{0}
\setcounter{section}{1}

\section*{Appendix A. Proofs}
\label{proofs}
\begin{theorem}
For $p = \frac{1}{3}$, $T(m,n) = O(m^2n).$
\end{theorem}
{\bf Proof.} For $p = \frac{1}{3}$, the recurrence inequality takes the form
\begin{equation}
T(m,n) \leq \left\{
\begin{array}{ll}
cmn +\\
(\frac{2}{3})^m  T(m,n-1) +\\
2\sum_{k=1}^m (_k^m) (\frac{1}{3})^k (\frac{2}{3})^{m-k} T(m-k,n-1) 
&  \ \ \ \ m,n \geq 1\\  
\\
1  & n=0 \ or \ m=0
\end{array} \right.
\label{tmn3}
\end{equation}
\citeA{goldberg1} showed, that for the following recurrence, 
$S(m,n) = O(m^2n)$.
\begin{equation}
S(m,n) = \left\{
\begin{array}{ll}
cmn +\\
2\sum_{k=1}^m (_k^m) (\frac{1}{3})^k (\frac{2}{3})^{m-k} S(m-k,n-1) 
&  \ \ \ \ m,n \geq 1\\  
\\
1  & n=0 \ or \ m=0
\end{array} \right.
\label{smn3}
\end{equation} 
The difference between (\ref{smn3}) and (\ref{tmn3}), the recurrence for
$S(m,n)$ and the recurrence for $T(m,n)$, is the extra term
$(\frac{2}{3})^m  T(m,n-1)$ in the latter. To compare $T(m,n)$ and
$S(m,n)$ we first need the following result.
\begin{lemma}
For all $m \geq 0$ and all $n \geq 0$, 
$S(m,n) \leq (\frac{3}{2})^{m-1} cmn$.
\label{sleq}
\end{lemma}
{\bf Proof.} \citeA{goldberg1} showed that $S(m,n) \leq cm^2n$.
Since $m<(\frac{3}{2})^{m-1}$ for $m \geq 5$, this proves the lemma for
all $m \geq 5$ and all $n \geq 0$. Direct computation of $S(m,n)$, due
to (\ref{smn3}), for $m=0,1,2,3,4$ completes the proof for all 
$m \geq 0$ and all $n \geq 0$.

\vspace{3mm}
Now $T(m,n)$ can be estimated as follows.
\begin{lemma}
For all {\it m\/} and all {\it n}, $T(m,n) \leq 3 \cdot S(m,n)$.
\end{lemma}
{\bf Proof.} By induction on {\it n\/}.\\
The assertion is true for $n \leq  1$.\\
Suppose it is true for every $i<n$, then 
\begin{eqnarray*}
T(m,n) & \leq & cmn + (\frac{2}{3})^m  T(m,n-1) 
+ 2\sum_{k=1}^m (_k^m) (\frac{1}{3})^k (\frac{2}{3})^{m-k} T(m-k,n-1)\\
& \leq  & cmn + 3 \cdot (\frac{2}{3})^m  S(m,n-1) +\\
& & 3 \cdot 2 \sum_{k=1}^m (_k^m) (\frac{1}{3})^k (\frac{2}{3})^{m-k} 
S(m-k,n-1).
\end{eqnarray*}
According to (\ref{smn3}),
$$
3S(m,n) = 3cmn + 3 \cdot 2 \sum_{k=1}^m (_k^m) (\frac{1}{3})^k 
(\frac{2}{3})^{m-k} S(m-k,n-1),
$$
so, $T(m,n) \leq 3S(m,n)+3(\frac{2}{3})^m S(m,n-1)-2cmn$.
For all $n>0$,  $S(m,n-1) \leq S(m,n)$, and by Lemma \ref{sleq},
for all {\it m\/} and all {\it n}, $3(\frac{2}{3})^m S(m,n) \leq 2cmn$.
This completes the proof.

Since $S(m,n) = O(m^2n)$ and $T(m,n) \leq 3 \cdot S(m,n)$, we get
for $p = \frac{1}{3}$, $T(m,n) = O(m^2n).$

\newpage
\begin{theorem}
$T(m,n)=O(m^dn)$, where
$d = \lceil \frac{-1}{\log_2(1-p)} \rceil$.
\end{theorem}
{\bf Proof.} We analyze the recurrence inequality for any {\it p}, using
considerations similar to those of \citeA{goldberg2}.\\
The recurrence inequality takes the form:
\begin{equation}
T(m,n) \leq \left\{
\begin{array}{ll}
cmn +\\
(1-p)^m  T(m,n-1) +\\
2\sum_{k=1}^m (_k^m) p^k (1-p)^{m-k} T(m-k,n-1) &  \ \ \ \ m,n \geq 1\\  
\\
1  & n=0 \ or \ m=0
\end{array} \right.
\end{equation}
It is easy to show, by induction on {\it n}, that $T(m,n)$ grows with 
{\it n}. Hence, 
\begin{equation}
T(m,n) \leq cmn + (1-p)^m  T(m,n) +
2\sum_{k=1}^m (_k^m) p^k (1-p)^{m-k} T(m-k,n).
\label{sndtmn}
\end{equation}
A solution of (\ref{sndtmn}) is linear in {\it n}, since this recurrence is linear
in the $T's$. Now for any value $m_0$ let us choose a constant {\it a\/} 
such that for all $m \leq m_0$
\begin{equation}
T(m,n) \leq am^dn,
\label{thirdtmn}
\end{equation}
where $d = \lceil \frac{-1}{\log_2(1-p)} \rceil$. Then for all $m \leq m_0$,
(\ref{sndtmn}), (\ref{thirdtmn}) imply
\begin{eqnarray*}
(1-(1-p)^m)T(m,n) & \leq & cmn + 2\sum_{k=1}^m (_k^m) p^k (1-p)^{m-k} 
                           T(m-k,n)\\
                  & \leq & cmn + 2\sum_{k=1}^m (_k^m) p^k (1-p)^{m-k} 
                           a(m-k)^dn\\
                  &  =   & cmn + am^dn \cdot 2\sum_{k=1}^m (_k^m) p^k 
                           (1-p)^{m-k} (1 - \frac{k}{m})^d.
\end{eqnarray*}
As \citeA{goldberg2} showed,
\begin{equation}
\sum_k (_k^m) p^k(1-p)^{m-k} (1 - \frac{k}{m})^d = (1-p)^d + O(m^{-1}),
\label{sigma}
\end{equation}
and therefore,
$$
(1-(1-p)^m)T(m,n) \leq cmn + 2am^dn(1-p)^d + an \cdot O(m^{d-1}).
$$
$cmn = O(mn)$, and so,
$$
T(m,n) \leq \frac{2am^dn(1-p)^d}{1-(1-p)^m} + an \cdot O(m^{max(1,d-1)}).
$$
We are going now to find out conditions under which
$$
\frac{2am^dn(1-p)^d}{1-(1-p)^m} + an \cdot O(m^{max(1,d-1)}) \leq am^dn,
$$
that is
\begin{equation}
O(m^{max(1,d-1)}) \leq m^d [1 - \frac{2(1-p)^d}{1-(1-p)^m}].
\label{bigo}
\end{equation}
First, let {\it g\/} denote the subexpression of (\ref{bigo}) in square brackets. 
For all {\it d}, {\it g\/} is less than 1, hence, {\it d\/} must be greater 
than 1 to satisfy $O(m^{max(1,d-1)}) \leq m^d$. So,
\begin{equation}
d > 1
\label{dvalue}
\end{equation}
Second, for $0<p<1$, $(1-p)^m$ diminishes monotonically, and tends to 0 as 
$m \rightarrow \infty$, hence to make 
{\it g\/} positive, we need
\begin{equation}
d> \frac{-1}{\log_2(1-p)}
\label{snddvalue}
\end{equation}
Thus, choosing {\it m\/} (and hence, $m_0$) sufficiently large 
(depending on the value of the $O(m^{-1})$ expression in (\ref{sigma})), and
determining the values of {\it a\/} and {\it d\/} satisfying conditions
(\ref{thirdtmn}), (\ref{dvalue}), (\ref{snddvalue}), establishes 
$T(m,n)=O(m^dn)$, where
$d = \lceil \frac{-1}{\log_2(1-p)} \rceil$.

\newpage

\setcounter{equation}{0}
\setcounter{lemma}{0}
\setcounter{theorem}{0}
\setcounter{table}{0}
\setcounter{figure}{0}

\section*{Appendix B. More Experimental Data}
\label{tables}
\begin{table}[ht]
\begin{center}
\begin{tabular}{|c||r|r|r|} \hline
Number of clauses & 40 variables & 50 variables & 60 variables 
\\ \hline 
10    &       16  &        15  &        13  \\ 
20    &      234  &       191  &       153  \\ 
30    &     1600  &      1203  &       868  \\ 
40    &     6294  &      5076  &      3699  \\ 
50    &    19856  &     16384  &     11370  \\
60    &    46645  &     53296  &     28467  \\ 
70    &   101607  &    109327  &     75472  \\
80    &   186199  &    244248  &    153384  \\ 
90    &   299220  &    426169  &    311668  \\
100   &   507888  &    807669  &    635712  \\
120   &  1093383  &   2222499  &   1687147  \\ 
140   &  1945874  &   5507340  &   4289713  \\
160   &  3095848  &  11824325  &  10812931  \\
180   &  4441760  &  22444086  &  20230352  \\  
200   &  6377501  &  39119045  &  37381207  \\ \hline
\end{tabular}
\end{center}
\caption{Average number of recursive calls for $p_1 = p_2 = 0.1$}
\end{table}

\begin{table}[ht]
\begin{center}
\begin{tabular}{|c||r|r|r|} \hline
Number of clauses & 20 variables & 30 variables & 40 variables 
\\ \hline 
10    &     8  &      7  &      7  \\ 
20    &    41  &     34  &     29  \\ 
30    &   110  &     88  &     76  \\ 
40    &   234  &    185  &    150  \\ 
50    &   433  &    332  &    266  \\
60    &   648  &    545  &    424  \\ 
70    &   973  &    835  &    636  \\
80    &  1302  &   1240  &    919  \\ 
90    &  1683  &   1731  &   1225  \\ 
100   &  2089  &   2349  &   1647  \\
120   &  3128  &   3947  &   2791  \\ 
140   &  3934  &   6461  &   4339  \\
160   &  5209  &   9821  &   6446  \\
180   &  6051  &  13661  &   9002  \\  
200   &  6513  &  18696  &  12193  \\ \hline
\end{tabular}
\end{center}
\caption{Average number of recursive calls for $p_1 = p_2 = 0.2$}
\end{table}

\begin{table}[ht]
\begin{center}
\begin{tabular}{|c||r|r|} \hline
Number of clauses & 20 variables & 30 variables  
\\ \hline 
10    &    5  &    5  \\ 
20    &   17  &   15  \\ 
30    &   32  &   29  \\ 
40    &   52  &   45  \\ 
50    &   78  &   65  \\
60    &  104  &   89  \\ 
70    &  134  &  114  \\
80    &  176  &  146  \\ 
90    &  218  &  178  \\ 
100   &  265  &  215  \\
120   &  363  &  295  \\ 
140   &  495  &  384  \\
160   &  623  &  489  \\
180   &  807  &  607  \\  
200   &  966  &  724  \\ \hline
\end{tabular}
\end{center}
\caption{Average number of recursive calls for $p_1 = p_2 = 0.3$}
\end{table}

\begin{table}[ht]
\begin{center}
\begin{tabular}{|c||r|r|r|} \hline
Number of clauses & 30 variables & 40 variables & 50 variables 
\\ \hline 
10    &       11  &        10  &         9  \\ 
20    &       89  &        75  &        60  \\ 
30    &      343  &       290  &       211  \\ 
40    &     1025  &       752  &       572  \\ 
50    &     2179  &      1709  &      1252  \\
60    &     4195  &      3438  &      2473  \\ 
70    &     7309  &      6250  &      4311  \\
80    &    11740  &     10919  &      7622  \\ 
90    &    19224  &     17619  &     10999  \\
100   &    25866  &     27847  &     16734  \\
120   &    44729  &     57548  &     37051  \\ 
140   &    74280  &    109469  &     68354  \\
160   &   109134  &    185568  &    117175  \\
180   &   144698  &    304983  &    201822  \\  
200   &   182516  &    463503  &    307851  \\ \hline
\end{tabular}
\end{center}
\caption{Average number of recursive calls for $p_1 = 0.1$, $p_2 = 0.2$}
\end{table}

\begin{table}[ht]
\begin{center}
\begin{tabular}{|c||r|r|r|} \hline
Number of clauses & 30 variables & 40 variables & 50 variables 
\\ \hline 
10    &        9  &         9  &         8  \\ 
20    &       51  &        41  &        36  \\ 
30    &      141  &       114  &        97  \\ 
40    &      333  &       239  &       206  \\ 
50    &      635  &       440  &       361  \\
60    &     1048  &       782  &       596  \\ 
70    &     1638  &      1117  &       903  \\
80    &     2603  &      1706  &      1317  \\ 
90    &     3801  &      2493  &      1915  \\
100   &     4813  &      3523  &      2568  \\
120   &     8591  &      6087  &      4401  \\ 
140   &    14043  &     10221  &      7254  \\
160   &    21237  &     15087  &     10731  \\
180   &    29782  &     22832  &     15271  \\  
200   &    40550  &     31882  &     20760  \\ \hline
\end{tabular}
\end{center}
\caption{Average number of recursive calls for $p_1 = 0.1$, $p_2 = 0.3$}
\end{table}

\begin{table}[ht]
\begin{center}
\begin{tabular}{|c||r|r|} \hline
Number of clauses & 20 variables & 30 variables  
\\ \hline 
10    &        6  &         6  \\ 
20    &       24  &        21  \\ 
30    &       56  &        45  \\ 
40    &      101  &        80  \\ 
50    &      164  &       124  \\
60    &      234  &       189  \\ 
70    &      337  &       255  \\
80    &      456  &       352  \\ 
90    &      606  &       447  \\
100   &      762  &       567  \\
120   &     1183  &       851  \\ 
140   &     1608  &      1225  \\
160   &     2184  &      1621  \\
180   &     2887  &      2159  \\  
200   &     3533  &      2743  \\ \hline
\end{tabular}
\end{center}
\caption{Average number of recursive calls for $p_1 = 0.2$, $p_2 = 0.3$}
\end{table}

\begin{table}[ht]
\begin{center}
\begin{tabular}{|c|c|c||r|r|} \hline
Probabilities & Variables & Clauses & Average & Standard deviation 
\\ \hline  
$p_1 = p_2 = 0.1$        &  40  &    120  &   1093383  &    412246   \\ 
                         &      &    200  &   6377501  &   2921029   \\ 
                         &  50  &    120  &   2222499  &   1141909   \\ 
                         &      &    200  &  39119045  &  14587096   \\ 
$p_1 = p_2 = 0.2$        &  30  &    120  &      3947  &       906   \\                   
                         &      &    200  &     18696  &      3387   \\ 
                         &  40  &    120  &      2791  &       473   \\
                         &      &    200  &     12193  &      2097   \\ 
$p_1 = p_2 = 0.3$        &  20  &    120  &       363  &        43   \\
                         &      &    200  &       966  &       106   \\
                         &  30  &    120  &       295  &        25   \\ 
                         &      &    200  &       724  &        63   \\
$p_1 = 0.1$, $p_2 = 0.2$ &  40  &    120  &     57548  &     21946   \\ 
                         &      &    200  &    463503  &    135171   \\ 
                         &  50  &    120  &     37051  &     11081   \\ 
                         &      &    200  &    307851  &     90897   \\ 
$p_1 = 0.1$, $p_2 = 0.3$ &  30  &    120  &      8591  &      2244   \\                   
                         &      &    200  &     40550  &      7003   \\ 
                         &  40  &    120  &      6087  &      1349   \\
                         &      &    200  &     31882  &      6264   \\ 
$p_1 = 0.2$, $p_2 = 0.3$ &  20  &    120  &      1183  &       183   \\
                         &      &    200  &      3533  &       514   \\
                         &  30  &    120  &       851  &       126   \\ 
                         &      &    200  &      2743  &       392   \\ \hline
\end{tabular}
\end{center}
\caption{Samples of standard deviation of number of recursive calls}
\label{stdev}
\end{table}

\begin{table}[ht]
\begin{center}
\begin{tabular}{|c||r|r|r|} \hline
Clauses-to-variables ratio & 20 variables & 40 variables & 50 variables 
\\ \hline 
0.2         &   59 &   1056 &    32062  \\ 
0.4         &  272 &  17715 &  2500987  \\ 
0.6         &  625 & 113185 & 11634670  \\ 
0.8         &  993 & 252044 & 31376686  \\ 
{\bf 1.0}   & 1301 & 502669 & 34843025  \\
1.2         & 1521 & 538579 & 59443580  \\ 
1.4         & 1445 & 529520 & 48805440  \\
1.6         & 1328 & 412563 & 26416134  \\ 
1.8         & 1283 & 307939 & 29494057  \\ 
{\bf 2.0}   & 1050 & 194754 & 11792351  \\
2.2         &  789 & 105089 &  8277529  \\ 
2.4         &  664 &  60548 &  4037986  \\
2.6         &  558 &  34057 &  2208147  \\
2.8         &  387 &  18875 &   923228  \\  
{\bf 3.0}   &  341 &   9574 &   633407  \\
{\bf 4.0}   &  135 &    816 &    21339  \\
{\bf 5.0}   &   86 &    335 &     1443  \\
{\bf 6.0}   &   65 &    225 &      862  \\
{\bf 7.0}   &   55 &    160 &      558  \\
{\bf 8.0}   &   48 &    138 &      476  \\ \hline
\end{tabular} 
\end{center}
\caption{Median number of recursive calls for 3-literal clauses,
$n = 20,40,50$}
\label{threetable}
\end{table}

\begin{figure}[ht]
\begin{center}
\epsfxsize=300pt \epsfbox{fig4.eps}
\end{center}
\caption{Average of maximal number of clauses stored during the running of
CDP for 50 variables.}
\label{aveM}
\end{figure}

\clearpage

\bibliography{jair}
\bibliographystyle{theapa}


\end{document}



