1106.0218

# Unknown Title 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 / /)/) /: $$\begin{array}{ll} \sum _ { i = 1 } ^ { m } | U _ { S _ { i } } | & = \sum _ { i < j } | S _ { i } | - \sum _ { i < j < k } | S _ { i } | - \sum _ { i < j < k < l } | S _ { i } | \\ & + ( - 1 ) ^ { m + 1 } | S _ { 1 } | n \cdot \ldots \cdot n S _ { m } . \end{array}$$ 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 ``` <doc> function DPP (F: propositional CNF formula); 1. if F is empty then return true; 2. if F contains an empty clause then return false; 3.* The pure literal rule *) if there exists a pure literal l in F (* such that l does not appear in C ); (* delete from F all clas- F1 = {C | C ∈ F}; return DPP(F1); return true *) </doc> ``` 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 ``` <doc> 4. (* The unit clause rule *) if F contains a unit clause Γ; then F = {C − {f} | C return DPP(F ); 1 i i } 5. (* The splitting rule *) choose a variable x of F = {C − {x} | C e 1 i 2 F = {C − {x} | C e 1 i 2 return (DPP(F) v It can be seen that the cases of the splitting rule, * are actually particular the splitting rule chooses * </doc> ``` 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 ``` <doc> Based on these observations, the following function CDP counts monomial over n variables. function CDP (F: propositional CNF formula; n: integer): 1. if F is empty then return 2"; 2. if F contains an empty clause then return 0; 3. if F contains a unit clause {i} then F = {C - {i}} | C ∈ F; i return CDP(F ,n-1); 4. choose a variable x of F; F = {C - {x}} | C ∈ F; 1 2 F = {C - {x} | C ∈ F; 2 3 return CDP(F ,n-1) + Any iteration of CDP deletes the chosen variable, and so, reduces the of F by at least one. This guarantees that CDP terminates (either on st </doc> ``` ## 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 $$T ( m , n ) ≤ \sum _ { k = 0 } ^ { n } \frac { c _ { mn } } { 1 }$$ 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/: $$\sum _ { m = 1 } ^ { n } \sum _ { k = 1 } ^ { n } ( \frac { T ( m , n - 1 ) + } { 2 } \sum _ { j = 1 } ^ { n } ( \frac { T ( m - k , n - 1 ) } { 3 } ) ( \frac { 3 } { 2 } m - k T ( m - k , n - 1 )$$ ## 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 ## Line Chart: Log of Number of Calls vs. Number of Clauses in the Formula ### Overview The image is a line chart depicting the relationship between the number of clauses in a formula and the logarithm of the number of calls required. Three distinct data series are plotted, each corresponding to different numbers of variables (50, 30, 20) and fixed probabilities (p1 = p2 = 0.1, 0.2, 0.3). The y-axis uses a logarithmic scale, and the x-axis represents the number of clauses. The chart shows exponential growth trends for all series, with steeper slopes for higher variable counts. ### Components/Axes - **X-axis**: "Number of clauses in the formula" (ranges from 0 to 200, with increments of 20). - **Y-axis**: "log of number of calls" (ranges from 0 to 26, with increments of 2). - **Legend**: Located on the right side of the chart, with three entries: - **Black circles**: 50 variables, p1 = p2 = 0.1 - **Dark gray squares**: 30 variables, p1 = p2 = 0.2 - **Light gray triangles**: 20 variables, p1 = p2 = 0.3 ### Detailed Analysis 1. **50 Variables (p1 = p2 = 0.1)**: - **Trend**: Steep upward slope, starting at (0, 0) and reaching approximately (200, 25). - **Key Data Points**: - At 20 clauses: ~4 - At 40 clauses: ~6 - At 60 clauses: ~8 - At 80 clauses: ~10 - At 100 clauses: ~12 - At 120 clauses: ~14 - At 140 clauses: ~16 - At 160 clauses: ~18 - At 180 clauses: ~20 - At 200 clauses: ~22 2. **30 Variables (p1 = p2 = 0.2)**: - **Trend**: Moderate upward slope, starting at (0, 0) and reaching approximately (200, 14). - **Key Data Points**: - At 20 clauses: ~3 - At 40 clauses: ~5 - At 60 clauses: ~7 - At 80 clauses: ~9 - At 100 clauses: ~11 - At 120 clauses: ~13 - At 140 clauses: ~15 - At 160 clauses: ~17 - At 180 clauses: ~19 - At 200 clauses: ~21 3. **20 Variables (p1 = p2 = 0.3)**: - **Trend**: Gentle upward slope, starting at (0, 0) and reaching approximately (200, 10). - **Key Data Points**: - At 20 clauses: ~2 - At 40 clauses: ~4 - At 60 clauses: ~6 - At 80 clauses: ~8 - At 100 clauses: ~10 - At 120 clauses: ~12 - At 140 clauses: ~14 - At 160 clauses: ~16 - At 180 clauses: ~18 - At 200 clauses: ~20 ### Key Observations - **Exponential Growth**: All series exhibit exponential growth, as indicated by the logarithmic y-axis. The 50-variable series grows the fastest, followed by 30 and 20 variables. - **Probability Impact**: Despite identical probabilities (p1 = p2) across series, the number of variables directly influences the slope. Higher variable counts result in steeper growth. - **Consistency**: The legend colors and markers (circles, squares, triangles) align precisely with their respective data series. ### Interpretation The chart suggests that the complexity of a formula (measured by the number of variables) significantly impacts the number of calls required, with more variables leading to exponentially higher call counts. The logarithmic scale on the y-axis emphasizes this exponential relationship. The fixed probabilities (p1 = p2) imply that the observed trends are primarily driven by variable count rather than probabilistic factors. This could reflect scenarios where increased variable interactions or dependencies in a formula necessitate more computational or operational "calls" to resolve or evaluate the system. </details> Average number of recursive calls for di/erent values of p/1/; p/2 <details> <summary>Image 2 Details</summary>  ### Visual Description ## Line Chart: Log of Number of Calls vs. Number of Clauses in the Formula ### Overview The chart illustrates the relationship between the number of clauses in a formula and the logarithmic scale of the number of calls required, across three scenarios with varying numbers of variables and parameter values (p1, p2). Three data series are plotted, each with distinct line styles and markers. ### Components/Axes - **X-axis**: "Number of clauses in the formula" (range: 0–200, linear scale). - **Y-axis**: "log of number of calls" (range: 0–20, logarithmic scale). - **Legend**: Positioned on the right, with three entries: 1. **40 variables, p1=0.1, p2=0.2** (solid black line with star markers). 2. **30 variables, p1=0.1, p2=0.3** (dashed black line with circle markers). 3. **20 variables, p1=0.2, p2=0.3** (dotted black line with square markers). ### Detailed Analysis - **40 variables (solid line)**: - At 20 clauses: ~log(3) ≈ 0.5. - At 100 clauses: ~log(12) ≈ 1.1. - At 200 clauses: ~log(18) ≈ 1.26. - **Trend**: Steepest upward slope, indicating the highest growth rate. - **30 variables (dashed line)**: - At 20 clauses: ~log(5) ≈ 0.7. - At 100 clauses: ~log(10) ≈ 1.0. - At 200 clauses: ~log(14) ≈ 1.15. - **Trend**: Moderate upward slope, less steep than 40 variables. - **20 variables (dotted line)**: - At 20 clauses: ~log(2) ≈ 0.3. - At 100 clauses: ~log(8) ≈ 0.9. - At 200 clauses: ~log(12) ≈ 1.08. - **Trend**: Gentle upward slope, least steep among the three. ### Key Observations 1. All three series exhibit a **positive correlation** between the number of clauses and the log of calls, confirming exponential growth in calls as clauses increase. 2. The **40-variable series** grows fastest, followed by 30 variables, then 20 variables. 3. The **logarithmic y-axis** compresses the scale, emphasizing multiplicative differences (e.g., 10x vs. 2x growth). 4. **Parameter differences** (p1, p2) do not override the dominant effect of variable count on growth rate. ### Interpretation The chart demonstrates that **formula complexity (clauses)** and **variable count** are critical drivers of computational effort (calls). Higher variable counts amplify the impact of additional clauses, as seen in the steeper slope for 40 variables. The parameters p1 and p2 likely modulate secondary aspects of the model (e.g., efficiency thresholds), but their influence is secondary to the variable count. The logarithmic scale highlights that even small increases in clauses lead to disproportionate rises in calls, suggesting exponential time complexity in the underlying process. This aligns with scenarios like combinatorial search or constraint satisfaction problems, where clause addition exponentially expands the solution space. </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 ## Line Chart: Log of Number of Calls vs. Clauses-to-Variables Ratio ### Overview The image is a line chart depicting the logarithmic relationship between the "clauses-to-variables ratio" (x-axis) and the "log of number of calls" (y-axis). Three data series are plotted, representing formulas with 20, 40, and 50 variables. The chart shows how the log of calls changes as the clauses-to-variables ratio increases, with distinct trends for each variable count. ### Components/Axes - **Title**: "log of number of calls" (top center). - **X-axis**: "clauses-to-variables ratio" (horizontal), scaled from 0 to 8 in increments of 1. - **Y-axis**: "log of number of calls" (vertical), scaled from 0 to 24 in increments of 2. - **Legend**: Located in the top-right corner, with three entries: - **20-variables formulas**: Black line with diamond markers. - **40-variables formulas**: Dark gray line with square markers. - **50-variables formulas**: Light gray line with star markers. ### Detailed Analysis 1. **20-variables formulas (Black, Diamonds)**: - Peaks at approximately **x = 2** (clauses-to-variables ratio) with a y-value of **~22**. - Declines sharply after x = 2, reaching ~8 at x = 8. - Initial rise is steep, with a plateau between x = 0 and x = 1. 2. **40-variables formulas (Dark Gray, Squares)**: - Peaks at approximately **x = 1.5** with a y-value of **~18**. - Declines more gradually than the 20-variable series, reaching ~6 at x = 8. - Initial rise is less steep than the 20-variable series. 3. **50-variables formulas (Light Gray, Stars)**: - Peaks at approximately **x = 1** with a y-value of **~16**. - Declines steadily, reaching ~4 at x = 8. - Initial rise is the least steep among the three series. ### Key Observations - **Peak Shifts**: Higher variable counts (50 > 40 > 20) peak at lower clauses-to-variables ratios (1 < 1.5 < 2). - **Logarithmic Decay**: All series exhibit a logarithmic decay after their respective peaks, with steeper declines for lower variable counts. - **Ordering**: The 20-variable series consistently has the highest y-values across all x-values, followed by 40 and 50 variables. ### Interpretation The data suggests that formulas with fewer variables (20) generate a higher log of calls at higher clauses-to-variables ratios compared to formulas with more variables (40, 50). This could indicate that simpler formulas (fewer variables) are more "active" or require more clauses to trigger calls, while complex formulas (more variables) reach their maximum efficiency at lower ratios. The logarithmic scale on the y-axis emphasizes the relative differences in call rates, highlighting that the 20-variable series dominates in magnitude. The trends may reflect computational or structural properties of the formulas, such as sensitivity to clause density or variable interactions. </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 $$Theorem 1 For p = \frac { 1 } { 3 } , T ( m , n ) = O ( m ^ { 2 } n ).$$ Proof/. Theorem /1 For p /= /1 /3 /, T/(m/; n/) /= O/(m /2 n/)/: /: /1 n /= /0 or m /= /0 $$\sum _ { k = 0 } ^ { n - 1 } ( m _ { k } ) \left( \frac { 3 } { 2 } \right) ^ { k } \left( \frac { 3 } { 2 } \right)^ { m - k } T ( m - k , n - 1 )$$ /: /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/) $$\sum _ { k = 1 } ^ { m } ( \frac { 1 } { k } ) ^ { | k | } ( \frac { 1 } { 3 } ) ^ { | 3 - k | } S ( m - k , n - 1 )$$ $$Lemma 1 For all m \geq 0 and n \geq 0 , S ( m , n ) \leq ( \frac { 3 } { 2 } ) ^ { m - 1 } c m n .$$ /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/)/. $$\begin{align*} T(m,n) & \leq c_{m} \\ & \leq c_3 \\ & \text{According to (2), } 3S(m,n) - 3 \cdot \left(\frac{1}{3}\right)^m S(m,n-1) + m + 3 \cdot \left(\frac{1}{3}\right)^m T(m,n-1) + 2 \sum_{k=1}^m k^3 \left(\frac{1}{3}\right)^m S(m,n-k,n-1), \\ & = 3 c_{m} + 3 \cdot \left(\frac{1}{3}\right)^m T(m-k,n-1) + 2 \sum_{k=1}^m k^3 \left(\frac{1}{3}\right)^m S(m-k,n-1), \\ & = ( - )^{m-k} T(m-k,n-1). \end{align*}$$ $$( m , n ) \leq 3 S ( m , n ) + 3 ( \frac { 1 } { k } ) ^ { n } \sum _ { i = 1 } ^ { n } ( \frac { 1 } { \frac { 1 } { k } } ) ^ { - 2 } S ( m - k , n - 1 ) ,$$ /3 k/=/1 k /3 /3 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/. 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 n/)/: /4/6/8 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 $$T ( m , n ) \leq \sum _ { k = 1 } ^ { n } p ^ { | k | } ( 1 - p ) ^ { m - k } T ( m - k , n - 1 )$$ $$It is easy to show, by induction on n, that T ( m , n ) \leq c m _ { k }$$ 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 $$I ( m , n ) \leq a _ { m } ^ { d } n .$$ $$\sum _ { k = 1 } ^ { m } \sum _ { k = 1 } ^ { n } ( p ^ { ( 1 - p ) ^ { m } } ) ^ { d } = ( 1 - p ) ^ { m } + O ( 1 ^ { n } )$$ and therefore/, /(/5/) $$\sum _ { q = 1 } ^ { n } ( p ^ { k } ( 1 - p ) ^ { m - k } ( 1 - \frac { k } { m } ) ^ { d } - ( 1 - p ) ^ { a } + O ( p ^ { k } ( 1 - p ) ^ { m - k } ( 1 - \frac { k } { m } ) ^ { d } )$$ /(/1 /BnZr /(/1 /BnZr p/) k/=/1 $$d _ { n } ( 1 - p ) ^ { m } I ( m , n ) \leq c m n + 2 a m - ( 1 - p ) ^ { m } I ( m , n ) .$$ $$n \cdot O ( m ^ { d - 1 } ) .$$ cmn /= O/(mn/)/, and so/, $$We are going now to find out conditions under which \frac { 2 a m ^ { d } n ( 1 - p ) ^ { d } } { 1 - ( 1 - p ) ^ { d } } + a n \cdot O ( n ^ { a x } ( 1 , d - 1 ) ) \geq a m ^ { d } _ { n }$$ T/(m/; n/) / /1 /BnZr /(/1 /BnZr p/) m /1 /BnZr /(/1 /BnZr p/) m /4/6/9 /)/: that is Birnbaum /& Lozinskii $$O ( m \max \{ 1 , d - 1 \} ) \leq O ( m ^ { d } [ 1 - \frac { 2 ( 1 - p ) ^ { d } } { 1 - ( 1 - p ) ^ { m } } ] .$$ 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 $$\frac { - 1 } { l a r }$$ 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 ## Line Chart: Relationship Between Clauses in Formula and Clauses Stored ### Overview The chart illustrates the relationship between the number of clauses in a formula and the number of clauses stored, across three distinct scenarios defined by the parameters `p1=p2=0.1`, `p1=p2=0.2`, and `p1=p2=0.3`. Each scenario is represented by a distinct line with unique markers and colors. The y-axis represents the "Number of clauses stored," while the x-axis represents the "Number of clauses in the formula." ### Components/Axes - **X-Axis (Horizontal)**: Labeled "Number of clauses in the formula," ranging from 0 to 200 in increments of 20. - **Y-Axis (Vertical)**: Labeled "Number of clauses stored," ranging from 0 to 1300 in increments of 100. - **Legend**: Positioned in the top-right corner, with three entries: - **Black circles**: `p1=p2=0.1` - **Dark gray squares**: `p1=p2=0.2` - **Light gray triangles**: `p1=p2=0.3` ### Detailed Analysis 1. **`p1=p2=0.1` (Black Circles)**: - Starts at (0, 0) and increases steadily. - Approximate values: - At x=20: ~50 - At x=100: ~300 - At x=200: ~580 2. **`p1=p2=0.2` (Dark Gray Squares)**: - Starts at (0, 0) with a steeper slope than `p1=p2=0.1`. - Approximate values: - At x=20: ~70 - At x=100: ~450 - At x=200: ~540 3. **`p1=p2=0.3` (Light Gray Triangles)**: - Starts at (0, 0) with the steepest slope. - Approximate values: - At x=20: ~90 - At x=100: ~600 - At x=200: ~1280 (near the y-axis maximum of 1300) ### Key Observations - The `p1=p2=0.3` series (light gray triangles) exhibits the fastest growth, surpassing all other series by x=200. - The `p1=p2=0.2` series (dark gray squares) initially grows faster than `p1=p2=0.1` but falls below it at x=200, suggesting an anomaly or non-linear behavior. - All series begin at (0, 0), indicating no stored clauses when no clauses are in the formula. ### Interpretation The data suggests a direct proportionality between the number of clauses in the formula and the number stored, with higher `p1=p2` values generally leading to greater storage efficiency. However, the `p1=p2=0.2` series deviates from this trend at higher x-values, potentially indicating: 1. A data collection error or mislabeling in the legend. 2. A non-linear relationship not captured by the linear model. 3. A threshold effect where `p1=p2=0.3` becomes disproportionately effective. The legend’s placement and color coding enhance clarity, but the inconsistency in the `p1=p2=0.2` series warrants further investigation to validate the underlying assumptions or data accuracy. </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/.