Phase Transitions of PP-Complete Satisfiability Problems

1 Introduction and Summary of Results

During the past several years, there has been an intensive investigation of random Boolean satisfiability in probability spaces parametrized by a fixed clauses-to-variables ratio. More precisely, if CZ AL BE is an integer, D2 is a positive integer and D6 is a positive rational such that D6D2 is an integer, then BY CZ B4D2BN D6B5 denotes the space of random CZCNF-formulas with D2 variables DC BD BN BM BM BM BN DC D2 and D6D2 clauses that are generated uniformly and independently by selecting CZ variables without replacement from the D2 variables and then negating each variable with probability BDBPBE. Much of the work in this area is aimed at establishing or at least providing evidence for the conjecture, first articulated by [Chv´atal and Reed, 1992], that a phase transition occurs in the probability D4 CZ B4D2BN D6B5 of a random formula in BY CZ B4D2BN D6B5 being satisfiable, as D2 AX BD. Specifically, this conjecture asserts that, for every CZ AL BE, there is a positive real number D6 CZ such that if D6 BO D6 CZ , then D0CXD1 D2AXBD D4 CZ B4D2BN D6B5 BP BD, whereas if D6 BQ D6 CZ , then D0CXD1 D2AXBD D4 CZ B4D2BN D6B5 BP BCBM

A3 Research of the authors was partially supported by NSF Grants No. CCR-9610257, CCR-9732041, and IIS-9907419

So far, this conjecture has been established only for CZ BP BE by showing that D6 BE BP BD [Chv´atal and Reed, 1992; Fernandez de la Vega, 1992; Goerdt, 1996]. For CZ AL BF, upper and lower bounds for D6 CZ have been obtained analytically and experiments have been carried out that provide evidence for the existence of D6 CZ and estimate its actual value. For CZ BP BF, in particular, it has been proved that BFBMBEBI AK D6 BF AK BGBMBHBLBI [Achlioptas and Sorkin, 2000; Janson et al., 2000] and extensive experiments have suggested that D6 BF AP BGBMBE [Selman et al., 1996]. Moreover, the experiments reveal that the median running time of the DavisPutnam-Logemann-Loveland (DPLL) procedure for satisfiability attains a peak around BGBMBE. Thus, the critical ratio at which the probability of satisfiability undergoes a phase transition coincides with the ratio at which this procedure requires maximum computational effort to decide whether a random formula is satisfiable.

Boolean satisfiability is the prototypical NP-complete problem. Since many reasoning and planning problems in artificial intelligence turn out to be complete for complexity classes beyond NP, in recent years researchers have embarked on an investigation of phase transitions for such problems. For instance, it is known that STRIPS planning is complete for the class PSPACE of all polynomial-space solvable problems [Bylander, 1994]. A probabilistic analysis of STRIPS planning and an experimental comparison of different algorithms for this problem have been carried out in [Bylander, 1996]. In addition to STRIPS planning, researchers have also investigated phase transitions for the prototypical PSPACEcomplete problem QSAT, which is the problem of evaluating a given quantified Boolean formula [Cadoli et al., 1997; Gent and Walsh, 1999]. Actually, this investigation has mainly focused on the restriction of QSAT to random quantified Boolean formulas with two alternations (universalexistential) of quantifiers, a restriction which forms a complete problem for the class A5 BE  at the second level of the polynomial hierarchy PH. The lowest level of PH is NP, while higher levels of this hierarchy consist of all decision problems (or of the complements of all decision problems) computable by nondeterministic polynomial-time Turing machines using oracles from lower levels (see [Papadimitriou, 1994] for additional information on PH and its levels). Another PSPACE-complete problem closely related to QSAT is stochastic Boolean satisfiability SSAT, which is the problem of evaluating an expression consisting of existential and ranodmized quantifiers applied to a Boolean formula. Experimental results on phase transitions for SSAT have been reported in [Littman, 1999] and [Littman et al., 2001].

