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 ## Chart: Logarithmic Plot of Calls vs. Clauses ### Overview The image presents a line chart illustrating 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 probability values. The chart displays three data series, each representing a different configuration of variables and probabilities. ### Components/Axes * **X-axis:** "Number of clauses in the formula", ranging from 0 to 200, with markers at intervals of 20. * **Y-axis:** "log₂ of number of calls", ranging from 0 to 26, with markers at intervals of 2. * **Legend:** Located in the top-right corner, containing the following entries: * Black circle: "50 variables, p1=p2=0.1" * Gray square: "30 variables, p1=p2=0.2" * Black triangle: "20 variables, p1=p2=0.3" ### Detailed Analysis The chart shows three distinct curves, each representing a different set of parameters. * **50 variables, p1=p2=0.1 (Black Circle):** This line exhibits a steep upward slope initially, then gradually flattens out. * At 0 clauses, log₂ of number of calls is approximately 0. * At 20 clauses, log₂ of number of calls is approximately 4. * At 40 clauses, log₂ of number of calls is approximately 8. * At 60 clauses, log₂ of number of calls is approximately 11. * At 80 clauses, log₂ of number of calls is approximately 14. * At 100 clauses, log₂ of number of calls is approximately 17. * At 120 clauses, log₂ of number of calls is approximately 20. * At 140 clauses, log₂ of number of calls is approximately 22. * At 160 clauses, log₂ of number of calls is approximately 23. * At 180 clauses, log₂ of number of calls is approximately 24. * At 200 clauses, log₂ of number of calls is approximately 25. * **30 variables, p1=p2=0.2 (Gray Square):** This line also slopes upward, but less steeply than the previous one. * At 0 clauses, log₂ of number of calls is approximately 0. * At 20 clauses, log₂ of number of calls is approximately 3. * At 40 clauses, log₂ of number of calls is approximately 6. * At 60 clauses, log₂ of number of calls is approximately 9. * At 80 clauses, log₂ of number of calls is approximately 11. * At 100 clauses, log₂ of number of calls is approximately 12. * At 120 clauses, log₂ of number of calls is approximately 13. * At 140 clauses, log₂ of number of calls is approximately 13.5. * At 160 clauses, log₂ of number of calls is approximately 14. * At 180 clauses, log₂ of number of calls is approximately 14.5. * At 200 clauses, log₂ of number of calls is approximately 15. * **20 variables, p1=p2=0.3 (Black Triangle):** This line has the shallowest slope of the three. * At 0 clauses, log₂ of number of calls is approximately 0. * At 20 clauses, log₂ of number of calls is approximately 2. * At 40 clauses, log₂ of number of calls is approximately 4. * At 60 clauses, log₂ of number of calls is approximately 6. * At 80 clauses, log₂ of number of calls is approximately 7. * At 100 clauses, log₂ of number of calls is approximately 8. * At 120 clauses, log₂ of number of calls is approximately 8.5. * At 140 clauses, log₂ of number of calls is approximately 9. * At 160 clauses, log₂ of number of calls is approximately 9.5. * At 180 clauses, log₂ of number of calls is approximately 10. * At 200 clauses, log₂ of number of calls is approximately 10.5. ### Key Observations * The number of calls increases with the number of clauses for all configurations. * The rate of increase in calls is highest for the configuration with 50 variables and p1=p2=0.1. * The rate of increase in calls is lowest for the configuration with 20 variables and p1=p2=0.3. * The curves demonstrate diminishing returns; the increase in calls becomes smaller as the number of clauses increases. ### Interpretation The chart suggests that the number of calls required to solve a formula grows with the number of clauses in the formula. The growth rate is influenced by the number of variables and the probability values (p1 and p2). A higher number of variables and lower probability values lead to a faster increase in the number of calls. This likely reflects the increased complexity of the search space as the number of variables increases and the probability of satisfying a clause decreases. The logarithmic scale on the y-axis indicates that the relationship is likely exponential. The diminishing returns observed in the curves suggest that adding more clauses beyond a certain point yields progressively smaller increases in the number of calls. This could be due to the formula becoming increasingly constrained, or due to the algorithm reaching its limits in exploring the search space. The data provides insights into the computational cost of solving formulas with varying numbers of clauses, variables, and probabilities, which is relevant in areas like constraint satisfaction and automated reasoning. </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 Plot of Calls vs. Clauses ### Overview The image presents a chart illustrating 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 parameter settings. The chart uses three distinct lines to represent different configurations. ### Components/Axes * **X-axis:** "Number of clauses in the formula", ranging from 0 to 200, with markers at 20, 40, 60, 80, 100, 120, 140, 160, 180, and 200. * **Y-axis:** "log₂ of number of calls", ranging from 0 to 20, with markers at 2, 4, 6, 8, 10, 12, 14, 16, and 18. * **Legend:** Located in the bottom-right corner, containing three entries: * "40 variables, p1=0.1 p2=0.2" (represented by a black circle) * "30 variables, p1=0.1 p2=0.3" (represented by a black circle) * "20 variables, p1=0.2 p2=0.3" (represented by a black triangle) ### Detailed Analysis The chart displays three curves, each representing a different set of parameters. * **Line 1 (40 variables, p1=0.1 p2=0.2):** This line (black circles) exhibits a steadily increasing, concave-downward trend. * At 20 clauses: log₂ of number of calls ≈ 2.1 * At 40 clauses: log₂ of number of calls ≈ 4.2 * At 60 clauses: log₂ of number of calls ≈ 6.1 * At 80 clauses: log₂ of number of calls ≈ 7.8 * At 100 clauses: log₂ of number of calls ≈ 9.4 * At 120 clauses: log₂ of number of calls ≈ 10.9 * At 140 clauses: log₂ of number of calls ≈ 12.4 * At 160 clauses: log₂ of number of calls ≈ 13.9 * At 180 clauses: log₂ of number of calls ≈ 15.4 * At 200 clauses: log₂ of number of calls ≈ 16.9 * **Line 2 (30 variables, p1=0.1 p2=0.3):** This line (black circles) also shows an increasing, concave-downward trend, but it consistently lies below Line 1. * At 20 clauses: log₂ of number of calls ≈ 1.6 * At 40 clauses: log₂ of number of calls ≈ 3.5 * At 60 clauses: log₂ of number of calls ≈ 5.2 * At 80 clauses: log₂ of number of calls ≈ 6.8 * At 100 clauses: log₂ of number of calls ≈ 8.3 * At 120 clauses: log₂ of number of calls ≈ 9.7 * At 140 clauses: log₂ of number of calls ≈ 11.1 * At 160 clauses: log₂ of number of calls ≈ 12.5 * At 180 clauses: log₂ of number of calls ≈ 13.9 * At 200 clauses: log₂ of number of calls ≈ 15.2 * **Line 3 (20 variables, p1=0.2 p2=0.3):** This line (black triangles) exhibits the slowest growth, remaining below both Line 1 and Line 2. * At 20 clauses: log₂ of number of calls ≈ 0.9 * At 40 clauses: log₂ of number of calls ≈ 2.5 * At 60 clauses: log₂ of number of calls ≈ 4.1 * At 80 clauses: log₂ of number of calls ≈ 5.6 * At 100 clauses: log₂ of number of calls ≈ 7.1 * At 120 clauses: log₂ of number of calls ≈ 8.5 * At 140 clauses: log₂ of number of calls ≈ 9.9 * At 160 clauses: log₂ of number of calls ≈ 11.3 * At 180 clauses: log₂ of number of calls ≈ 12.6 * At 200 clauses: log₂ of number of calls ≈ 13.9 ### Key Observations * The number of calls increases with the number of clauses for all parameter settings. * Increasing the number of variables (from 20 to 40) leads to a higher number of calls for a given number of clauses. * Increasing p2 (from 0.2 to 0.3) while keeping p1 constant, leads to a lower number of calls for a given number of clauses. * The logarithmic scale on the Y-axis suggests that the relationship between the number of calls and the number of clauses is likely exponential. ### Interpretation The chart demonstrates the computational cost associated with processing formulas with varying numbers of clauses and different parameter settings. The number of variables and the values of parameters p1 and p2 significantly influence the number of calls required. The logarithmic scale indicates that the computational cost grows exponentially with the number of clauses. This suggests that as the complexity of the formula (number of clauses) increases, the computational resources needed to process it grow rapidly. The differences between the lines highlight the importance of parameter tuning and variable management in optimizing performance. The data suggests that reducing the number of variables or adjusting the parameters can help mitigate the exponential growth in computational cost. The chart is likely illustrating the performance of a SAT solver or a similar constraint satisfaction algorithm. </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 \n ## Chart: Log of Number </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: Number of Clauses Stored vs. Number of Clauses in the Formula ### Overview This image presents a line chart illustrating the relationship between the number of clauses in a formula and the number of clauses stored, for three different probability values (p1=p2). The chart displays how the number of stored clauses increases with the number of clauses in the formula, varying based on the specified probability. ### Components/Axes * **X-axis:** "Number of clauses in the formula", ranging from 0 to 200, with increments of 20. * **Y-axis:** "Number of clauses stored", ranging from 0 to 1300, with increments of 100. * **Legend:** Located in the top-right corner, containing three lines with associated labels: * "p1=p2=0.1" (represented by a diamond-shaped marker and a light gray line) * "p1=p2=0.2" (represented by a circle-shaped marker and a black line) * "p1=p2=0.3" (represented by a triangle-shaped marker and a dark gray line) ### Detailed Analysis The chart shows three distinct lines, each representing a different probability value. * **Line 1 (p1=p2=0.1):** This line slopes upward, indicating a positive correlation between the number of clauses in the formula and the number of clauses stored. * At 0 clauses in the formula, approximately 0 clauses are stored. * At 20 clauses in the formula, approximately 20 clauses are stored. * At 40 clauses in the formula, approximately 40 clauses are stored. * At 60 clauses in the formula, approximately 60 clauses are stored. * At 80 clauses in the formula, approximately 80 clauses are stored. * At 100 clauses in the formula, approximately 100 clauses are stored. * At 120 clauses in the formula, approximately 120 clauses are stored. * At 140 clauses in the formula, approximately 140 clauses are stored. * At 160 clauses in the formula, approximately 160 clauses are stored. * At 180 clauses in the formula, approximately 180 clauses are stored. * At 200 clauses in the formula, approximately 200 clauses are stored. * **Line 2 (p1=p2=0.2):** This line also slopes upward, but at a steeper rate than Line 1. * At 0 clauses in the formula, approximately 0 clauses are stored. * At 20 clauses in the formula, approximately 40 clauses are stored. * At 40 clauses in the formula, approximately 80 clauses are stored. * At 60 clauses in the formula, approximately 120 clauses are stored. * At 80 clauses in the formula, approximately 160 clauses are stored. * At 100 clauses in the formula, approximately 200 clauses are stored. * At 120 clauses in the formula, approximately 240 clauses are stored. * At 140 clauses in the formula, approximately 280 clauses are stored. * At 160 clauses in the formula, approximately 320 clauses are stored. * At 180 clauses in the formula, approximately 360 clauses are stored. * At 200 clauses in the formula, approximately 400 clauses are stored. * **Line 3 (p1=p2=0.3):** This line has the steepest upward slope, indicating the strongest positive correlation. * At 0 clauses in the formula, approximately 0 clauses are stored. * At 20 clauses in the formula, approximately 60 clauses are stored. * At 40 clauses in the formula, approximately 120 clauses are stored. * At 60 clauses in the formula, approximately 180 clauses are stored. * At 80 clauses in the formula, approximately 240 clauses are stored. * At 100 clauses in the formula, approximately 300 clauses are stored. * At 120 clauses in the formula, approximately 360 clauses are stored. * At 140 clauses in the formula, approximately 420 clauses are stored. * At 160 clauses in the formula, approximately 480 clauses are stored. * At 180 clauses in the formula, approximately 540 clauses are stored. * At 200 clauses in the formula, approximately 600 clauses are stored. ### Key Observations * The number of clauses stored increases linearly with the number of clauses in the formula for all three probability values. * Higher probability values (p1=p2=0.3) result in a significantly greater number of clauses stored compared to lower probability values (p1=p2=0.1). * The relationship appears to be approximately proportional, but the lines are not perfectly straight, suggesting some non-linear behavior or noise in the data. ### Interpretation The chart demonstrates that the number of clauses stored is directly proportional to the number of clauses in the formula, and this relationship is heavily influenced by the probability values p1 and p2. A higher probability leads to a greater number of clauses being stored for the same number of clauses in the formula. This suggests that the probability values represent a threshold or a weighting factor determining how many clauses are considered significant enough to be stored. The linear trend indicates a consistent storage mechanism, while the differences between the lines highlight the impact of the probability parameter on the storage process. The data suggests that the storage mechanism becomes more aggressive (stores more clauses) as the probability increases. This could be related to a confidence level or a decision-making process where higher probabilities lead to more clauses being retained. </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/.