...zchaff.¹

The second two papers have been published as technical reports [Dixon, Ginsberg, Luks, ParkesDixon et al.2003b,Dixon, Ginsberg, Hofer, Luks, ParkesDixon et al.2003a] but have not yet been peer reviewed.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... practice.²

Systematic alternatives include the original Davis-Putnam Davis-Putnam method, polynomial calculus solvers [Clegg, Edmonds, ImpagliazzoClegg et al.1996] based on Buchberger's Groebner65,Groebner85 Groebner basis algorithm, methods based on binary decision diagrams or BDDs [BryantBryant1986,BryantBryant1992], and direct first-order methods such as those employed by OTTER [McCune WosMcCune Wos1997]. Nonsystematic methods include the WSAT family [Selman, Kautz, CohenSelman et al.1993], which received a great deal of attention in the 1990's and still appears to be the method of choice for randomly generated problems and some specific other sets of instances. In general, however, systematic algorithms with their roots in DPLL tend to outperform the alternatives.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... solved.³

Problems involving quantified Boolean formulae, or QBF, are PSPACE-complete [Cadoli, Schaerf, Giovanardi, GiovanardiCadoli et al.2002] as opposed to the NP-complete problems considered by DPLL and its direct successors.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...http://www.ece.cmu.edu/~mvelev).⁴

The examples used to generate the graph are those solved by ZCHAFF within 100 seconds using an Intel Pentium 4M running at 1.6GHz. For those not solved within the 100 second limit, an average of 89.4% of the time was spent unit propagating.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... hand.⁵

In this particular example, it is also possible to backtrack over $v_8$ as well, although no reason is recorded. The branch point for $v_8$ is removed from the search, and $v_9$ is set to false by unit propagation. The advantage of this is that there is now flexibility in either the choice of value for $v_8$ or the choice of branch variable itself. This idea is related to Baker's Baker:fancy work on the difficulties associated with some backjumping schemes, and is employed in ZCHAFF [Moskewicz, Madigan, Zhao, Zhang, MalikMoskewicz et al.2001].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... effectively.⁶

Indeed, the final column of our table might better be named ``forgetting'' than ``learning''. Learning (everything) is easy; it's forgetting in a coherent way that's hard.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... point.⁷

Although accepted wisdom, we know of no proof in the literature of this result; Bayardo and Miranker's Bayardo:relsat proof appears to assume that the order in which branch variables are chosen is fixed. We present a general proof in the next paper in this series [Dixon, Ginsberg, Luks, ParkesDixon et al.2003b].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... restriction.⁸

Results such as these necessarily become somewhat suspect as algorithmic methods mature; an unfortunate consequence of the extremely rapid progress in satisfiability engines over recent years is the lack of careful experimental work evaluating the host of new ideas that have been developed.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... subproblem.⁹

This idea tends to obviate the need for use of the pure literal rule, as well. If $p$ is a pure literal, there is no particular reason to hurry to set $p$ to true; the key thing is to avoid setting it to false. But if $p$ is pure, $\neg p$ cannot generate any unit propagations, so $p$ will tend not to be selected as a branch variable. Pure literals can obviously never be set false by unit propagation, so heuristics based on unit propagation counts tend to achieve most of the advantages of the pure literal rule without incurring the associated computational costs.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... implementation):¹⁰

There are other hard problems as well, such as Haken's Haken:mosquito broken mosquito screen problem. The three examples quoted here are sufficient for our purposes.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... setting.¹¹

As we have remarked, our table is designed to reflect the issues involved in lifting DPLL to a more expressive representation. Extending a nonsystematic search technique such as WSAT to a pseudo-Boolean setting has been discussed by Walser Walser:WSATPB and Prestwich Prestwich:pb.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

....¹²

Chai and Kuehlmann Chai:pb refer to poss as slack.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... instances.¹³

Without preprocessing, the two systems perform comparably on this class of problems. As we have stressed, representational extensions are of little use without matching modifications to inference methods.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... finite.¹⁴

There appears to be no effective alternative but to treat existentially quantified clauses as simple disjunctions, as in (9).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

....¹⁵

In interpreting the expression $S_u^s(C,P)$, the set $C$ of clauses and partial assignment $P$ should generally be clear from context. The superscript refers to the number of satisfied literals because satisfied literals are ``super good'' and the subscript refers to the unvalued literals because unvalued literals aren't so good.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... improvements.¹⁶

We know of no effective way to lift the watched literal idea to the QPROP setting. But as we will see when we discuss the ZAP implementation [Dixon, Ginsberg, Hofer, Luks, ParkesDixon et al.2003a], a still broader generalization allows watched literals to return in an elegant and far more general way.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.