Between NP and PSPACE lie several other important complexity classes that contain problems of significance in artificial intelligence. Two such classes, closely related to each other and of interest to us here, are #P and PP. The class #P, introduced and first studied by [Valiant, 1979a; 1979b], consists of all functions that count the number of accepting paths of nondeterministic polynomial-time Turing machines. The prototypical #P-complete problem is #SAT, i.e., the problem of counting the number of truth assignments that satisfy a CNF-formula. It is well known that numerous AZ-complete problems arise naturally in logic, algebra, and graph theory [Valiant, 1979a; 1979b]. Moreover, #P-complete problems are encountered in artificial intelligence; these include the problem of computing Dempster's rule for combining evidence [Orponen, 1990] and the problem of computing probabilities in Bayesian belief networks [Roth, 1996]. Recently, researchers have initiated an experimental investigation of extensions of the DPLL procedure for solving #SAT. Specifically, a procedure for solving #SAT, called Counting Davis-Putnam (CDP), was presented and experiments on random 3CNF formulas from the space BY BF B4D2BN D6B5 were carried out in [Birnbaum and Lozinskii, 1999]. The main experimental finding was that the median running time of CDP reaches its peak when D6 AP BDBMBE. A different DPLL extension for solving #SAT, called Decomposing Davis-Putnam (DDP), was presented in [Bayardo and Pehoushek, 2000]; this procedure is based on recursively identifying connected components in the constraint graph associated with a CNFformula. Additional experiments on random 3CNF-formulas from BY BF B4D2BN D6B5 were conducted and it was found out that the median running time of DDP reaches its peak when D6 AP BDBMBH.

In the case of the NP-complete problems CZSAT, CZ AL BF, the peak in the median running time of the DPLL procedure occurs at the critical ratio at which the probability of satisfiability appears to undergo a phase transition. Since #SAT is a counting problem (returning numbers as answers) and not a decision problem (returning "yes" or "no" as answers), it is not meaningful to associate with it a probability of getting a "yes" answer; therefore, it does not seem possible to correlate the peak in the median running times of algorithms for #SAT with a structural phase transition of #SAT. Nonetheless, there exist decision problems that in a certain sense embody the intrinsic computational complexity of #P-complete problems. These are the problems that are complete for the class  of all decision problems solvable using a polynomial-time probabilistic Turing machine, i.e., a polynomial-time nondeterministic Turing machine  that accepts a string DC if and only if at least half of the computations of  on input DC are accepting. The class  was first studied by [Simon, 1975]

and [Gill, 1977], where several problems were shown to be -complete under polynomial-time reductions. In particular, the following decision problem, also called #SAT, is -complete: given a CNF-formula B3 and a positive integer CX, does B3 have at least CX satisfying truth assignments? This problem constitutes the decision version of the counting problem #SAT, which justifies the innocuous overload of notation. Another canonical -complete problem, which is actually a special case of #SAT, is MAJORITY SAT: given a CNF-formula, is it satisfied by at least half of the possible truth assignments to its variables? In addition, several evaluation and testing problems in probabilistic planning under various domain representations have recently been shown to be PP-complete [Littman et al., 1998].

