- ...zchaff.
^{1} - 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.
^{2} - 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.
^{3} - 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*).^{4} - 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.
^{5} - In this
particular example, it is also possible to backtrack over as
well, although no reason is recorded. The branch point for is
removed from the search, and is set to false by unit propagation. The
advantage of this is that there is now flexibility in either the
choice of value for 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.
^{6} - 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.
^{7} - 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.
^{8} - 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.
^{9} - This idea tends to obviate the need for
use of the pure literal rule, as well. If is a pure literal,
there is no particular reason to hurry to set to true; the key
thing is to avoid setting it to false. But if is pure,
cannot generate any unit propagations, so 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):
^{10} - 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.
^{11} - 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.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ....
^{12} - Chai and Kuehlmann Chai:pb refer to
`poss`as*slack*.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...
instances.
^{13} - 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.
^{14} - There appears to be no effective alternative but to
treat existentially quantified clauses as simple disjunctions, as in
(9).
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ....
^{15} - In interpreting the expression
, the set of clauses and partial assignment 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.
^{16} - 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.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .