1106.0218v1

Journal of Arti/cial Intelligence Research /1/0 /(/1/9/9/9/) /4/5/7/-/4/7/7 Submitted /1/1///9/8/; published /6///9/9 ## Research Note The Good Old Davis/-Putnam Procedure Helps Elazar Birnbaum Eliezer L/. Lozinskii /9/1/9/0/4 Jerusalem/, Israel Institute of Computer Science The Hebrew University 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/(m d n/)/, where d /= d /BnZr/1 log /2 /(/1/BnZrp/) e/. The practical performance of CDP has been estimated in a series of experiments on a wide variety of CNF formulas/. /1/. Introduction Given a propositional formula F in CNF or DNF/, one may want to know what is the number //(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/, /1/9/9/6/)/. 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 su/cient statistics this probability can be estimated by j//(KB /[fsg/)j /= j//(KB/)j/. /(b/) Inference in Bayesian belief networks/. As Roth /(/1/9/9/6/) 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 /; /: /: /: /;xn may be regarded as a constraint satisfaction problem in which the domain of each variable is f/0/; /1g/, and each clause C is a relation R / f/0/; /1g 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 //(F/)/. /(d/) Estimating the utility of reasoning with approximate theory AT instead of the original theory T /. This utility depends on the size of j//(AT /)j /BnZr j//(T /)j /(Roth/, /1/9/9/6/)/. Another important application is to reasoning with incomplete information /(Grove et al/./, /1/9/9/4/; Lozinskii/, /1/9/8/9/, /1/9/9/5/)/. Indeed/, if F describes a real world W faithfully/, then given a formula / such that neither / nor /:/ is a logical consequence of F/, a reasonable assumption c assert //, the more likely is that / is true in W/. / /1/9/9/9 AI Access Foundation and Morgan Kaufmann Publishers/. All rights reserved/. elazar/@cs/.huji/.ac/.il lozinski/@cs/.huji/.ac/.il Counting Models Birnbaum /& Lozinskii The problem of counting models is /#P/-complete in general /(Valiant/, /1/9/7/9/)/, and so/, according to the present state of the art in the /eld/, computationally intractable in the worst case/. Dubois /(/1/9/9/1/) introduced an algorithm that for any formula F of n variables and m clauses/, each clause containing r literals/, counts models of F in time O/(m/ n r /)/, / r being the positive root of the polynomial y r /BnZr y r/BnZr/1 /BnZr /
/
/
/BnZr /1 /(/ /2 / /1/:/6/2/; / /3 / /1/:/8/4/; / /4 / /1/:/9/3/; /: /: /: and limr/!/1 / r /= /2/)/. Recently/, Zhang /(/1/9/9/6/) 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 complexity/. Regarding the /rst alternative/, Luby and Veli/ ckovi/ c /(/1/9/9/1/) presented a deterministic algorithm for approximating the proportion of truth assignments that satisfy a DNF formula F/. Let Pr/[F/] denote this proportion /(P r/[F /] /= //(F /)/=/2 n where n is the number of variables of F/)/. Given small numbers //; / /> /0/, the algorithm computes an estimate Y of Pr/[F /] which truth values to the variables of a formula F in time O/(m/2 n /)/. To satisfy practical applications/, one has either to resort to a good approximation of //(F /)/, or use an algorithm for computing //(F/) exactly with a reasonable average time satis/es time of the algorithm is estimated by a polynomial in n and m multiplied by /(/1 /BnZr //)P r/[F /] /BnZr / / Y / P r/[F /] /+ //: Let m and n be the number of clauses and variables of F/, respectively/. The running n O/( /1 / /(log /2 m/+log /2 /1 / /)/(log log m/+log /1 / /+log /1 / /)/) /: <!-- formula-not-decoded --> So/, the running time of the algorithm grows fast with the precision required/. Linial and Nisan /(/1/9/9/0/) studied the problem of computing the size of a union of a given /+/(/BnZr/1/) m/+/1 jS /1 /\ /
/
/
/\ S m j/: /(/1/) 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 k sets/. If k / / /( p m/)/, then the union size can be precision/, k approaches m/. For instance/, for m /= /1/0/0 and an error of /1/0 /BnZr/3 /, k / /3/4/: Iwama /(/1/9/8/9/) introduced an algorithm for testing satis/ability of a CNF formula F over n variables by counting the truth assignments falsifying 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 F is computed with the aid of the approximated with a relative error of O/(e /BnZr/2k/= p m /)/. As Linial and Nisan /(/1/9/9/0/) pointed out/, this result can be applied to approximating the number of models of a DNF formula F /| each clause of F has its set of models/, and //(F /) is equal to the size of the union of all those sets/. Thus/, only the /rst k terms of the formula /(/1/) are needed for a good approximation/, where p m / k / m/. However/, for a high observation that this set is the union of the sets of truth assignments falsifying each clause /4/5/8 Davis/-Putnam Procedure Helps Counting Models of 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 / ln m /BnZr p /2 n/, 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 variables is O/(m c n/)/, where c /= O/(log m/)/. In the sequel we present an algorithm which we call CDP /(Counting by Davis/-Putnam/) for computing //(F/) precisely/. Algorithm CDP is based on the Davis/-Putnam procedure /(DPP/) /(Davis /& Putnam/, /1/9/6/0/) for solving the satis/ability problem /(SAT/)/. We study features of DPP/, and show how its rules can be modi/ed/, resulting in an algorithm for counting models/. An analysis shows that for a formula F with m clauses on n variables/, the average running time of CDP is O/(m d n/)/, where d /= d /BnZr/1 log /2 /(/1/BnZrp/) e/, and p is the probability O/(m c/+/1 /)/. Lozinskii /(/1/9/9/2/) employed an algorithm which is similar to that presented by Iwama /(/1/9/8/9/)/, for counting models/. He showed that under reasonable assumptions/, the average running time of computing the exact number of models of a formula with m clauses on n that any literal occurs in a given clause/. Section /5 describes numerous experiments with CDP showing that its actual average time complexity is signi/cantly lower than the upper bounds provided by mathematical analysis in Section /3 and in previous works /(Dubois/, /1/9/9/1/; Iwama/, /1/9/8/9/; Lozinskii/, /1/9/9/2/; Zhang/, /1/9/9/6/)/. 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 satis/ability of such formulas by ## DPP presented by Mitchell et al/. /(/1/9/9/2/)/. /2/. Algorithm for Counting Models In the sequel we consider propositional formulas over a set V /= fx /1 /; /: /: /: /; x n g of variables/, l /2/./1 The Davis/-Putnam Procedure The Davis/-Putnam procedure /(DPP/) /(Davis /& Putnam/, /1/9/6/0/) is intended for deciding satis/ability of a propositional CNF formula F /(regarded as a set of clauses/)/, and can be ## denotes a literal /(l /2 fx /1 /; /: /: /: /; x n /; / x/1 /; /: /: /: /; / xng/)/, and / l stands for the negation of l/. presented as a recursive boolean function /(assuming that no clause of F ``` ``` return DPP/(F/1 /)/; /(/* F is satis/able i/ F /1 is a tautology/)/: - /*/) then - if there exists a pure literal l in F /(/* such that / l does not appear in F F/1 /= fC j C /2 F/; l /6/2 Cg/; /(/* delete from F all clauses containing l /*/) /4/5/9 is so /*/) Birnbaum /& Lozinskii ``` ``` the pure literal rule/. If F contains a unit clause flg/, and the splitting rule chooses l/, then F/2 contains an empty clause /(the unit clause without its only literal/)/, and so/, is unsatis/able/. So/, F is satis/able i/ F/1 is so/. This is the unit clause rule/. /(Incidentally/, the splitting rule treats well tautological clauses too/. If a clause C of F contains a literal l and its complement / l/, return /(DPP/(F /1 /) /\_ DPP/(F /2 /)/)/. /(/* F is satis/able i/ /(F /1 /\_ F /2 /) is so /*/) 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 l in F/, and the splitting rule chooses l /, then F/1 / F /2 /, and hence /(F /1 /\_ F /2 /) is satis/able i/ F /1 is so/. According to the splitting rule/, F is satis/able i/ /(F /1 /\_ F /2 /) is so/, and hence/, F is satis/able i/ F /1 is so/. This is exactly and the splitting rule is applied to l/, then 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 e/ciently/. Indeed/, if F contains a unit clause flg or a pure literal l/, then applying the splitting rule to l yields only one formula/, but choosing ## We address this issue in the sequel/. a non/-pure and non/-unit/-clause literal leaves two formulas for further processing/. If 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/. /2/./2 Counting Models Thinking of counting models of a propositional formula F/, we notice that by choosing a variable x/, the splitting rule actually splits the set of models of F into two disjoint subsets/: one in which x is true /(namely/, the models of F /1 /)/, and the other /(models of F /2 /) in which x is false/. The chosen variable x appears neither in F /1 nor in F /2 /, and there may be other variables that appear in 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 x /(or / x/, respectively/)/. Hence/, every model of F/1 /(F /2 /) can be completed to a model of F by assigning true /(false/, respectively/) to x/, and true or false arbitrarily to every variable of F that does not appear in F /1 /(F /2 /, respectively/)/. Let //(F /) stand for the number of models of F/, and n /1 /(n /2 /) denote the number of variables satis/ability/, the pure literal rule turns out to be ine/cient for counting models/. /(other than x/) which occur in F but not in F /1 /(F /2 /)/, then //(F /) /= /2 n/1 //(F /1 /) /+ /2 n/2 //(F /2 /)/. As it has been shown in Section /2/./1/, if checking satis/ability 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 F/. So/, in contrast to checking /4/6/0 Davis/-Putnam Procedure Helps Counting Models Based on these observations/, the following function CDP counts models of a formula F return CDP/(F/1 /; n /BnZr /1/) /+ CDP/(F/2 /; n /BnZr /1/)/. Any iteration of CDP deletes the chosen variable/, and so/, reduces the number of variables ``` ``` ## of F by at least one/. This guarantees that CDP terminates /(either on step /1 or on step /2/)/. /3/. Average Running Time In the analysis of the average running time of the function CDP we follow Goldberg /(/1/9/7/9/) /3/./1 The Recurrence Equation Let m and n denote the number of clauses and variables of F/, respectively/. Assume that all the literals have the same probability p to appear in each clause C of F/. /(To simplify the analysis we allow F to contain duplicate clauses and tautologies/./) Assume also that there is no dependency among the occurrences of di/erent variables and among the occurrences of the same variable in di/erent clauses/. For a given distribution of p/, let T /(m/; n/) denote and Goldberg et al/. /(/1/9/8/2/)/, who studied the average running time of DPP/. the average running time of CDP/(F/; n/) with F containing m clauses/. If F contains m clauses on n variables/, then mn bounds the size of F/. Each step of cmn bounds the time of executing one iteration of function CDP/. 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 a/ect Lemma /1/. We also assume function CDP can be accomplished during at most two passes over F/. Lemma /1 If F contains m clauses on n variables/, then there is a constant c such that that the literal for the splitting rule is chosen randomly/. Let l be the literal that has been chosen for the splitting rule/. Since the probability that l occurs in a clause is p/, the probability that k out of m clauses contain l is /( m /)p k /(/1 /BnZr p/) m/BnZrk /. /4/6/1 k Birnbaum /& Lozinskii The same holds for / l/. The number of clauses of formulas F /1 /, F /2 produced by splitting F is equal to the number of all clauses of F minus the number of clauses of F which contain the probability /( m k /)p k /(/1 /BnZr p/) m/BnZrk /. Since each of F /1 /, F /2 contains at most n/BnZr/1 variables/, the following recurrence inequality literal l/, / l/, respectively/. Lemma /2 Each of formulas F/1/, F/2 produced by splitting F contains m /BnZr k clauses with <!-- formula-not-decoded --> at /0/. The right/-hand side of /(/2/) overestimates T /(m/; n/) since/, /rst/, the number of variables of F/1 /, F/2 is at most n /BnZr /1/, and/, second/, function CDP may stop when F contains an empty /: /1 n /= /0 or m /= /0 The /rst 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 l appears in F/, it is impossible that the number of clauses in which l occurs is /0/, and so/, the summation of the second term starts at /1/. The literal / l may not appear at all in F /(if l is pure/)/. Consequently/, the summation of the third term begins clause/, even before m or n becomes /0/. To estimate T/(m/; n/)/, we show/, /rst/, that for p /= /1/=/3/, T /(m/; n/) /= O/(m /2 n/)/, and/, second/, that for any p/, T /(m/; n/) /= O/(m d n/) where d /= d /BnZr/1 log /2 /(/1/BnZrp/) e/: <!-- formula-not-decoded --> ## Proof is given in Appendix A/. /3/./2 The Average Running Time for p /= /1/=/3 Following Goldberg /(/1/9/7/9/)/, 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 /: /1 T/(m/; n/) /= O/(m /2 n /= /0 or m /= /0 Theorem /1 For p /= /1 /3 /, n/)/: /3/./3 The Average Running Time for Any p The assumption of p /= /1/=/3 is commonly adopted in probabilistic analysis of algorithms handling CNF or DNF formulas /(Franco /& Paull/, /1/9/8/3/; /4/6/2 Goldberg/, /1/9/7/9/; Goldberg et al/./, Davis/-Putnam Procedure Helps Counting Models /1/9/8/2/)/, 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 p of a literal occurrence formulas which contain an empty clause/. If an internal node represents a formula with k clauses/, the expected number of clauses in each of its children is k/(/1/BnZrp/)/. The expected height of the tree h is therefore about log b m where b /= /1 /1/BnZrp /. The number of nodes in a complete binary tree of height h is about /2 /
/2 h /, and this is the expected number / of iterations of the function CDP/. So/, / /= /2 /
/2 h /= /2m d /, where d /= /BnZr/1 log /2 /(/1/BnZrp/) /. The running time of each iteration is O/( /~ m/~ n/) where /~ m is the number in a clause of 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 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 of clauses and /~ n is the number of variables of the formula that is treated at that iteration/. Theorem /2 T/(m/; n/) /= O/(m d n/)/, where d /= d /BnZr/1 log /2 /(/1/BnZrp/) e/. 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 /2 holds for p being the lowest occurrence probability among all literals of F/. Second/, if 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 n/. /4/. Re/ning the CDP /4/./1 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 ## This section describes some re/nements to CDP improving its performance/. and F/2 to be as small as possible/. The size of these formulas is determined by both m and n/. As minimizing the number of variables in F /1 /, F /2 causes an unjusti/ed 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 F/)/, or by minimizing max/(m /1 /; m /2 /)/. The latter can be achieved by maximizing over x the quantity min/(pos/(x/)/; neg/(x/)/)/, where pos/(x/) /(neg/(x/)/) denotes the number of clauses of F in which x occurs unnegated /(negated/, respectively/)/. These two approaches may be combined/. Indeed/, experiments reported in Section /5 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 /)/. /4/6/3 ## small computation overhead/. Birnbaum /& Lozinskii As has been suggested by an anonymous reviewer/, by using proper data structures/, the computation of pos/(x/) and neg/(x/) for all variables x can be done e/ciently/, causing only a /4/./2 Handling Small Formulas The function CDP stops when F contains an empty clause or when F is empty/. What if F consists of only one clause containing k literals/? The splitting rule will be applied to 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 F/. So/, splitting of the single clause of F will be being processed is reduced under /6/, CDP runs the algorithm of Lozinskii /(/1/9/9/2/)/. repeated k times/. A similar process of ine/cient splitting takes place also on formulas consisting of rela/tively few clauses/. It turns out that the algorithm presented by Lozinskii /(/1/9/9/2/) is more e/cient for handling small sets of clauses/. Experiments on randomly chosen formulas showed that for formulas with less than /6 clauses the algorithm of Lozinskii /(/1/9/9/2/) performs better than function CDP in its original form/. Therefore/, when the number of clauses of a formula /5/. Experiments Algorithm CDP presented in the previous sections has been programmed in Turbo/-Pascal/, and run on PC/, with the purpose of determining an e/cient way of choosing a variable for the splitting rule/, /nding an appropriate number of clauses in a formula for switching the function CDP to the algorithm of Lozinskii /(/1/9/9/2/)/, and assessing the actual running time 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 / m/, such that for m / / m the hard cases lie around a corresponding number of variables/. For instance/, the hard cases for p /1 /= p /2 /= /0/:/1 and / m /= /6/0 are located around n /= /5/0/. Figures /1 and /2 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 /7 in Appendix B/)/. All the experiments ran on a pentium based PC /(/2/6/6 MHz/)/. The actual running time of CDP/. In the experiments/, CDP has been applied to randomly produced sets of clauses with the following parameters/: /1/0 / m / /2/0/0/, /1/0 / n / /8/0 and p/1 /; p /2 /2 f/0/:/1/; /0/:/2/; /0/:/3g/, 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/, /1/0/0 random instances of F have been processed/. Performance of CDP has been measured by of CDP ranged from less than one second to /5 hours/. Following the discovery of hard cases for SAT /(Mitchell et al/./, /1/9/9/2/)/, 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/, /2/0/0 instances were considered/. Figure /3 gives the median number of recursive calls performed by CDP for a sample of n /= /2/0/; /4/0/; /5/0/. /4/6/4 More data in Table /8 Figure /1/: Davis/-Putnam Procedure Helps Counting Models <details> <summary>Image 1 Details</summary>  ### Visual Description ## Chart: Logarithmic Plot of Number of Calls vs. Number of Clauses ### Overview The image is a line chart that plots the base-2 logarithm of the number of calls against the number of clauses in a formula. There are three data series, each representing a different number of variables (50, 30, and 20) with corresponding probabilities p1 and p2. The x-axis represents the number of clauses in the formula, ranging from 0 to 200. The y-axis represents the log base 2 of the number of calls, ranging from 0 to 26. ### Components/Axes * **X-axis:** "Number of clauses in the formula" with tick marks at intervals of 20, ranging from 0 to 200. * **Y-axis:** "log2 of number of calls" with tick marks at intervals of 2, ranging from 0 to 26. * **Legend (bottom-right):** * Line with diamond markers: "50 variables, p1=p2=0.1" * Line with circle markers: "30 variables, p1=p2=0.2" * Line with triangle markers: "20 variables, p1=p2=0.3" ### Detailed Analysis * **50 variables, p1=p2=0.1 (Line with diamond markers):** * Trend: The line slopes upward, with a decreasing rate of increase as the number of clauses increases. * Data Points: * At 0 clauses, log2(calls) ≈ 0 * At 20 clauses, log2(calls) ≈ 7 * At 40 clauses, log2(calls) ≈ 11 * At 60 clauses, log2(calls) ≈ 14 * At 80 clauses, log2(calls) ≈ 16 * At 100 clauses, log2(calls) ≈ 17.5 * At 120 clauses, log2(calls) ≈ 19 * At 140 clauses, log2(calls) ≈ 20 * At 160 clauses, log2(calls) ≈ 21 * At 180 clauses, log2(calls) ≈ 22 * At 200 clauses, log2(calls) ≈ 23 * **30 variables, p1=p2=0.2 (Line with circle markers):** * Trend: The line slopes upward, with a decreasing rate of increase as the number of clauses increases. * Data Points: * At 0 clauses, log2(calls) ≈ 0 * At 20 clauses, log2(calls) ≈ 5 * At 40 clauses, log2(calls) ≈ 7.5 * At 60 clauses, log2(calls) ≈ 9 * At 80 clauses, log2(calls) ≈ 10 * At 100 clauses, log2(calls) ≈ 11 * At 120 clauses, log2(calls) ≈ 11.7 * At 140 clauses, log2(calls) ≈ 12.3 * At 160 clauses, log2(calls) ≈ 12.8 * At 180 clauses, log2(calls) ≈ 13.3 * At 200 clauses, log2(calls) ≈ 14 * **20 variables, p1=p2=0.3 (Line with triangle markers):** * Trend: The line slopes upward, with a decreasing rate of increase as the number of clauses increases. * Data Points: * At 0 clauses, log2(calls) ≈ 0 * At 20 clauses, log2(calls) ≈ 3 * At 40 clauses, log2(calls) ≈ 5 * At 60 clauses, log2(calls) ≈ 6 * At 80 clauses, log2(calls) ≈ 6.8 * At 100 clauses, log2(calls) ≈ 7.3 * At 120 clauses, log2(calls) ≈ 7.7 * At 140 clauses, log2(calls) ≈ 8 * At 160 clauses, log2(calls) ≈ 8.3 * At 180 clauses, log2(calls) ≈ 8.6 * At 200 clauses, log2(calls) ≈ 9 ### Key Observations * For a fixed number of clauses, the log2 of the number of calls increases as the number of variables increases (and p1=p2 decreases). * The rate of increase of log2(calls) decreases as the number of clauses increases for all three data series. * The line representing 50 variables has the highest values for log2(calls) across the entire range of clauses. * The line representing 20 variables has the lowest values for log2(calls) across the entire range of clauses. ### Interpretation The chart illustrates the relationship between the number of clauses in a formula and the number of calls required, under different conditions defined by the number of variables and probabilities p1 and p2. The logarithmic scale on the y-axis suggests that the actual number of calls grows exponentially with the number of clauses. The data indicates that increasing the number of variables (while decreasing the probabilities p1 and p2) leads to a higher number of calls for a given number of clauses. This could be interpreted as an increase in the complexity of the problem, requiring more calls to solve. The diminishing rate of increase in log2(calls) as the number of clauses increases suggests that the marginal cost of adding more clauses decreases, possibly due to some form of optimization or saturation effect. </details> Average number of recursive calls for di/erent values of p/1/; p/2 <details> <summary>Image 2 Details</summary>  ### Visual Description ## Chart: Logarithmic Growth of Calls vs. Clauses ### Overview The image is a line chart that depicts the relationship between the number of clauses in a formula and the base-2 logarithm of the number of calls, for different numbers of variables and probabilities p1 and p2. The chart shows three distinct lines, each representing a different configuration of variables and probabilities. ### Components/Axes * **X-axis:** "Number of clauses in the formula". The scale ranges from 0 to 200, with tick marks every 20 units. * **Y-axis:** "log2 of number of calls". The scale ranges from 0 to 20, with tick marks every 2 units. * **Legend (bottom-right):** * Line with diamonds: "40 variables, p1=0.1 p2=0.2" * Line with circles: "30 variables, p1=0.1 p2=0.3" * Line with triangles: "20 variables, p1=0.2 p2=0.3" ### Detailed Analysis * **40 variables, p1=0.1 p2=0.2 (Diamonds):** * The line starts at approximately (0, 0). * At 20 clauses, the log2 of calls is approximately 6. * At 60 clauses, the log2 of calls is approximately 11. * At 100 clauses, the log2 of calls is approximately 13. * At 140 clauses, the log2 of calls is approximately 15. * At 180 clauses, the log2 of calls is approximately 16. * At 200 clauses, the log2 of calls is approximately 16.5. * Trend: The line slopes upward, with the slope decreasing as the number of clauses increases. * **30 variables, p1=0.1 p2=0.3 (Circles):** * The line starts at approximately (0, 0). * At 20 clauses, the log2 of calls is approximately 5. * At 60 clauses, the log2 of calls is approximately 9. * At 100 clauses, the log2 of calls is approximately 11. * At 140 clauses, the log2 of calls is approximately 12. * At 180 clauses, the log2 of calls is approximately 13. * At 200 clauses, the log2 of calls is approximately 13.5. * Trend: The line slopes upward, with the slope decreasing as the number of clauses increases. * **20 variables, p1=0.2 p2=0.3 (Triangles):** * The line starts at approximately (0, 0). * At 20 clauses, the log2 of calls is approximately 4. * At 60 clauses, the log2 of calls is approximately 7. * At 100 clauses, the log2 of calls is approximately 8.5. * At 140 clauses, the log2 of calls is approximately 9.5. * At 180 clauses, the log2 of calls is approximately 10.5. * At 200 clauses, the log2 of calls is approximately 11.5. * Trend: The line slopes upward, with the slope decreasing as the number of clauses increases. ### Key Observations * All three lines start at the origin (0,0). * The line representing "40 variables, p1=0.1 p2=0.2" consistently has the highest log2 of calls for any given number of clauses. * The line representing "20 variables, p1=0.2 p2=0.3" consistently has the lowest log2 of calls for any given number of clauses. * All three lines show a decreasing rate of increase as the number of clauses increases, suggesting a logarithmic relationship. ### Interpretation The chart illustrates how the number of variables and the probabilities p1 and p2 affect the number of calls (on a log2 scale) as the number of clauses in a formula increases. The data suggests that increasing the number of variables while keeping p1 and p2 relatively low (40 variables, p1=0.1, p2=0.2) results in a higher number of calls compared to scenarios with fewer variables or different probability combinations. The logarithmic trend indicates that the impact of adding more clauses diminishes as the number of clauses grows larger. The probabilities p1 and p2 seem to have an inverse relationship with the number of variables. </details> Average number of recursive calls for di/erent values of p/1/; p/2 /(continued/) Figure /2/: of Appendix B/. /(Median number is shown to enable comparison with the results presented /4/6/5 by Mitchell et al/./, /1/9/9/2/)/. Figure /3/: Birnbaum /& Lozinskii <details> <summary>Image 3 Details</summary>  ### Visual Description ## Chart: Logarithmic Plot of Calls vs. Clause-to-Variable Ratio ### Overview The image is a line chart comparing the logarithmic number of calls (base 2) against the clauses-to-variables ratio for formulas with 20, 40, and 50 variables. The chart illustrates how the number of calls changes as the ratio of clauses to variables increases for each formula type. ### Components/Axes * **Y-axis:** "log2 of number of calls". The scale ranges from 0 to 24, with tick marks at every increment of 2. * **X-axis:** "clauses-to-variables ratio". The scale ranges from 0 to 8, with tick marks at every increment of 1. * **Legend:** Located in the top-right corner of the chart. * Black line with diamond markers: "20-variables formulas" * Black line with circle markers: "40-variables formulas" * Black line with triangle markers: "50-variables formulas" ### Detailed Analysis * **20-variables formulas (Black line with diamond markers):** * The line starts at approximately 0 when the clauses-to-variables ratio is 0. * The line increases to a peak of approximately 10.5 at a ratio of around 1. * The line then decreases, stabilizing at approximately 6.5 when the ratio is 8. * **40-variables formulas (Black line with circle markers):** * The line starts at approximately 0 when the clauses-to-variables ratio is 0. * The line increases to a peak of approximately 19 at a ratio of around 1.5. * The line then decreases, stabilizing at approximately 8 when the ratio is 8. * **50-variables formulas (Black line with triangle markers):** * The line starts at approximately 0 when the clauses-to-variables ratio is 0. * The line increases to a peak of approximately 23 at a ratio of around 1.5. * The line then decreases, stabilizing at approximately 9 when the ratio is 8. ### Key Observations * All three lines start at the origin (0,0). * Each line exhibits a peak, indicating a maximum number of calls at a specific clauses-to-variables ratio. * The peak number of calls increases as the number of variables in the formula increases. * After reaching their peaks, all lines decrease and appear to converge towards a stable value as the clauses-to-variables ratio increases. * The peak for the 20-variable formula occurs at a lower clauses-to-variables ratio than the peaks for the 40 and 50-variable formulas. ### Interpretation The chart suggests that the number of calls required to solve a formula initially increases with the clauses-to-variables ratio, reaching a maximum before decreasing and stabilizing. The peak number of calls is higher for formulas with more variables. This indicates that more complex formulas (with more variables) require more calls to solve, especially around a critical clauses-to-variables ratio. The convergence of the lines at higher ratios suggests that the impact of the number of variables diminishes as the formula becomes heavily constrained. The location of the peak may indicate an "easier-harder-easier" transition, where the problem is easiest to solve at the extremes of the clauses-to-variables ratio. </details> Median number of recursive calls for /3/-literal formulas/. In all experiments with counting models we have observed a phenomenon akin to that characteristic of checking satis/ability/, 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 /3/) this /\hard/" ratio is /1/./2/, while it has been reported in many works /(e/.g/./, Mitchell et al/./, /1/9/9/2/) 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 satis/able/, 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 satis/ability/. /6/. Concluding Remarks We have presented an algorithm /(CDP/) for counting models of a propositional formula F/. The previous sections considered CNF formulas/, however/, it is easy to construct a dual This feature is also common to the algorithms presented by Dubois /(/1/9/9/1/) and by Zhang algorithm for DNF formulas/. Comparing algorithm CDP with that of Iwama /(/1/9/8/9/) and Lozinskii /(/1/9/9/2/)/, 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/. /4/6/6 Davis/-Putnam Procedure Helps Counting Models /(/1/9/9/6/)/. In contrast to checking satis/ability/, pure literals slow down counting models by least one variable is deleted/, the maximal number of stored clauses is bounded by mn/. During the experiments we checked also the maximal number M of stored clauses/. The results showed that M does almost not depend on n/, such that M / sm t /, where t / /1/:/3 is not depending on p/1 and p /2 /, while s depends on p /1 and p /2 /. Table /1 displays s as a function of p /1 and p/2 /. Figure /1 in Appendix B shows average values of M for n /= /5/0/; p /1 /= p /2 /= /0/:/1/; /0/:/2/; /0/:/3/. these algorithms/. The experiments made with algorithm CDP have shown that it performs better than that of Lozinskii /(/1/9/9/2/)/. However the main advantage of CDP is in the amount of storage it requires/. In the experiments that have been performed by Lozinskii /(/1/9/9/2/) for m / /1/0/0 and n / /3/0/, there were cases with thousands of clauses stored during the run of the algorithm/. Since algorithm CDP performs a depth/-/rst search of the split tree/, and by each split at The maximum of M in all our experiments was /1/4/9/1 /(for n /= /5/0/; m /= /2/0/0/)/. /0/./2 | | p/2 | | |---------------|---------------|-------------------| | p/1 | | s | | /0/./1 /0/./1 | /0/./1 /0/./2 | /1/./5/4 /0/./8/2 | | /0/./1 | | | | | /0/./3 /0/./2 | /0/./5/7 /0/./7/4 | | /0/./2 | | | /0/./3 /0/./5/0 /0/./3 /0/./3 /0/./4/6 Table /1/: s as a function of p /1 and p/2 The analysis of the running time of CDP follows the method developed by Goldberg /(/1/9/7/9/) and by Goldberg et al/. /(/1/9/8/2/)/. This method was used also by Iwama /(/1/9/8/9/)/. The well known criticisms by Franco and Paull /(/1/9/8/3/)/, and by Mitchell et al/. /(/1/9/9/2/) points out that the instances generated by this method are mostly satis/able/, and that is indeed the reason for the good performance of satis/ability checking algorithms/: the algorithms /nd rapidly one model of the formula/. This point does not apply when we seek not only just for predicate calculus formulas is a next challenge of a great importance/. one model but all the models/. Finally/, it should be noted that the algorithms for counting models developed so far are designed for 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 predicate calculus/. Therefore/, developing counting algorithms Acknowledgments 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/. /4/6/7 Appendix A/. Proofs Birnbaum /& Lozinskii Proof/. Theorem /1 For p /= /1 /3 /, T/(m/; n/) /= O/(m /2 n/)/: /: /1 n /= /0 or m /= /0 <!-- formula-not-decoded --> /: /1 n /= /0 or m /= /0 The di/erence between /(/2/) and /(/1/)/, the recurrence for S/(m/; n/) and the recurrence for T/(m/; n/)/, is the extra term /( /2 /) m T/(m/; n /BnZr /1/) in the latter/. To compare T/(m/; n/) and S/(m/; n/) <!-- formula-not-decoded --> /3 we /rst need the following result/. for m /= /0/; /1/; /2/; /3/; /4 completes the proof for all m / /0 and all n / /0/. Lemma /1 For all m / /0 and all n / /0/, S/(m/; n/) / /( /3 /2 /) m/BnZr/1 cmn/. Proof/. Goldberg /(/1/9/7/9/) showed that S/(m/; n/) / cm /2 n/. Since m /< /( /3 /2 /) m/BnZr/1 for m / /5/, this proves the lemma for all m / /5 and all n / /0/. Direct computation of S/(m/; n/)/, due to /(/2/)/, Now T/(m/; n/) can be estimated as follows/. Proof/. By induction on n/. The assertion is true for n / /1/. Lemma /2 For all m and all n/, T/(m/; n/) / /3 /
S/(m/; n/)/. <!-- formula-not-decoded --> <!-- formula-not-decoded --> k/=/1 k /3 /3 Since S/(m/; n/) /= O/(m /2 n/) and T /(m/; n/) / /3/
S/(m/; n/)/, we get for p /= /1 /, T/(m/; n/) /= O/(m /2 According to /(/2/)/, so/, T/(m/; n/) / /3S/(m/; n/) /+ /3/( /2 /3 /) m S/(m/; n /BnZr /1/) /BnZr /2cmn/. For all n /> /0/, S/(m/; n /BnZr /1/) / S/(m/; n/)/, and by Lemma /1/, for all m and all n/, /3/( /2 /3 /) m S/(m/; n/) / /2cmn/. This completes the proof/. /4/6/8 /3 n/)/: Davis/-Putnam Procedure Helps Counting Models Theorem /2 T/(m/; n/) /= O/(m d n/)/, where d /= d /BnZr/1 log /2 /(/1/BnZrp/) e/. Proof/. We analyze the recurrence inequality for any p/, using considerations similar to those of Goldberg et al/. /(/1/9/8/2/)/. /: /1 <!-- formula-not-decoded --> <!-- formula-not-decoded --> n /= /0 or m /= /0 k/=/1 A solution of /(/4/) is linear in n/, since this recurrence is linear in the T /0 s/. Now for any value T/(m/; n/) / am d n/; where d /= d m/0 let us choose a constant a such that for all m / m /0 <!-- formula-not-decoded --> and therefore/, /(/5/) <!-- formula-not-decoded --> /(/1 /BnZr /(/1 /BnZr p/) k/=/1 <!-- formula-not-decoded --> <!-- formula-not-decoded --> cmn /= O/(mn/)/, and so/, <!-- formula-not-decoded --> T/(m/; n/) / /1 /BnZr /(/1 /BnZr p/) m /1 /BnZr /(/1 /BnZr p/) m /4/6/9 /)/: that is Birnbaum /& Lozinskii <!-- formula-not-decoded --> d /> /1 /(/8/) Second/, for /0 /< p /< /1/, /(/1 /BnZr p/) m diminishes monotonically/, and tends to /0 as m /! /1/, hence /[/1 /BnZr /1 /BnZr /(/1 /BnZr p/) m /]/: /(/7/) First/, let g denote the subexpression of /(/7/) in square brackets/. For all d/, g is less than /1/, hence/, d must be greater than /1 to satisfy O/(m max/(/1/;d/BnZr/1/) /) / m d /. So/, to make g positive/, we need <!-- formula-not-decoded --> d /> log /2 /(/1 /BnZr p/) /(/9/) Thus/, choosing m /(and hence/, m /0 /) su/ciently large /(depending on the value of the O/(m /BnZr/1 /) expression in /(/6/)/)/, and determining the values of a and d satisfying conditions /(/5/)/, /(/8/)/, /(/9/)/, establishes T /(m/; n/) /= O/(m d n/)/, where d /= d /BnZr/1 log /2 /(/1/BnZrp/) e/. /4/7/0 Davis/-Putnam Procedure Helps Counting Models Appendix B/. More Experimental Data | Number clauses | /4/0 | /5/0 | /6/0 | |------------------|-----------------------------|-----------------------------|---------------------------| | of /1/0 | variables /1/6 | variables /1/5 | variables /1/3 | | /2/0 | /2/3/4 | /1/9/1 | | | | /1/6/0/0 | | /1/5/3 | | /3/0 | /6/2/9/4 | /1/2/0/3 /5/0/7/6 | /8/6/8 /3/6/9/9 | | /4/0 /5/0 | | | /1/1/3/7/0 | | /6/0 | /1/9/8/5/6 /4/6/6/4/5 | /1/6/3/8/4 /5/3/2/9/6 | /2/8/4/6/7 | | | /1/0/1/6/0/7 | /1/0/9/3/2/7 | /7/5/4/7/2 | | /7/0 | /1/8/6/1/9/9 | /2/4/4/2/4/8 | /1/5/3/3/8/4 | | /8/0 | | | | | /9/0 /1/0/0 | /2/9/9/2/2/0 | /4/2/6/1/6/9 | /3/1/1/6/6/8 /6/3/5/7/1/2 | | | /5/0/7/8/8/8 /1/0/9/3/3/8/3 | /8/0/7/6/6/9 /2/2/2/2/4/9/9 | | | /1/2/0 /1/4/0 | | | /1/6/8/7/1/4/7 | | | /1/9/4/5/8/7/4 | /5/5/0/7/3/4/0 | /4/2/8/9/7/1/3 | | /1/6/0 | /3/0/9/5/8/4/8 | /1/1/8/2/4/3/2/5 | /1/0/8/1/2/9/3/1 | /1/8/0 /2/0/0 Table /1/: /4/4/4/1/7/6/0 /2/2/4/4/4/0/8/6 /2/0/2/3/0/3/5/2 /6/3/7/7/5/0/1 /3/9/1/1/9/0/4/5 /3/7/3/8/1/2/0/7 Average number of recursive calls for p /1 /= p /2 /= /0/:/1 | Number clauses | /2/0 | /3/0 | /4/0 | |------------------|--------------|--------------|-------------------| | of /1/0 | variables /8 | variables /7 | variables /7 | | /2/0 | /4/1 | | | | | /1/1/0 | /3/4 /8/8 | /2/9 /7/6 | | /3/0 /4/0 | /2/3/4 | /1/8/5 | /1/5/0 | | /5/0 | /4/3/3 | /3/3/2 | /2/6/6 | | /6/0 | /6/4/8 | /5/4/5 | /4/2/4 | | /7/0 | /9/7/3 | /8/3/5 | /6/3/6 | | | /1/3/0/2 | /1/2/4/0 | /9/1/9 | | /8/0 | /1/6/8/3 | /1/7/3/1 | /1/2/2/5 | | /9/0 /1/0/0 | /2/0/8/9 | /2/3/4/9 | /1/6/4/7 | | /1/2/0 | /3/1/2/8 | /3/9/4/7 | | | /1/4/0 | /3/9/3/4 | /6/4/6/1 | /2/7/9/1 | | /1/6/0 | /5/2/0/9 | /9/8/2/1 | /4/3/3/9 /6/4/4/6 | /1/8/0 /2/0/0 Table /2/: /6/0/5/1 /1/3/6/6/1 /9/0/0/2 /6/5/1/3 /1/8/6/9/6 /1/2/1/9/3 Average number of recursive calls for p /1 /= p /2 /= /0/:/2 /4/7/1 Birnbaum /& Lozinskii | Number clauses | /2/0 | /3/0 | |------------------|------------------------------------------------------------------------------------------|--------------| | of | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | | | /1/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | variables /5 | | /2/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /1/5 | | /3/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /2/9 | | /4/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /4/5 | | /5/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /6/5 | | /6/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /8/9 | | /7/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /1/1/4 | | /8/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /1/4/6 | | /9/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /1/7/8 | | /1/0/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /2/1/5 | | /1/2/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /2/9/5 | | /1/4/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /3/8/4 | | /1/6/0 | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | /4/8/9 | | | variables /5 /1/7 /3/2 /5/2 /7/8 /1/0/4 /1/3/4 /1/7/6 /2/1/8 /2/6/5 /3/6/3 /4/9/5 /6/2/3 | | Table /3/: /1/8/0 /8/0/7 /6/0/7 /2/0/0 /9/6/6 /7/2/4 Average number of recursive calls for p /1 /= p /2 /= /0/:/3 | Number clauses | /3/0 | /4/0 | /5/0 | |------------------|-----------------------|---------------------------|-------------------| | of | | variables | | | /1/0 | variables /1/1 | | variables /9 | | /2/0 | /8/9 | /1/0 /7/5 | /6/0 | | | /3/4/3 | | /2/1/1 | | /3/0 | /1/0/2/5 | /2/9/0 | /5/7/2 | | /4/0 /5/0 | /2/1/7/9 | /7/5/2 /1/7/0/9 | /1/2/5/2 | | /6/0 | | /3/4/3/8 | /2/4/7/3 | | | /4/1/9/5 /7/3/0/9 | /6/2/5/0 | | | /7/0 | /1/1/7/4/0 | | /4/3/1/1 /7/6/2/2 | | /8/0 | /1/9/2/2/4 | /1/0/9/1/9 /1/7/6/1/9 | /1/0/9/9/9 | | /9/0 | | | /1/6/7/3/4 | | /1/0/0 /1/2/0 | /2/5/8/6/6 /4/4/7/2/9 | /2/7/8/4/7 /5/7/5/4/8 | | | /1/4/0 | /7/4/2/8/0 | | /3/7/0/5/1 | | | | /1/0/9/4/6/9 /1/8/5/5/6/8 | /6/8/3/5/4 | | /1/6/0 | /1/0/9/1/3/4 | | /1/1/7/1/7/5 | Table /4/: /1/8/0 /1/4/4/6/9/8 /3/0/4/9/8/3 /2/0/1/8/2/2 /2/0/0 /1/8/2/5/1/6 /4/6/3/5/0/3 /3/0/7/8/5/1 Average number of recursive calls for p /1 /= /0/:/1/, p /2 /= /0/:/2 /4/7/2 Davis/-Putnam Procedure Helps Counting Models | Number clauses | /3/0 | /4/0 | /5/0 | |------------------|--------------|--------------|---------------------| | of | | | | | /1/0 | variables /9 | variables /9 | variables | | /2/0 | /5/1 | /4/1 | /8 /3/6 | | | /1/4/1 | /1/1/4 | /9/7 | | /3/0 /4/0 | /3/3/3 | /2/3/9 | /2/0/6 | | /5/0 | /6/3/5 | /4/4/0 | /3/6/1 | | /6/0 | /1/0/4/8 | /7/8/2 | /5/9/6 | | /7/0 | /1/6/3/8 | /1/1/1/7 | /9/0/3 | | | /2/6/0/3 | /1/7/0/6 | /1/3/1/7 | | /8/0 /9/0 | /3/8/0/1 | /2/4/9/3 | | | /1/0/0 | /4/8/1/3 | /3/5/2/3 | /1/9/1/5 /2/5/6/8 | | /1/2/0 | /8/5/9/1 | /6/0/8/7 | | | /1/4/0 | /1/4/0/4/3 | /1/0/2/2/1 | /4/4/0/1 | | | /2/1/2/3/7 | | /7/2/5/4 /1/0/7/3/1 | | /1/6/0 | | /1/5/0/8/7 | | Table /5/: /1/8/0 /2/9/7/8/2 /2/2/8/3/2 /1/5/2/7/1 /2/0/0 /4/0/5/5/0 /3/1/8/8/2 /2/0/7/6/0 Average number of recursive calls for p /1 /= /0/:/1/, p /2 /= /0/:/3 | Number clauses | /2/0 | /3/0 | |------------------|---------------|-----------------| | of | | | | /1/0 | variables /6 | variables /6 | | /2/0 | /2/4 | /2/1 | | /3/0 | /5/6 | /4/5 | | /4/0 | /1/0/1 | /8/0 | | /5/0 | /1/6/4 | /1/2/4 | | /6/0 | /2/3/4 | /1/8/9 | | /7/0 | | | | /8/0 | /3/3/7 /4/5/6 | /2/5/5 /3/5/2 | | /9/0 | /6/0/6 | /4/4/7 | | /1/0/0 | /7/6/2 | /5/6/7 | | /1/2/0 | /1/1/8/3 | | | /1/4/0 | /1/6/0/8 | /8/5/1 /1/2/2/5 | | /1/6/0 | /2/1/8/4 | /1/6/2/1 | Table /6/: /1/8/0 /2/8/8/7 /2/1/5/9 /2/0/0 /3/5/3/3 /2/7/4/3 Average number of recursive calls for p /1 /= /0/:/2/, p /2 /= /0/:/3 /4/7/3 Birnbaum /& Lozinskii | | | | | Standard | |-------------------------------|-----------|----------------|---------------------------|-------------------------| | Probabilities | | | Average | deviation | | | Variables | Clauses /1/2/0 | /1/0/9/3/3/8/3 | /4/1/2/2/4/6 | | p/1 /= p/2 /= /0/:/1 | /4/0 | | /6/3/7/7/5/0/1 | /2/9/2/1/0/2/9 | | | | /2/0/0 /1/2/0 | /2/2/2/2/4/9/9 | /1/1/4/1/9/0/9 | | | /5/0 | | | | | | | /2/0/0 | /3/9/1/1/9/0/4/5 /3/9/4/7 | /1/4/5/8/7/0/9/6 /9/0/6 | | p/1 /= p/2 /= /0/:/2 | /3/0 | /1/2/0 /2/0/0 | | | | | | /1/2/0 | /1/8/6/9/6 /2/7/9/1 | /3/3/8/7 /4/7/3 | | | /4/0 | | | | | | /2/0 | /2/0/0 /1/2/0 | /1/2/1/9/3 | /2/0/9/7 /4/3 | | p/1 /= p/2 /= /0/:/3 | | /2/0/0 | /3/6/3 /9/6/6 | /1/0/6 | | | | /1/2/0 | | /2/5 | | | /3/0 | /2/0/0 | /2/9/5 /7/2/4 | /6/3 | | | | /1/2/0 | /5/7/5/4/8 | /2/1/9/4/6 | | p/1 /= /0/:/1/, p/2 /= /0/:/2 | /4/0 | /2/0/0 | /4/6/3/5/0/3 | /1/3/5/1/7/1 | | | /5/0 | /1/2/0 | /3/7/0/5/1 | /1/1/0/8/1 | | | | /2/0/0 | | /9/0/8/9/7 | | | /3/0 | /1/2/0 | /3/0/7/8/5/1 /8/5/9/1 | /2/2/4/4 | | p/1 /= /0/:/1/, p/2 /= /0/:/3 | | /2/0/0 | | /7/0/0/3 | | | | /1/2/0 | /4/0/5/5/0 /6/0/8/7 | /1/3/4/9 | | | /4/0 | /2/0/0 | | | | /= /0/:/2/, /= /0/:/3 | | /1/2/0 | /3/1/8/8/2 /1/1/8/3 | /6/2/6/4 /1/8/3 | | p/1 p/2 | /2/0 | /2/0/0 | | /5/1/4 | | | | | /3/5/3/3 | | Table /7/: /3/0 /1/2/0 /8/5/1 /1/2/6 /2/0/0 /2/7/4/3 /3/9/2 Samples of standard deviation of number of recursive calls /4/7/4 Davis/-Putnam Procedure Helps Counting Models | Clauses/-to/-variables ratio | /2/0 | /4/0 | /5/0 | |--------------------------------|-------------------|---------------------------|-----------------------------------| | /0/./2 | variables | variables /1/0/5/6 | variables /3/2/0/6/2 | | | /5/9 /2/7/2 | | /2/5/0/0/9/8/7 | | /0/./4 /0/./6 | | /1/7/7/1/5 | /1/1/6/3/4/6/7/0 | | | /6/2/5 | /1/1/3/1/8/5 /2/5/2/0/4/4 | /3/1/3/7/6/6/8/6 | | /0/./8 | /9/9/3 /1/3/0/1 | | /3/4/8/4/3/0/2/5 | | /1/./0 | /1/5/2/1 | /5/0/2/6/6/9 /5/3/8/5/7/9 | /5/9/4/4/3/5/8/0 | | /1/./2 /1/./4 | | /5/2/9/5/2/0 | | | /1/./6 | /1/4/4/5 /1/3/2/8 | | /4/8/8/0/5/4/4/0 /2/6/4/1/6/1/3/4 | | | /1/2/8/3 | /4/1/2/5/6/3 /3/0/7/9/3/9 | /2/9/4/9/4/0/5/7 | | /1/./8 /2/./0 | | /1/9/4/7/5/4 | /1/1/7/9/2/3/5/1 | | /2/./2 | /1/0/5/0 /7/8/9 | | /8/2/7/7/5/2/9 | | /2/./4 | /6/6/4 | /1/0/5/0/8/9 /6/0/5/4/8 | /4/0/3/7/9/8/6 | | | /5/5/8 | /3/4/0/5/7 | /2/2/0/8/1/4/7 | | /2/./6 /2/./8 | /3/8/7 | /1/8/8/7/5 | /9/2/3/2/2/8 | | /3/./0 | /3/4/1 | | /6/3/3/4/0/7 | | /4/./0 | /1/3/5 | /9/5/7/4 | /2/1/3/3/9 | | | /8/6 | /8/1/6 | | | /5/./0 | | /3/3/5 /2/2/5 | /1/4/4/3 | | /6/./0 | /6/5 | | /8/6/2 | Table /8/: /7/./0 /5/5 /1/6/0 /5/5/8 /8/./0 /4/8 /1/3/8 /4/7/6 Median number of recursive calls for /3/-literal clauses/, n /= /2/0/; /4/0/; /5/0 /4/7/5 Birnbaum /& Lozinskii <details> <summary>Image 4 Details</summary>  ### Visual Description ## Chart: Number of Clauses Stored vs. Number of Clauses in the Formula ### Overview The image is a line chart comparing the number of clauses stored versus the number of clauses in the formula for three different parameter settings: p1=p2=0.1, p1=p2=0.2, and p1=p2=0.3. The x-axis represents the number of clauses in the formula, and the y-axis represents the number of clauses stored. All three lines show an increasing trend, with p1=p2=0.1 having the steepest slope and thus the highest number of clauses stored for a given number of clauses in the formula. ### Components/Axes * **X-axis:** Number of clauses in the formula. Scale ranges from 0 to 200, with tick marks at intervals of 20. * **Y-axis:** Number of clauses stored. Scale ranges from 0 to 1300, with tick marks at intervals of 100. * **Legend (top-right):** * Line with diamond markers: p1=p2=0.1 * Line with circle markers: p1=p2=0.2 * Line with triangle markers: p1=p2=0.3 ### Detailed Analysis * **p1=p2=0.1 (diamond markers):** The line starts at approximately (0,0) and increases almost linearly. * At x=20, y ≈ 80 * At x=40, y ≈ 170 * At x=60, y ≈ 270 * At x=80, y ≈ 370 * At x=100, y ≈ 470 * At x=120, y ≈ 580 * At x=140, y ≈ 700 * At x=160, y ≈ 830 * At x=180, y ≈ 980 * At x=200, y ≈ 1200 * **p1=p2=0.2 (circle markers):** The line starts at approximately (0,0) and increases, but at a slower rate than p1=p2=0.1. * At x=20, y ≈ 30 * At x=40, y ≈ 70 * At x=60, y ≈ 120 * At x=80, y ≈ 180 * At x=100, y ≈ 240 * At x=120, y ≈ 300 * At x=140, y ≈ 370 * At x=160, y ≈ 440 * At x=180, y ≈ 510 * At x=200, y ≈ 580 * **p1=p2=0.3 (triangle markers):** The line starts at approximately (0,0) and increases at the slowest rate among the three. * At x=20, y ≈ 10 * At x=40, y ≈ 30 * At x=60, y ≈ 60 * At x=80, y ≈ 90 * At x=100, y ≈ 120 * At x=120, y ≈ 160 * At x=140, y ≈ 200 * At x=160, y ≈ 240 * At x=180, y ≈ 290 * At x=200, y ≈ 350 ### Key Observations * All three lines start at or near the origin (0,0). * The line representing p1=p2=0.1 has the steepest slope, indicating a higher number of clauses stored for a given number of clauses in the formula compared to the other two parameter settings. * The line representing p1=p2=0.3 has the shallowest slope, indicating the lowest number of clauses stored for a given number of clauses in the formula. * The relationship between the number of clauses in the formula and the number of clauses stored appears to be approximately linear for all three parameter settings, although there might be a slight curve, especially for p1=p2=0.1. ### Interpretation The chart demonstrates the relationship between the number of clauses in a formula and the number of clauses stored, under different parameter settings (p1 and p2). The parameter setting p1=p2=0.1 results in the highest number of clauses stored for a given number of clauses in the formula, suggesting that this setting is more efficient in storing clauses. Conversely, p1=p2=0.3 results in the lowest number of clauses stored, indicating lower efficiency. The approximately linear relationship suggests a direct proportionality between the number of clauses in the formula and the number of clauses stored, with the slope of the line determined by the parameter settings. The data suggests that the values of p1 and p2 significantly impact the storage efficiency of clauses in the formula. </details> /G31/G58/G50/G45/G48/G55/G03/G52/G49/G03/G46/G4F/G44/G58/G56/G48/G56/G03/G4C/G51/G03/G57/G4B/G48/G03/G49/G52/G55/G50/G58/G4F/G44 Figure /1/: Average of maximal number of clauses stored during the running of CDP for /5/0 /4/7/6 variables/. Davis/-Putnam Procedure Helps Counting Models - References Davis/, M/./, /& Putnam/, H/. /(/1/9/6/0/)/. A computing procedure for quanti/cation theory/. Journal - Computer Science/, /8/1/(/1/)/, /4/9/{/6/4/. Franco/, J/./, /& Paull/, M/. /(/1/9/8/3/)/. Probabilistic analysis of the Davis/-Putnam procedure for - of the ACM/, /7/, /2/0/1/{/2/1/5/. Dubois/, J/. /(/1/9/9/1/)/. Counting the number of solutions for instances of satis/ability/. Theoretical - solving the satis/ability problem/. Discrete Applied Mathematics/, /5/, /7/7/{/8/7/. Goldberg/, A/. /(/1/9/7/9/)/. Average case complexity of the satis/ability problem/. In Proceedings - Putnam procedures/. Information Processing Letters/, /1/5/(/2/)/, /7/2/{/7/5/. Grove/, A/./, Halpern/, J/./, /& Koller/, D/. /(/1/9/9/4/)/. Random worlds and maximum entropy/. Journal - of the /4th Workshop on Automated Deduction Austin/, Texas/. Goldberg/, A/./, Purdom/, P/./, /& Brown/, C/. /(/1/9/8/2/)/. Average time analysis of simpli/ed Davis/- - of Arti/cial Intelligence Research/, /2/, /3/3/{/8/8/. Iwama/, K/. /(/1/9/8/9/)/. CNF satis/ability test by counting and polynomial average time/. SIAM - /3/4/9/{/3/6/5/. Lozinskii/, E/. /(/1/9/8/9/)/. Answering atomic queries in inde/nite deductive databases/. Interna/- - Journal on Computing/, /1/8/(/2/)/, /3/8/5/{/3/9/1/. Linial/, N/./, /& Nisan/, N/. /(/1/9/9/0/)/. Approximate inclusion/-exclusion/. Combinatorica/, /1/0 /(/4/)/, - tional Journal of Intelligent Systems/, /4/(/4/)/, /4/0/3/{/4/2/9/. Lozinskii/, E/. /(/1/9/9/2/)/. Counting propositional models/. Information Processing Letters/, /4/1/(/6/)/, - imental and Theoretical Arti/cial Intelligence/, /7/, /3/6/1/{/3/7/8/. Luby/, M/./, /& Veli/ ckovi/ c/, B/. /(/1/9/9/1/)/. On deterministic approximation of DNF/. In Proceedings - /3/2/7/{/3/3/2/. Lozinskii/, E/. /(/1/9/9/5/)/. Is there an alternative to parsimonious semantics /?/. Journal of Exper/- - of STOC/'/9/1/. Mitchell/, D/./, Selman/, B/./, /& Levesque/, H/. /(/1/9/9/2/)/. Hard and easy distributions of SAT - /2/7/3/{/3/0/2/. Valiant/, L/. /(/1/9/7/9/)/. The complexity of computing the permanent/. Theoretical Computer - problems/. In Proceedings of AAAI/-/9/2/. Roth/, D/. /(/1/9/9/6/)/. On the hardness of approximate reasoning/. Arti/cial Intelligence/, /8/2/, - Science/, /8/, /1/8/9/{/2/0/1/. Zhang/, W/. /(/1/9/9/6/)/. Number of models and satis/ability of sets of clauses/. Theoretical /4/7/7 Computer Science/, /1/5/5/(/1/)/, /2/7/7/{/2/8/8/.