It is known that the class  contains both NP and coNP, and is contained in PSPACE (see [Papadimitriou, 1994]). Moreover, as pointed out by [Angluin, 1980], there is a tight connection between AZ and . Specifically,  AZ BP   , which means that the class of decision problems computable in polynomial time using AZ oracles coincides with the class of decision problems computable in polynomial time using  oracles. This is precisely the sense in which -complete problems embody the same intrinsic computational complexity as AZ-complete problems. Moreover, PP-complete problems (and #P-complete problems) are considered to be substantially harder than NP-complete problems, since in a technical sense they dominate all problems in the polynomial hierarchy PH. Indeed, the main result in [Toda, 1989] asserts that  AI   BP  AZ . In particular, Toda's result implies that no -complete problem lies in , unless  collapses at one of its levels, which is considered to be a highly improbable state of affairs in complexity theory.

In [Littman, 1999], initial experiments were carried out to study the median running time of an extension of the DPLL procedure on instances B4B3BN CXB5 of the PP-complete decision problem #SAT in which B3 was a random 3CNF-formula drawn from BY BF B4D2BN D6D2B5 and CX BP BE D8 , for some nonnegative integer D8 AK D2. These experiments were also reported in [Littman et al., 2001], which additionally contains a discussion on possible phase transitions for the decision problem #SAT and preliminary results concerning coarse upper and lower bounds for the critical ratios at which phase transitions may occur (in these two papers #SAT is called MAJSAT). As noted earlier, the main emphasis of both [Littman, 1999] and [Littman et al., 2001] is not on #SAT or on -complete problems, but on stochastic Boolean satisfiability SSAT, which is a PSPACEcomplete problem containing #SAT as a special case.

In this paper, we embark on a systematic investigation of phase transitions for a large family of -complete satisfiability problems. Specifically, for every integer CZ AL BF and every integer D8 AL BE, let #kSAT(AL BE D2BPD8 ) be the following decision problem: given a CZCNF-formula B3 with D2 variables, does B3 have at least BE D2BPD8 satisfying truth assignments? In particular, for D8 BP BE and for every CZ AL BF, we have the decision problem #kSAT(AL BE D2BPBE ): given a CZCNF-formula, is it satisfied by at least the square-root of the total number of possible truth assignments? Clearly, each problem in this family is a restriction of the decision problem #SAT. Note that, while an instance of #SAT is a pair B4B3BN CXB5, an instance of #kSAT(AL BE D2BPD8 ) is just a CZCNF-formula B3; this makes it possible to study the behavior of random #kSAT(AL BE D2BPD8 ) in the same framework as the one used for random CZSAT. One may also consider the behavior of randomMAJORITY CZSAT, CZ AL BF. In Section 3.2, however, we observe that the asymptotic behavior of randomMAJORITY CZSAT is trivial and that, in particular, it does not undergo any phase transition. In contrast, the state of affairs for random #kSAT(AL BE D2BPD8 ) will turn out to be by far more interesting.

We first show that, for every CZ AL BF and every D8 AL BE, the problem #kSAT(AL BE D2BPD8 ) is indeed -complete. We conjecture that each of these problems undergoes a phase transition at some critical ratio D6 CZBND8 of clauses to variables: as D2 AXBD, for ratios D6 BO D6 CZBND8 , almost all formulas in BY CZ B4D2BN D6B5 are "yes" instances of #kSAT(AL BE D2BPD8 ), whereas for ratios D6 BQ D6 CZBND8 , almost all formulas in BY CZ B4D2BN D6B5 are "no" instances of #kSAT(AL BE D2BPD8 ). As a first step towards this conjecture, we establish analytically upper and lower bounds for D6 CZBND8 . A standard application of Markov's inequality easily yields that B4D8A0BDB5 D8 BD B4CZA0D0CVB4BE CZ A0BDB5B5 is an upper bound for D6 CZBND8 (this was also implicit in [Littman et al., 2001]). Using an elementary argument and the fact that the probability of satisfiability of random 2CNF-formulas undergoes a phase transition at D6 BE BP BD, we show that B4BD A0 BDBPD8B5 is a coarse lower bound for D6 CZBND8 . In particular, these results imply that the critical ratio D6 BFBNBE of #3SAT(AL BE D2BPBE ) obeys the following bounds: BCBMBH AK D6 BFBNBE AK BEBMBHBLBH. After this, we analyze a randomized algorithm, called Extended Unit Clause (EUC), for #3SAT(AL BE D2BPBE ) and show that it almost surely returns a "yes" answer when D6 BO BCBMBLBEBEBJ; therefore, D6 BFBNBE AL BCBMBLBEBEBJ. Although EUC is a simple heuristic, its analysis is rather complex. This analysis is carried out by adopting and extending the powerful methodology of differential equations, first used by [Achlioptas, 2000] to derive improved lower bounds for the critical ratio D6 BF of random 3CNF-formulas.

Finally, we complement these analytical results with a set of experiments for #3SAT(AL BE D2BPBE ) by implementing a modification of the Counting Davis-Putnam procedure (CDP) and running it on formulas drawn from BY BF B4D2BN D6D2B5. Our experimental results suggest that the probability of #3SAT(AL BE D2BPBE ) undergoes a phase transition when D6 AP BEBMBH. Thus, the BEBMBHBLBH upper bound for D6 BFBNBE obtained using Markov's inequality turns out to be remarkably close to the value of D6 BFBNBE suggested by the experiments. Moreover, the average number of recursive calls of the modified CDP procedure reaches a peak around the same critical ratio BEBMBH.

2 PP-completeness of #kSAT(AL BE D2BPD8 )

In Valiant [Valiant, 1979a], the counting problem #SAT was shown to be AZ-complete via parsimonious reductions, i.e., every problem in AZ can be reduced to #SAT via a polynomial-time reduction that preserves the number of solutions. Moreover, the same holds true for the counting versions of many other NP-complete problems, including #CZSAT, the restriction of #SAT to CZCNF-formulas. We now use this fact to identify a large family of -complete problems.

Proposition 2.1: For every integer CZ AL BF and every integer D8 AL BE, the decision problem #kSAT(AL BE D2BPD8 ) is -complete. In particular, #3SAT(AL BE D2BPBE ) is -complete.

Proof: For concreteness, in what follows we show that #3SAT(AL BE D2BPBE ) is -complete. Let be the following problem: given a 3CNF-formula AW and a positive integer CX, does AW have at least BE CX satisfying truth assignments? Since #3SAT is a AZ-complete problem under parsimonious reductions, there is a polynomial-time transformation such that, given a CNF-formula B3 with variables DC BD BN BM BM BM BN DC D2 , it produces a 3CNF-formula AW whose variables include DC BD BN BM BM BM BN DC D2 and has the same number of satisfying truth assignments as B3. Consequently, B3 is a "yes" instance of MAJORITY SAT (i.e., it has at least BE D2A0BD satisfying truth assignments) if and only if B4AWBN D2A0 BDB5 is a "yes" instance of . Consequently, is -complete.

We now show that there is a polynomial-time reduction of to #3SAT(AL BE D2BPBE ). Given a 3CNF-formula AW with variables DC BD BN BM BM BM BN DC D2 and a positive integer CX, we can construct in polynomial time a 3CNF-formula AV with variables DC BD BN BM BM BM BN DC D2 BN DD BD BN BM BM BM BN DD D2 that is tautologically equivalent to the CNF-formula AW CM DD D2A0CXB7BD CM A1 A1 A1 CM DD D2 . It is clear that AZAV BP BE D2A0CX AZAW, where AZAV and AZAW denote the numbers of truth assignments that satisfy AV and AW respectively. Consequently, AW has at least BE CX satisfying truth assignments if and only if AV has at least BE D2 BP BE BED2BPBE satisying truth assignments.

3 Upper and Lower Bounds for #kSAT(AL BE D2BPD8 )

Let CG D2BND6 CZ be the random variable on BY CZ B4D2BN D6B5 such that CG D2BND6 CZ B4B3B5 is the number of truth assignments on DC BD BN BM BM BM BN DC D2 that satisfy B3, where B3 is a random CZCNF-formula in BY CZ B4D2BN D6B5. Thus, B3 is a "yes" instance of #kSAT(AL BE D2BPD8 ) if and only if CG D2BND6 CZ B4B3B5 AL BE D2BPD8 . We now have all the notation in place to formulate the following conjecture for the family of problems #kSAT(AL BE D2BPD8 ), where CZ AL BF and D8 AL BE.

Conjecture 3.1: For every integer CZ AL BF and every integer D8 AL BE, there is a positive real number D6 CZBND8 such that:

• AF If D6 BO D6 CZBND8 , then D0CXD1 D2AXBD D6CJCG D2BND6 CZ AL BE D2BPD8 CL BP BD.
• AF If D6 BQ D6 CZBND8 , then D0CXD1 D2AXBD D6CJCG D2BND6 CZ AL BE D2BPD8 CL BP BC.

We have not been able to settle this conjecture, which appears to be as difficult as the conjecture concerning phase transitions of random CZSAT, CZ AL BF. In what follows, however, we establish certain analytical results that yield upper and lower bounds for the value of D6 CZBND8 ; in particular, these results demonstrate that the asymptotic behavior of random #kSAT(AL BE D2BPD8 ) is non-trivial.

3.1 Upper Bounds for #kSAT(AL BE D2BPD8 )

Let CG be a random variable taking nonnegative values and having finite expectation BXB4CGB5. Markov's inequality is a basic result in probability theory which asserts that if D7 is a positive real number, then D6CJCG AL D7CL AK BXB4CGB5 D7 BM The special case of this inequality with D7 BP BD has been used in the past to obtain a coarse upper bound for the critical ratio D6 CZ in random CZSAT. We now use the full power of Markov's inequality to obtain an upper bound for D6 CZBND8 . As usual, D0CVB4DCB5 denotes the logarithm of DC in base BE.

Proposition 3.2: Let CZ AL BF and D8 AL BE be two integers. For every positive rational number D6 BQ B4D8A0BDB5 D8 BD B4CZA0D0CVB4BE CZ A0BDB5B5 ,

It follows that if D6 CZBND8 exists, then D6 CZBND8 AK B4D8A0BDB5 D8 BD B4CZA0D0CVB4BE CZ A0BDB5B5 . In particular, D6 BFBNBE AK BD BE BD B4BFA0D0CV BJB5 AP BEBMBHBLBHBM

Proof: For every truth assignment AB on the variables DC BD BN BM BM BM BN DC D2 , let
AB be the random variable on BY CZ B4D2BN D6B5 such that
AB B4B3B5 BP BD, if AB satisfies B3, and
AB B4B3B5 BP BC, otherwise. Each
AB is a Bernoulli random variable with mean B4BD A0 BDBPBE CZ B5 D6D2 . Since CG D2BND6 CZ BP A6 AB
AB , the linearity of expectation implies that BXB4CG D2BND6 CZ B5 BP B4BD A0 BDBPBE CZ B5 D6D2 BE D2 . By Markov's inequality, we have that

It follows that if D6 is such that B4BDA0BDBPBE CZ B5 D6 BE B4BDA0BDBPD8B5 BO BD, then D0CXD1 D2AXBD D6CJCG D2BND6 CZ AL BE D2BPD8 CL BP BC. The result then is obtained by taking logarithms in base BE in both sides of the above inequality and solving for D6.

Several remarks are in order now. First, note if CZ is kept fixed while D8 is allowed to vary, then the smallest upper bound is obtained when D8 BP BE. Moreover, the quantity BD B4CZA0D0CVB4BE CZ A0BDB5B5 is the coarse upper bound for the critical ratio D6 CZ for random CZSAT obtained using Markov's inequality. In particular, for random BFSAT this bound is AP BHBMBLBD, which is twice the bound for D6 BFBNBE given by Proposition 3.2.

Let MAJORITY CZSAT be the restriction of MAJORITY SAT to CZCNF-formulas, CZ AL BE. Obviously, a formula B3 in BY CZ B4D2BN D6B5 is a "yes" instance of MAJORITY CZSAT if and only if CG D2BND6 CZ B4B3B5 AL BE D2A0BD . Markov's inequality implies that D6CJCG D2BND6 CZ AL BE D2A0BD CL AK BEB4BD A0 BDBPBE CZ B5 D6D2 , from which it follows that D0CXD1 D2AXBD D6CJCG D2BND6 CZ AL BE D2A0BD CL BP BC, for every CZ AL BE. Thus, for every CZ AL BE, the asymptotic behavior of random MAJORITY CZSAT is trivial; in particular, MAJORITY CZSAT does not undergo any phase transition.

3.2 Lower Bounds for #kSAT(AL BE D2BPD8 )

We say that a partial truth assignment AB covers a clause CR if it satisfies at least one of the literals of CR. We also say that AB covers a CNF-formula B3 with D2 variables if AB covers every clause of B3. Perhaps the simplest sufficient condition for B3 to have at least BE D2BPD8 satisfying truth assignments is to ensure that there is a partial assignment over CQD2A0D2BPD8CR variables covering B3. The next proposition shows that if D6 is small enough, then this sufficient condition is almost surely true for formulas in BY CZ B4D2BN D6B5, as D2 AXBD.

Proposition 3.3: Let CZ AL BF and D8 AL BE be two integers. If BC BO D6 BO BD A0 BDBPD8, then, as D2 AX BD, almost all formulas in BY CZ B4D2BN D6B5 are covered by a partial truth assignment on CQD2 A0 D2BPD8CR variables. Consequently, if BC BO D6 BO BD A0 BDBPD8, then

It follows that if D6 CZBND8 exists, then D6 CZBND8 AL BDA0BDBPD8. In particular, D6 BFBNBE AL BCBMBHBM

Proof: In [Chv´atal and Reed, 1992; Fernandez de la Vega, 1992; Goerdt, 1996]), it was shown that if D6 BO BD, then 2CNFformulas in BY BEBND2BND6 are satisfiable with asymptotic probability BD. Fix a ratio D6 BO BDA0BDBPD8 and consider a random formula B3 in BY CZ B4D2BN D6B5. By removing B4CZ A0 BEB5 literals at random from every clause of B3, we obtain a random 2CNF-formula B3 A3 which is almost surely satisfiable. Let AC be a satisfying truth assignment of B3 A3 and let AB be the partial truth assignment obtained from AC by taking for each clause a literal satisfied by AB. Since D6 BO BDA0BDBPD8, we have that AB is a truth assignment on CQD2A0D2BPD8CR variables that covers B3 A3 ; hence, AB covers B3 as well.

The preceding Propositions 3.2 and 3.3 imply that, unlike MAJORITY CZSAT, for every CZ AL BF and every D8 AL BE, the asymptotic behavior of #kSAT(AL BE D2BPD8 ) is non-trivial.

3.3 An Improved Lower Bound for #3SAT(AL BE D2BPBE )

In what follows, we focus on #3SAT(AL BE D2BPBE ). So far, we have established that if D6 BFBNBE exists, then BCBMBH AK D6 BFBNBE AK BEBMBHBLBH. The main result is an improved lower bound for D6 BFBNBE .

Theorem 3.4: For every positive real number D6 BO BCBMBLBEBEBJ,

It follows that if D6 BFBNBE exists, then D6 BFBNBE AL BCBMBLBEBEBJ.

The remainder of this section is devoted to a discussion of the methodology used and an outline of the proof of this result. We adopt an algorithmic approach, which originated in [Chao and Franco, 1986] and has turned out to be very fruitful in establishing lower bound for the critical ratio D6 BF of random BFSAT (see [Achlioptas, 2001] for an overview). We consider a particular randomized algorithm, called Extended Unit Clause (EUC), that takes as a input a 3CNF-formula B3 on D2 variables and attempts to construct a small partial assignment AB covering all clauses of B3. Algorirthm EUC succeeds if the number of variables assigned by AB is AK CQD2BPBECR, and fails otherwise. Our goal is to show that algorithm EUC succeeds almost surely on formulas B3 from BY BF B4D2BN D6B5 for each D6 BO BCBMBLBEBEBJ. Consequently, D6 BFBNBE AL BCBMBLBEBEBJ.

EUC Algorithm:

For D8 BMBP BD to D2 do

If there are any 1-clauses, (forced step)

pick a 1-clause uniformly at random and satisfy it.

Otherwise, (free step)

pick an unassigned variable uniformly at random and remove all literals involving that variable in all remaining clauses.

Return true if the number of assigned variables is AK CQD2BPBECR;

otherwise, return false.

To analyze the average performance of algorithm EUC we use the differential equations methodology (DEM), initially introduced in [Achlioptas, 2000] and described more extensively in [Achlioptas, 2001]. Due to space limitations, we give only a high-level description of how DEM can be applied to the analysis of algorithm EUC and also outline the steps in the derivation of the improved lower bound BCBMBLBEBEBJ.

Since DEM was developed to analyze satisfiability testing algorithms, it should not be surprising that certain modifications are needed so that it can be applied to counting algorithms, such as EUC. The main component of EUC not handled directly by DEM is the free step, since in a satisfiability context it is always a better strategy to assign a value to the selected variable, instead of removing all the literals involving that variable. We will describe where and how we extend DEM to handle free steps.

Let CE B4D8B5 be the random set of variables remaining at iteration D8 B4BC AK D8 AK D2B5 and let CB CX B4D8B5 denote the set of random CX-clauses B4BD AK CX AK BFB5 remaining at iteration D8. To trace the value of CYCB CX B4D8B5CY, we rely on the assumption that, at every iteration of the execution of the algorithm being considered, a property called uniform randomness is maintained. This property asserts that in every iteration BC AK D8 AK D2, conditional on CYCE B4D8B5CY BP D2 BC and CYCB CX B4D8B5CY BP D1 BC , CB CX B4D8B5 is drawn from BY CX B4D2 BC BND1 BC B5. In [Achlioptas, 2001], a protocol, called card game, is presented; this protocol restricts the possible ways in which a variable can be selected and assigned. It is shown that any algorithmobeying that protocol. satisfies the uniform randomness property. Unfortunately, due to the presence of the free steps, algorithm EUC does not satisfy the card protocol, unlike the majority of algorithms for satisfiability analyzed so far. It is tedious, but straightforward, to show that the natural generalization of the card game in which we allow the elimination of the literals involving the selected variable guarantees the uniform randomness property.

We analyze the algorithm EUC by studying the evolution of the random variables that count the number of clauses in CB CX B4D8B5, BV CX B4D8B5 BP CYCB CX B4D8B5CY. We also need a random variable BYB4D8B5 that counts the number of variables assigned up to iteration D8. We trace the evolution of BV CX B4D8B5 and BYB4D8B5 by using a result in [Wormald, 1995], which states that if a set of random variables CG CY B4D8B5BN BD AK CY AK CZ evolving jointly with D8 such that (1) in each iteration D8, the random variable BGCG CY B4D8B5 BP CG CY B4D8B7BDB5A0CG CY B4D8B5 with high probability (w.h.p.) is very close to its expectation and (2) CG CY B4D8B5 evolves smoothly with D8, then the entire evolution of CG CY B4D8B5 will remain close to its mean path, that is, the path that CG CY B4D8B5 would follow if BGCG CY B4D8B5 was, in each iteration, the value of its expectation. Furthermore, this mean path can be expressed as the set of solutions of a system of differential equations obtained by considering the scaled version of the space-state of the process obtained by dividing every parameter by D2.

As discussed in [Achlioptas, 2001], Wormald's theorem guarantees that the value of the random variables considered differs in D3B4D2B5 from its mean path. This possible deviation produces some difficulties in our analysis; indeed, at each iteration we need to know the value of BV BD B4D8B5 with far more precision, because depending on the exact value taken by BV BD B4D8B5 algorithm EUC performs different operations. To settle this technical difficulty, Achlioptas derived an elegant solution, called the lazy-server lemma. Intutively, this lemma states that the aforementioned difficulty can be overcome if, instead of handling unit clauses deterministically as soon as they appear, at iteration D8 we take care of unit clauses with probability D4 and perform a free step with probability B4BD A0 D4B5, where D4 has to be chosen appropriately.

An additional technical difficulty remains. As discussed in [Achlioptas, 2001], condition (2) of Wormald's theorem does not hold when the iteration D8 is getting close to D2. This second problem is fixed by determining an iteration D8 A3 BP CQB4BD A0 AFB5D2CR at which our algorithm will stop the iterative process and it will deal with the remaining formula in a deterministic fashion. We now modify algorithm EUC by incorporating the features described above and obtain the following algorithm:

EUC with lazy-server policy:

For D8 BMBP BD to D8 A3 do

Set CDB4D8B5 BP BD with probability D4

1. If CDB4D8B5 BP BD
2. If there are BD-clauses,

pick a 1-clause uniformly at random and satisfy it.

b) Otherwise

pick an unset variable uniformly at random and assign it uniformly at random

1. Otherwise

Pick an unset variable uniformly at random and remove all literals with that underlying variable in all remaining clauses.

Find a minimal covering for the remaining clauses.

Return true if the number of assigned variables is CQD2BPBECR; otherwise, return false.

Next, we compute the equation that determine the expected value for the evolution of BV BE B4D8B5, BV BF B4D8B5 and BYB4D8B5, conditional on the history of the random variables considered up to iteration D8. Let B4D8B5 be a random variable representing this history (i.e., B4D8B5 BP CWBVB4BCB5BN BM BM BM BNBVB4D8B5CX, where BVB4D8B5 BP B4BV BE B4D8B5BNBV BF B4D8B5BN BYB4D8B5B5). Since CB CX B4D8B5 distributes as BY CX B4D2 A0 D8BNBV CX B4D8B5B5, the expected number of clauses in BV CX B4D8B5 containing a given literal D0 is equal to CXBV CX B4D8B5BPBEB4D2 A0 D8B5. Using this, we obtain the following system of equations describing the evolution of BV BE B4D8B5, BV BF B4D8B5 and BYB4D8B5.

with initial conditions BV BE B4BCB5 BP BC, BV BF B4BCB5 BP D6D2, BY B4BCB5 BP BC.

It is time to fix the value of D4. According to the lazy-server lemma any value such that

would suffice. This inequality is solved by setting

with AI BQ BC.

To obtain the set of differential equations associated to the process, as discussed in [Achlioptas, 2001], we consider the scaled version of the process, DCBN CR BE B4DCB5BN CR BF B4DCB5BN CUB4DCB5 obtained by dividing every parameter D8BNBV BE B4D8B5BNBV BF B4D8B5BN BYB4D8B5 by D2. We obtain the following differential equations.

with D4B4DCBN CR BE B4DCB5B5 BP B4BD B7 AIB5 BECR BE B4DCB5BPB4BDA0DCB5 BDB7CR BE B4DCB5BPB4BDA0DCB5 and initial conditions CR BF B4BCB5 BP D6, CR BE B4BCB5 BP BC and CUB4BCB5 BP BC. We solve the system numerically using the utility dsolve of mapple (it is easy to get CR BF B4DCB5 BP D6B4BD A0 DCB5 BF analytically) for D6 BP BCBMBLBEBEBJ, AF BP BDBC A0BE and AI BP BDBC A0BH .

Now we are almost done. First, we can see that for every BD AK D8 AK D8A3 w.h.p. CB BC B4D8B5 BP BN by testing numerically that D4B4DCBN CR BE B4DCB5B5 BO BDA0BDBC A0BD if DC BE CJBCBMBMBDA0BDBC A0BE CL and appealing to the lazy-server lemma. Moreover, we get CUB4BD A0 BDBC A0BE B5 BO BCBMBGBLBLBJBK and, transforming this result back to the randomized space-state, we can infer that CUB4D8 A3 B5 BO BCBMBGBLBLBJBKD2B7 D3B4D2B5. Similarly, the number of remaining clauses at that iteration is BV BE B4D8 A3 B5 B7 BV BF B4D8 A3 B5 BP CR BE B4BD A0 BDBC A0BE B5 B7 CR BF B4BD A0 BDBC A0BE B5 B7 D3B4D2B5 BO BCBMBCBCBCBEBDD2B7 D3B4D2B5. It is easy to verify that the ratio of clauses to variables at iteration D8 A3 is smaller than BD, and we can apply again the argument used to obtain the first naive lower bound of BDBPBE to guarantee that there exists a covering partial assignment with size BO BCBMBCBCBCBEBDD2. Thus, by adding the previous quantities, we get BCBMBGBLBLBLBLD2 BO D2BPBE, which means that the algorithm succeeds.

4 Experimental Results for #3SAT(AL BE D2BPBE )

Preliminary experiments were run for random 3CNFformulas with 4, 8, 16 and 32 variables on a SUN Ultra 5 workstation. For each space we generated 1200 random 3CNF-formulas with sizes ranging from 1 to 160 clauses in length. Each clause was generated by randomly selecting 3 variables without replacement and then negating each of them with probability of BDBPBE.

Our goal was to test the formulas for being "yes" instances of #3SAT(AL BE D2BPBE ), i.e., for having at least as many satisfying assignments as the square-root of the total number of truth assignments. For this, we implemented a threshold DPLL algorithm by modifying the basic Counting Davis-Putnam algorithm in [Birnbaum and Lozinskii, 1999] to include tracking of lower and upper bounds on the count and early termination if the threshold is violated by the upper bound or satisfied by the lower bound.

The results are depicted in Figures 1 and 2. In both figures the horizontal axis is the ratio of the number of clauses to number of variables in the space. The ranges of formula sizes represented in the graphs are 1 to 20, 1 to 40, 1 to 80, and 1 to 160 for the 4, 8, 16 and 32 variable spaces respectively.

The phase transition graphs show for each test point the fraction of 1200 newly generated random formulas that had a number of satisfying truth assignments greater than or equal to the square-root of the total number of truth assignments. They strongly suggest that BEBMBH is a critical ratio around which a phase transition occurs. The performance graphs show the average number of recursive calls required to test each formula and they exhibit a peak around the same ratio. In the test runs a range of 1 to 160 clauses was used for each space and the run-times on the SUN Ultra 5 were approximately 10, 15 and 35 minutes for the 4, 8 and 16 variable cases, and 7 hours for the 32 variable case.

After a larger set of experiments is carried out, we plan to apply finite-size scaling to further analyze the phase transition phenomenon exhibited by #3SAT(AL BE D2BPBE ).

We conclude by pointing out that in Section 3.1.4 of [Littman et al., 2001] it was suggested that for every BC AK AB AK BD, the critical ratio of #3SAT(AL BE ABD2 ) is given aproximately by the formula BGBMBEB4BD A0 ABB5. By taking AB BP BDBPBE, this formula suggests that the critical ratio D6 BFBNBE of #3SAT(AL BE D2BPBE ) should be approximately 2.1, which is at odds with our experimental finding of 2.5 as the approximate value of D6 BFBNBE . We stand behind our experimental results; actually, we believe that this discrepancy is not caused by any significant difference in the outcome between the experiments carried out by [Littman et al., 2001] and ours, but rather is due to the way in which the above formula was extrapolated from the experiments in [Littman et al., 2001]. Specifically, in [Littman et al., 2001] experiments were carried out by varying AB and the ratio D6 of clauses to variables, but keeping the number of variables to a fixed value D2 BP BFBC. The above formula BGBMBEB4BD A0 ABB5 was then derived by visual inspection of the resulting surface. We believe that, instead, the value of the critical ratio should be estimated by the crossover points of the curves obtained from experiments for different values of the number D2 of variables. In any case, we see no theoretical argument or experimental evidence that a linear relationship between the critical ratio and AB should hold.

Acknowledgments: We are grateful to Dimitris Achlioptas for stimulating discussions and pointers to his work on lower bounds for 3SAT via differential equations. We also wish to thank Peter Young for generously sharing with us his expertise on phase transition phenomena, and Moshe Y. Vardi for listening to an informal presentation of the results reported here and offering valuable suggestions on an earlier draft of this paper.