1: \documentclass{llncs}
2: \usepackage{makeidx} % allows for indexgeneration
3: \usepackage{epsfig}
4: \begin{document}
5:
6: \title{A generating function method for the average-case analysis of DPLL}
7: \author{R\'emi Monasson}
8: \institute{CNRS-Laboratoire de Physique Th{\'e}orique, ENS, Paris, France
9: \\{\bf monasson@lpt.ens.fr}}
10: \maketitle
11:
12: \begin{abstract}
13: A method to calculate the average size of
14: Davis-Putnam-Loveland-Logemann (DPLL) search trees for random
15: computational problems is introduced, and applied to the
16: satisfiability of random CNF formulas (SAT) and the coloring of random
17: graph (COL) problems. We establish recursion relations for the generating
18: functions of the average numbers of (variable or color) assignments at a given
19: height in the search tree, which allow us to derive the asymptotics of
20: the expected DPLL tree size, $2^{\, N \omega + o(N)}$, where $N$ is the
21: instance size. $\omega$ is calculated as a function of the
22: input distribution parameters (ratio of clauses per variable for
23: SAT, average vertex degree for COL), and the branching heuristics.
24: \end{abstract}
25:
26: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
27: \baselineskip=16pt
28:
29: \section{Introduction and main results.}
30:
31: Many efforts have been devoted to the study
32: of the performances of the Davis-Putnam-Loveland-Logemann (DPLL)
33: procedure \cite{Karp}, and more generally,
34: resolution proof complexity for combinatorial problems
35: with randomly generated instances. Two examples
36: are random $k$-Satisfiability ($k$-SAT), where an
37: instance ${\cal F}$ is a uniformly and randomly chosen set of $M=\alpha\, N$
38: disjunctions of $k$ literals built from $N$ Boolean variables and
39: their negations (with no repetition and no complementary literals), and
40: random graph $k$-Coloring ($k$-COL), where an instance ${\cal F}$ is
41: an Erd\H{o}s-R\'enyi random graph from $G(N,p=c/N)$ {\em i.e.} with
42: average vertex degree $c$.
43:
44: Originally, efforts were concentrated on the random width
45: distribution for $k$-SAT, where each literal appear with a fixed probability.
46: Franco, Purdom and collaborators showed that
47: simplified versions of DPLL had polynomial average-case complexity in
48: this case, see \cite{purd2,Fra2} for reviews. It was then recognized that
49: the fixed clause length ensemble might provide harder instances
50: for DPLL \cite{fra0}. Chv\'atal and
51: Szemer\'edi indeed showed that DPLL proof size is w.h.p. exponentially
52: large (in $N$ at fixed ratio $\alpha$) for an unsatisfiable instance
53: \cite{Chv}. Later on, Beame {\em et al.} \cite{Bea} showed that the
54: proof size was w.h.p. bounded from above by $2^{c \, N/\alpha}$ (for
55: some constant $c$), a decreasing function of $\alpha$. As for the
56: satisfiable case, Frieze and Suen showed that backtracking is
57: irrelevant at small enough ratios $\alpha$ ($\le 3.003$ with the
58: Generalized Unit Clause heuristic, to be defined below) \cite{Fri},
59: allowing DPLL to find satisfying assignment in polynomial (linear)
60: time. Achlioptas, Beame and Molloy proved that, conversely, at ratios
61: smaller than the generally accepted satisfiability
62: threshold, DPLL takes w.h.p. exponential time to find a satisfying assignment
63: \cite{Achl3}. Altogether these results provide explanations for the
64: `easy-hard-easy' (or, more precisely, `easy-hard-less hard') pattern
65: of complexity experimentally observed when running DPLL on random
66: 3-SAT instances \cite{Mit}.
67:
68: A precise calculation of the average size of the search space explored by
69: DPLL (and \#DPLL, a version of the procedure solving the enumeration
70: problems \#SAT and \#COL) as a function of the parameters
71: $N$ and $\alpha$ or $c$ is difficult due to the
72: statistical correlations between branches in the search tree resulting
73: from backtracking. Heuristic derivations were
74: nevertheless proposed by Cocco and Monasson based on a `dynamic annealing'
75: assumption \cite{Coc,Coc2,Eindor}. Hereafter, using the linearity of
76: expectation, we show that `dynamic annealing' turns not to be an
77: assumption at all when the expected tree size is concerned.
78:
79: We first illustrate the approach, based on the use of recurrence relations
80: for the generating functions of the number of nodes at a given height in
81: the tree, on the random $k$-SAT problem and
82: the simple Unit Clause (UC) branching heuristic where unset variables
83: are chosen uniformly
84: at random and assigned to True or False uniformly at random
85: \cite{fra2,Fra}. Consider the following counting
86: algorithm
87: \vskip .3cm \noindent
88: {\small Procedure \#DPLL-UC[${\cal F}$,A,S]
89:
90: \noindent Call ${\cal F}_A$ what is left from instance ${\cal F}$ given
91: partial variable assignment $A$;
92:
93: 1. If ${\cal F}_A$ is empty, $S\to S+ 2^{N-|A|}$, Return;
94: {\em (Solution Leaf)}
95:
96: 2. If there is an empty clause in ${\cal F}_A$, Return;
97: {\em (Contradiction Leaf)}
98:
99: 3. If there is no empty clause in ${\cal F}_A$,
100: let $\Gamma _1=\{$1-clauses$\ \in {\cal F}_A\}$,
101:
102: \hskip .6cm if $\Gamma _1 \ne \emptyset$, pick any 1-clause, say, $\ell$,
103: and call DPLL[${\cal F}$,A$\cup \ell$]; {\em (unit-propagation)}
104:
105: \hskip .6cm if $\Gamma_1=\emptyset$, pick up an unset
106: literal uniformly at random, say, $\ell$, and call
107:
108: \hskip 2.1cm DPLL[${\cal F}$,A$\cup \ell$], then
109: DPLL[${\cal F}$,A$\cup \bar \ell$] ; {\em (variable splitting)}
110:
111: \noindent End;}
112:
113: \noindent
114: \#DPLL-UC, called with $A=\emptyset$ and $S=0$, returns the number $S$
115: of solutions of the instance ${\cal F}$; the history of the search
116: can be summarized as a search tree with leaves marked with solution or
117: contradiction labels. As the instance to be treated and the sequence
118: of operations done by \#DPLL-UC are stochastic, so are
119: the numbers $L_S$ and $L_C$ of solution and contradiction leaves respectively.
120:
121: \begin{theorem}
122: {Let $k\ge 3$ and
123: $\displaystyle{
124: \Omega (t,\alpha,k) = t + \alpha \; \log_2 \big(1
125: - \frac {k}{2^k} t^{k-1} +\frac{k-1}{2^k} {t^k} \big)}$.
126: The expectations of the
127: numbers of solution and contradiction leaves in the
128: \#DPLL-UC search tree of random $k$-SAT instances with $N$ variables
129: and $\alpha N$ clauses are, respectively,
130: $\displaystyle{
131: L_S(N,\alpha,k)=2^{N \omega _S(\alpha,k) +o(N)}}$ with
132: $\omega _S(\alpha,k)= \Omega (1,\alpha,k)$ and
133: $\displaystyle{
134: L_C(N,\alpha,k)=2^{N \omega _C (\alpha ,k) +o(N)} \ \ with \ \
135: \omega _C(\alpha,k)=\max _{t\in [0;1]}\Omega (t,\alpha,k)
136: }$.}
137: \end{theorem}
138: \noindent
139: An immediate consequence of Theorem 1 is that
140: the expectation value of the total number of leaves, $L_S+L_C$, is
141: $2^{N \omega _C (\alpha ,k) +o(N)}$. This result was
142: first found by M\'ejean, Morel and Reynaud in the particular case $k= 3$
143: and for ratios
144: $\alpha > 1$ \cite{mejean}. Our approach not only provides a much
145: shorter proof, but can also be easily extended to other
146: problems and more sophisticated heuristics, see Theorems 2 and 3 below.
147: In addition, Theorem 1 provides us with some information about the expected
148: search tree size of the decision procedure DPLL-UC,
149: corresponding to \#DPLL-UC with Line 1 replaced with:
150: {\small If ${\cal F}_A$ is empty, output Satisfiable; Halt}.
151: \begin{corollary}
152: {Let $\alpha > \alpha _u(k)$, the root
153: of $\omega _C (\alpha,k) = 2+ \alpha \log _2(1-2^{-k})$ e.g.
154: $\alpha _u (3)= 10.1286...$. The average size of
155: DPLL-UC search trees for random $k$-SAT instances
156: with $N$ variables and $\alpha N$ clauses equals $2^{N \omega _C(\alpha,k)
157: +o(N)}$.}
158: \end{corollary}
159:
160: \noindent
161: Functions $\omega_S,\omega_C$ are shown in Figure 1 in the $k=3$ case. They
162: coincide and are equal to $1 - \alpha
163: \log_2 (8/7)$ for $\alpha < \alpha ^* = 4.56429...$, while
164: $\omega_C > \omega_S$ for $\alpha > \alpha ^*$. In other words, for
165: $\alpha >\alpha^*$, most leaves in \#DPLL-UC trees are contradiction
166: leaves, while for $\alpha < \alpha ^*$, both contradiction and
167: solution leaf numbers are (to exponential order in $N$) of the same
168: order. As for DPLL-UC trees, notice that
169: $\displaystyle{
170: \omega _C(\alpha,k) \asymp \frac{2 \ln 2}{3 \,\alpha} =
171: \frac{0.46209...}\alpha
172: }$.
173: This behaviour agrees with
174: Beame et al.'s result ($\Theta (1/\alpha)$) for the average resolution
175: proof complexity of unsatisfiable instances \cite{Bea}.
176: Corollary 1 shows that the expected DPLL tree size can be estimated
177: for a whole range of $\alpha$; we conjecture that the above expression
178: holds for ratios smaller than $\alpha _u$ {\em i.e.}
179: down to $\alpha ^*$ roughly. For generic $k\ge 3$,
180: we have $\displaystyle{
181: \omega _C(\alpha,k) \asymp \frac{k-2}{k-1} \bigg(
182: \frac{2^k \ln 2}{k (k-1) \, \alpha} \bigg) ^{1/(k-2)}}$; the decrease
183: of $\omega_C$ with $\alpha$ is therefore slower and slower as $k$ increases.
184:
185: \begin{figure}[h]
186: \begin{center}
187: \epsfig{file=omega.eps,angle=-90,width=8cm}
188: \end{center}
189: \caption{Logarithms of the average numbers of solution and
190: contradiction leaves, respectively $\omega _S$ and $\omega_C$, in
191: \#DPLL-UC search trees versus ratio $\alpha$ of
192: clauses per variable for random 3-SAT.
193: Notice that $\omega_C$ coincides with the
194: logarithm of the expected size of \#DPLL-UC at all ratios $\alpha$, and
195: with the one of DPLL-UC search trees for $\alpha \ge 10.1286...$.}
196: \label{figomega}
197: \end{figure}
198:
199: So far, no expression for $\omega$ has been obtained for more sophisticated
200: heuristics than UC. We consider
201: the Generalized Unit Clause (GUC) heuristic \cite{Fra,Achl}
202: where the shortest clauses are preferentially satisfied. The associated
203: decision procedure, DPLL-GUC, corresponds to DPLL-UC with Line 3 replaced with:
204: {\small Pick a clause uniformly at random among the shortest clauses,
205: and a literal, say, $\ell$, in the clause; call
206: DPLL[${\cal F}$,A$\cup \ell$], then DPLL[${\cal F}$,A$\cup \bar \ell$].}
207: \begin{theorem}
208: Define
209: $m(x_2) = \frac 12 \big(1 + \sqrt{1+4x_2}) -2 x_2$,
210: $y_3(y_2)$ the solution of the ordinary differential equation
211: ${dy_3}/{dy_2} = 3(1+y_2-2 \;y_3)/(2m(y_2))$
212: such that $y_3(1)=1$, and
213: \begin{equation} \nonumber \label{refiuy}
214: \omega ^g (\alpha) = \max _{\frac 34 < y_2 \le 1} \bigg[
215: \int _{y_2}^1 \frac {dz}{m(z)} \log _2 \big(2z +m(z)\big)\
216: \exp \left( - \int _{z}^1 \frac {dw}{m(w)}\right)
217: + \alpha \log _2 y_3 (y_2) \bigg] \quad .
218: \end{equation}
219: Let $\alpha > \alpha ^g _u = 10.2183...$, the root
220: of $\omega ^g (\alpha) + \alpha \log _2(8/7) =2$.
221: The expected size of DPLL-GUC search tree for random 3-SAT instances
222: with $N$ variables and $\alpha N$ clauses is $2^{N\,\omega ^g (\alpha) +
223: o(N)}$.
224: \end{theorem}
225:
226: \noindent
227: Notice that, at large $\alpha$,
228: $\displaystyle{
229: \omega ^g (\alpha ) \asymp
230: \frac{3+\sqrt{5}}{6\,\ln 2}\big[ \ln \big( \frac{1+\sqrt{5}}{2} \big)
231: \big]^2 \frac 1\alpha = \frac {0.29154...}\alpha
232: }$
233: in agreement with the $1/\alpha$ scaling established in \cite{Bea}.
234: Furthermore, the multiplicative factor is smaller than the one for
235: UC, showing that DPLL-GUC is more efficient than DPLL-UC in
236: proving unsatisfiability.
237: \vskip .3cm
238: A third application is the analysis of the counterpart of GUC for the
239: random 3-COL problem. The version of DPLL we have analyzed operates as
240: follows \cite{mol}.
241: Initially, each vertex is assigned a list of 3 available colors.
242: In the course of the procedure, a vertex, say, $v$, with
243: the smallest number of available colors, say, $j$, is chosen at random
244: and uniformly. DPLL-GUC then removes $v$, and successively branches to the
245: $j$ color
246: assignments corresponding to removal of one of the $j$ colors of $v$ from the
247: lists of the neighbors of $v$. The procedure backtracks when a vertex
248: with no color left is created ({contradiction}), or no vertex
249: is left (a {proper coloring} is found).
250: \begin{theorem}
251: Define
252: $\displaystyle{
253: \omega ^h (c) = \max _{0 < t < 1} \big[
254: \frac c6 t^2 - \frac c3 t - (1-t) \ln 2 + \ln \big( 3 -e^{-2 c\,t / 3}
255: \big) \big]
256: }$.
257:
258: \noindent
259: Let $c > c ^h _u = 13.1538...$, the root
260: of $\omega ^h (c) + \frac c6 = 2 \ln 3$.
261: The expected size of DPLL-GUC search tree for deciding 3-COL on random
262: graphs from $G(N,c/N)$ with $N$ vertices is $e^{\,N\,\omega ^h (c) +
263: o(N)}$.
264: \end{theorem}
265:
266: \noindent
267: Asymptotically, $\displaystyle{
268: \omega ^h (c ) \asymp
269: \frac{3\, \ln 2}{2\, c^2}= \frac {1.0397...}{c^2}
270: }$
271: in agreement with Beame et al.'s scaling ($\Theta (1/c^2)$) \cite{Cris}.
272: An extension of Theorem 3 to higher values of the number $k$ of
273: colors gives
274: $\displaystyle{ \omega^h(c,k) \asymp
275: \frac{k(k-2)}{k-1} \; \big[ \frac{2\, \ln 2}{k-1}
276: \big] ^{1/(k-2)} c^{-(k-1)/(k-2)}}$. This result is compatible with
277: the bounds derived in \cite{Cris}, and suggests that the
278: $\Theta( c ^{-(k-1)/(k-2)})$ dependence
279: could hold w.h.p. (and not only
280: in expectation).
281:
282:
283: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
284:
285: \section{Recurrence equation for \#DPLL-UC search tree}
286:
287: Let ${\cal F}$ be an instance of the 3-SAT problem defined over a set of
288: $N$ Boolean variables $X$. A partial assignment $A$
289: of length $T (\le N)$ is the specification of the truth values of $T$
290: variables in $X$. We denote by ${\cal F}_A$ the residual instance
291: given $A$. A clause $c\in {\cal F}_A$ is said to be a $\ell$-clause
292: with $\ell \in\{0,1,2,3\}$ if the number of false literals
293: in $c$ is equal to $3-\ell$. We denote by $C _\ell({\cal F}_A)$
294: the number of $\ell$-clauses in ${\cal F}_A$.
295: The instance ${\cal F}$ is said to be satisfied under $A$ if
296: $C_\ell ({\cal F}_A)=0$ for $\ell=0,1,2,3$, unsatisfied (or violated)
297: under $A$ if $C_0({\cal F}_A) \ge 1$, undetermined under $A$ otherwise.
298: The clause vector of an undetermined or satisfied residual instance
299: ${\cal F}_A$ is the three-dimensional vector $\vec C$ with components
300: $C_1({\cal F}_A),C_2({\cal F}_A),C_3({\cal F}_A)$.
301: The search tree associated to an instance ${\cal F}$
302: and a run of \#DPLL is the tree whose nodes carry the residual assignments
303: $A$ considered in the course of the search.
304: The height $T$ of a node is the length of the attached assignment.
305:
306: \vskip .3cm
307:
308: It was shown by Chao and Franco \cite{fra2,Fra}
309: that, during the first descent in the search tree {\em i.e.} prior to any
310: backtracking, the distribution of residual instances remains uniformly
311: random conditioned on the numbers of $\ell$-clauses. This statement remains
312: correct for heuristics more sophisticated than UC {\em e.g.}
313: GUC, SC$_1$ \cite{Fra,Achl}, and was recently extended to splitting
314: heuristics based on variable occurrences by Kaporis, Kirousis and
315: Lalas \cite{Kap}. Clearly, in this context, uniformity is lost after
316: backtracking enters into play (with the exception of Suen and Frieze's
317: analysis of a limited version of backtracking \cite{Fri}).
318: Though this limitation appears to forbid (and has forbidden so far)
319: the extension of average-case studies of backtrack-free DPLL to full DPLL
320: with backtracking, we point out here that it is not as severe as it
321: looks. Indeed, let us forget about how \#DPLL or DPLL search tree is built and
322: consider its final state. We refer to a
323: branch (of the search tree) as the shortest path from the root node
324: (empty assignment) to a leaf. The two key remarks underlying the
325: present work can be informally stated as follows.
326: First, the expected size of a \#DPLL search tree can be calculated from the
327: knolwedge of the statistical distribution of (residual instances on)
328: a single branch; no characterization of the
329: correlations between distinct branches in the tree is necessary.
330: Secondly, the statistical distribution of (residual instances on) a single
331: branch is simple since, along a branch, uniformity is
332: preserved (as in the absence of backtracking).
333: More precisely,
334: \begin{lemma}
335: [from Chao \& Franco \cite{fra2}]
336: { Let ${\cal F}_A$ be a residual instance attached
337: to a node $A$ at height $T$ in a \#DPLL-UC search tree
338: produced from an instance ${\cal F}$ drawn from the random 3-SAT distribution.
339: Then the set of $\ell$-clauses in ${\cal F}_A$ is
340: uniformly random conditioned on its size $C_\ell({\cal F}_A)$
341: and the number $N-T$ of unassigned variables for each $\ell \in\{0,1,2,3\}$.}
342: \end{lemma}
343: \begin{proof}
344: the above Lemma is an immediate application
345: of Lemma 3 in Achlioptas' Card Game framework which establishes
346: uniformity for algorithms ({\em a}) `pointing to a particular card (clause)',
347: or ({\em b}) 'naming a variable that has not yet been assigned a value'
348: (Section 2.1 in Ref. \cite{Achl}).
349: The operation of \#DPLL-UC along a branch precisely amounts to
350: these two operations: unit-propagation relies on action ({\em a}), and
351: variable splitting on ({\em b}). \qed
352: \end{proof}
353: Lemma 1 does not address the question of uniformity among
354: different branches. Residual instances attached to two (or more)
355: nodes on distinct branches in the search tree are correlated.
356: However, these correlations can be
357: safely ignored in calculating the average number of residual instances,
358: in much the same way as the average
359: value of the sum of correlated random variables is simply the sum of
360: their average values.
361: \begin{proposition}
362: {Let $L ( \vec C , T)$ be the
363: expectation of the number of undetermined residual instances with clause
364: vector $\vec C$ at height $T$ in \#DPLL-UC search tree, and
365: $\displaystyle{
366: G (x_1,x_2,x_3;T\,) =\sum_{\vec C}\; x_1 ^{\, C_1}\; x_2 ^{\, C_2}\;
367: x_3 ^{\, C_3}\ L(\,{\vec C}\,,T\,)
368: }$
369: its generating function. Then, for $0\le T <N$,
370: \vskip -.4cm
371: \begin{eqnarray}
372: \label{eqev}
373: G(x_1,x_2,x_3;T+1\,)&=& \frac 1{f_1}\; G \big( f_1,f_2,f_3;
374: T\,\big) + \bigg( 2 - \frac 1{f_1} \bigg) \; G\big( 0, f_2,f_3; T\, \big)
375: \nonumber \\
376: &-& 2 \; G(0,0,0;T)
377: \end{eqnarray}
378: where $f_1,f_2,f_3$ stand for the functions
379: $f_1 ^{(T)} (x_1)=x_1+ \frac 12 \mu (1 -2 x_1)$,
380: $f_2 ^{(T)} (x_1,x_2)=x_2+ \mu ( x_1+1 -2x_2)$,
381: $f_3 ^{(T)}(x_2,x_3)=x_3+\frac32 \mu ( x_2+1 -2x_3)$,
382: and $\mu =1/(N-T)$. The generating function
383: $G$ is entirely defined from recurrence relation (\ref{eqev})
384: and the initial condition $G(x_1,x_2,x_3 ; 0) =\big( x_3 \big)^{\alpha N}$.}
385: \end{proposition}
386: \begin{proof} Let $\delta _n$ denote the Kronecker function
387: ($\delta _n=1$ if $n=0$, $\delta _n=0$ otherwise),
388: $B _n ^{m,q}={m \choose n} q^n(1-q)^{m-n}$ the
389: binomial distribution. Let $A$ be a node
390: at height $T$, and ${\cal F}_A$ the attached residual instance.
391: Call $\vec C$ the clause vector of ${\cal F}_A$. Assume first that
392: $C_1\ge 1$. Pick up one 1-clause, say, $\ell$. Call $z_j$
393: the number of $j$-clauses that contain $\bar \ell$ or $\ell$
394: (for $j=1,2,3$). From Lemma 1, the $z_{j}$'s are
395: binomial variables with parameter $j/(N-T)$ among $C_j-\delta _{j-1}$
396: (the 1-clause that is satisfied through unit-propagation is removed).
397: Among the $z_j$ clauses, $w_{j-1}$ contained $\bar \ell$ and are
398: reduced to $(j-1)$-clauses, while the remaining $z_j-w_{j-1}$ contained
399: $\ell$ and are satisfied and removed. From Lemma 1 again, $w_{j-1}$ is
400: a binomial variable with parameter $1/2$ among $z_j$.
401: The probability that the instance produced has no
402: empty clause ($w_0=0$) is $B_0^{z_1,\frac 12}=2^{-z_1}$. Thus, setting
403: $\mu = \frac 1{N-T}$,
404: \begin{eqnarray}
405: \label{bbra2}
406: M _{P} && [\vec C',\vec C; T] =
407: \sum _{z_3=0} ^{C_3} B_{z_3}^{ C_3,3\mu} \sum _{w_2=0}^{z_3}
408: B_{w_2}^{z_3,\frac 12} \sum_{z_2=0}^{C_2} B_{z_2}^{ C_2,2\mu}
409: \sum _{w_1=0}^{z_2} B_{w_1}^{z_2,\frac 12} \nonumber \\ &&
410: \times\ \sum _{z_1=0}^{C_1-1} B_{z_1}^{C_1-1,\mu}
411: \frac 1{2^{z_1}} \, \delta _{C'_3 - (C_3 - z_3)}
412: \delta _{C'_2- (C_2 -z_2+w_2)} \delta _{C' _1- (C_1-1 -z_1+w_1)} \nonumber
413: \end{eqnarray}
414: expresses the probability that a residual instance at height $T$ with
415: clause vector $\vec C$ gives rise to a (non-violated) residual instance
416: with clause vector $\vec C'$ at height $T+1$ through unit-propagation.
417: Assume now $C_1=0$. Then, a
418: yet unset variable is chosen and set to True or False uniformly at
419: random. The calculation of the new vector $\vec C'$ is identical
420: to the unit-propagation case above, except that: $z_1=w_0=0$ (absence
421: of 1-clauses), and two nodes are produced (instead of one).
422: Hence,
423: \begin{eqnarray}
424: M _{UC} [\vec C',\vec C; T] &=& 2\sum _{z_3=0} ^{C_3} B_{z_3}^{ C_3,3\mu}
425: \sum _{w_2=0}^{z_3} B_{w_2} ^{z_3,\frac 12}
426: \sum_{z_2=0}^{C_2} B_{z_2}^{ C_2,2\mu}
427: \sum _{w_1=0}^{z_2} B_{w_1}^{z_2,\frac 12} \nonumber \\
428: &&\times\ \delta _{C'_3 - (C_3 - z_3)} \delta _{C'_2- (C_2 -z_2+w_2)}
429: \delta _{C' _1- w_1 } \nonumber
430: \end{eqnarray}
431: expresses the expected number of residual instances at height $T+1$
432: and with clause vector $\vec C'$ produced from a residual instance at
433: height $T$ and with clause vector $\vec C$ through UC branching.
434:
435: Now, consider all the nodes $A_i$ at height $T$, with $i=1,
436: \ldots, {\cal L}$. Let $o_i$ be the operation done by \#DPLL-UC
437: on $A_i$. $o_i$ represents either unit-propagation (literal $\ell_i$
438: set to True) or variable splitting (literals $\ell _i$ set to T and F
439: on the descendent nodes respectively).
440: Denoting by $\mathbf{E}_{Y}(X)$ the
441: expectation value of a quantity $X$ over variable $Y$,
442: $\displaystyle{
443: L(\vec C';T+1) = \mathbf{E}_{{\cal L}, \{A_i, o_i\}} \left(
444: \sum _{i=1}^{\cal L} {\cal M} [\vec C' ; A_i,o_i ] \right)
445: }$
446: where ${\cal M}$ is the number (0, 1 or 2) of
447: residual instances with clause vector $\vec C'$ produced from $A_i$
448: after \#DPLL-UC has carried out operation $o_i$.
449: Using the linearity of expectation,
450: $\displaystyle{
451: L(\vec C';T+1) = \mathbf{E}_{{\cal L}} \left(\sum _{i=1}^{\cal L}
452: \mathbf{E}_{\{A_i, o_i\}} \big( {\cal M} [\vec C' ; A_i,o_i ] \big)\right)
453: = \mathbf{E}_{{\cal L}} \left( \sum _{i=1}^{\cal L}
454: M[\vec C',\vec C_i; T]
455: \right)}
456: $
457:
458: \noindent
459: where $\vec C_i$ is the clause vector of the residual
460: instance attached to $A_i$, and
461: $M[\vec C',\vec C; T] = \big( 1-\delta_{C_1} \big)
462: \, M _{P} [\vec C',\vec C; T]
463: + \delta _{C_1}\, M_{UC} [\vec C',\vec C; T]$.
464: Gathering assignments with identical clause vectors gives the
465: reccurence relation
466: $L ( \vec C' , T+1) =$
467: $\displaystyle{\sum_{\vec C} M [\vec C',\vec C; T]
468: \ L ( \vec C , T)}$.
469: Recurrence relation (\ref{eqev}) for the generating function is an immediate
470: consequence. The initial condition over $G$ stems from the fact that
471: the instance is originally drawn from the random 3-SAT distribution,
472: $L(\vec C;0)=\delta _{C_1}\, \delta _{C_2}\, \delta_{C_3-\alpha N}$.\qed
473: \end{proof}
474:
475: \section{Asymptotic analysis and application to DPLL-UC}
476:
477: The asymptotic analysis of $G$ relies on the
478: following technical lemma:
479: \begin{lemma}
480: {Let $\gamma (x_2,x_3,t) = (1-t)^3 x_3
481: + \frac {3t}2 (1-t)^2 x_2+ \frac t8 (12-3t-2t^2)$, with
482: $t\in]0;1[$ and $x_2,x_3>0$. Define
483: $\displaystyle{S_0(T) \equiv \sum _{H=0}^{T} 2^{T-H} \, G(0,0,0;H)}$.
484: Then, in the large $N$ limit,
485: $\displaystyle{
486: S_0([tN]) \le 2^{N (t + \alpha \log _2 \gamma(0,0,t)) +
487: o(N)}}$ and $G \big(\frac 12,x _2,x_3;[tN]\big) =
488: \displaystyle{2^{N(t + \alpha \log _2 \gamma(x_2,x_3,t)) + o(N)}}$.}
489: \end{lemma}
490: Due to space limitations, we give here only some elements of the
491: proof.
492: The first step in the proof is inspired
493: by Knuth's kernel method \cite{knu}: when $x_1=\frac 12$, $f_1=\frac 12$ and
494: recurrence relation (\ref{eqev}) simplifies and is easier to handle. Iterating
495: this equation then allows us to relate the value of $G$ at height $T$ and
496: coordinates $(\frac 12, x_2,x_3)$ to the (known) value of $G$ at height 0
497: and coordinates $(\frac 12,y_2,y_3)$ which are functions of $x_2,x_3, T,N$,
498: and $\alpha$. The function $\gamma$ is the value of $y_3$ when $T,N$
499: are sent to infinity at fixed ratio $t$. The asymptotic statement
500: about $S_0(T)$ comes from the previous result and the fact that the
501: dominant terms in the sum defining $S_0$ are the ones
502: with $H$ close to $T$.
503:
504: \begin{proposition}
505: {Let $L_C(N,T,\alpha)$ be the expected number of contradiction leaves
506: of height $T$ in the \#DPLL-UC resolution tree of random 3-SAT instances
507: with $N$ variables and $\alpha N$ clauses, and $\epsilon >0$.
508: Then, for $t\in [\epsilon; 1-\epsilon]$ and $\alpha >0$,
509: $\displaystyle{
510: \Omega (t,\alpha,3) \le
511: \frac 1N \log _2 L_C(N,[tN],\alpha) +o(1) \le \max _{h\in[\epsilon, ;t]}
512: \Omega (h,\alpha,3)
513: }$
514: where $\Omega$ is defined in Theorem 1.
515: }
516: \end{proposition}
517: \noindent
518: Observe that a contradiction may appear with a positive (and
519: non--exponentially small in $N$) probability as soon as two 1-clauses are
520: present. These 1-clauses will be present as a result of 2-clause
521: reduction when the residual instances include a large number ($\Theta (N)$)
522: of 2-clauses. As this is the case for a finite fraction of residual
523: instances, $G(1,1,1;T)$ is not exponentially larger than $L_C(T)$. Use of
524: the monotonicity of $G$ with respect to $x_1$ and Lemma 2 gives the announced
525: lower bound (recognize that $\Omega (t,\alpha,3)=t + \alpha \log _2
526: \gamma (1,1;t)$). To derive the upper bound, remark that
527: contradictions leaves cannot be more numerous
528: than the number of branches created through splittings; hence $L_C(T)$
529: is bounded from above by the number of splittings at
530: smaller heights $H$, that is, $\displaystyle{\sum _{H < T}} G(0,1,1;H)$.
531: Once more, we use the monotonicity of $G$ with respect to $x_1$ and
532: Lemma 2 to obtain the upper bound.
533: The complete proof will be given in the full version.
534:
535: \begin{proof} {\em (Theorem 1)}
536: By definition, a solution leaf is a node in the search tree
537: where no clauses are left; the average number $L_S$ of solution leaves
538: is thus given by
539: $\displaystyle{
540: L_S = \sum _{H=0}^N L(0,0,0;H) = \sum _{H=0}^N G(\vec 0;H)
541: }$. A straightforward albeit useful upper bound on $L_S$ is obtained from
542: $L_S \le S_0(N)$.
543: By definition of the algorithm \#DPLL, $S_0 (N)$ is
544: the average number of solutions of an instance with $\alpha N$ clauses
545: over $N$ variables drawn from the random 3-SAT distribution,
546: $S_0 (N) = 2^N \,(7/8) ^{\alpha N}$ \cite{fra0}.
547: This upper bound is indeed tight (to within terms that are
548: subexponential in $N$),
549: as most solution leaves have heights equal, or close to $N$. To show this,
550: consider $\epsilon >0$, and write
551: $$
552: L_S \ge \sum _{H=N(1-\epsilon)}^N G(\vec 0;H)
553: \ge 2^{-N \epsilon} \; \sum _{H=N(1-\epsilon)}^N 2^{N-H} G(\vec 0;H)
554: = 2^{-N \epsilon} \; S_0(N) \; \big[ 1 - A\big]
555: $$
556: with $A = 2^{N\epsilon} S_0(N(1-\epsilon))/S_0(N)$. From
557: Lemma 2, $A\le (\kappa +o(1))^{\alpha N}$ with
558: $\displaystyle{
559: \kappa = \frac{\gamma(0,0,1-\epsilon)}{7/8} = 1 - \frac 97 \, \epsilon^2
560: + \frac 27 \, \epsilon ^3 <1
561: }$
562: for small enough $\epsilon$ (but $\Theta(1)$ with respect to $N$).
563: We conclude that $A$ is exponential small in $N$, and
564: $
565: -\epsilon + 1 - \alpha \log_2 \frac 87 + o(1)
566: \le \frac 1N \log_2 L_S \le 1 - \alpha \log_2 \frac 87
567: $.
568: Choosing arbitrarily small $\epsilon$ allows us to
569: establish the statement about the asymptotic behaviour of
570: $L_S$ in Theorem~1.
571:
572:
573: Proposition 2, with arbitrarily small $\epsilon$, immediately
574: leads to Theorem 1 for $k=3$,
575: for the average number of contradiction leaves, $L_C$, equals
576: the sum over all heights $T=tN$ (with $0\le t\le 1$) of $L_C(N,T,\alpha)$,
577: and the sum is bounded from below by its largest term and,
578: from above, by $N$ times this largest term.
579: The statement on the number of leaves following Theorem 1
580: comes from the observation that the expected
581: total number of leaves is $L_S+L_C$, and $\displaystyle{\omega _S
582: (\alpha,3) = \Omega (1,\alpha,3) \le \max _{t \in[0;1]} \Omega
583: (t,\alpha,3) = \omega _C(\alpha,3 )}$.
584: \qed
585: \end{proof}
586:
587:
588: \begin{proof} ({\em Corollary 1}) Let $P_{sat}$ be the probability
589: that a random 3-SAT instance with $N$ variables and $\alpha N$ clauses
590: is satisfiable. Define
591: $\#L_{sat}$ and $\#L_{unsat}$ (respectively, $L_{sat}$ and
592: $L_{unsat}$) the expected numbers of leaves in \#DPLL-UC (resp. DPLL-UC)
593: search trees for satisfiable and unsatisfiable instances respectively.
594: All these quantities depend on $\alpha$ and $N$.
595: As the operations of \#DPLL and DPLL coincide for unsatifiable instances,
596: we have $\#L_{unsat} =L_{unsat}$. Conversely, $\#L_{sat} \ge L_{sat}$ since
597: DPLL halts after having encountered the first solution leaf.
598: Therefore, the difference between the average sizes \#L and L
599: of \#DPLL-UC and DPLL-UC search trees satisfies
600: $0 \le \#L - L = P_{sat} \; (\#L_{sat} - L_{sat}) \le P_{sat} \; \#L_{sat}$.
601: Hence, $1 - P_{sat} \; \#L_{sat}/\#L \le L/\#L \le 1$.
602: Using $\#L_{sat}\le 2^N$, $P_{sat} \le 2^N (7/8)^{\alpha N}$ from the
603: first moment theorem and the asymptotic scaling for $\#L$ given in
604: Theorem 1, we see that the left hand side of the previous inequality tends to 1
605: when $N\to \infty$ and $\alpha >\alpha _u$. \qed
606: \end{proof}
607:
608: \noindent Proofs for higher values of $k$ are
609: identical, and will be given in the full version.
610:
611: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
612:
613: \section{The GUC heuristic for random SAT and COL}
614:
615: The above analysis of the DPLL-UC search tree can be extended to the
616: GUC heuristic \cite{Fra}, where literals are preferentially chosen to
617: satisfy 2-clauses (if any). The outlines of the proofs of Theorems
618: 2 and 3 are given below; details will be found in the full version.
619:
620: {\bf 3-SAT}.
621: The main difference with respect to the UC case is that the
622: two branches issued from the split are not statistically identical. In
623: fact, the literal $\ell$ chosen by GUC satisfies at least one clause,
624: while this clause is reduced to a shorter clause when $\ell$ is set to
625: False. The cases $C_2\ge 1$ and $C_2=0$ have also to be considered
626: separately.
627: With $f_1,f_2,f_3$ defined in the same way as in the UC case,
628: we obtain
629: \begin{eqnarray}
630: \label{eqevg}
631: G(x_1,x_2,x_3&;&T+1\,) = \frac 1{f_1}\; G \big( f_1,f_2,f_3;
632: T\,\big) + \bigg( \frac{1+f_1}{f_2} - \frac 1{f_1} \bigg) \;
633: G\big( 0, f_2,f_3; T\, \big) \nonumber \\
634: &+& \bigg( \frac{1+f_2}{f_3} - \frac {1+f_1}{f_2} \bigg) \;
635: G\big( 0, 0,f_3; T\, \big) - \frac{1+f_2}{f_3} \; G(0,0,0;T) \ .
636: \end{eqnarray}
637: The asymptotic analysis of $G$ follows the lines of Section 3.
638: Choosing $f_2=f_1+f_1^2$ {\em i.e.}
639: $x_1=(-1+\sqrt{1+4 x_2})/2+O(1/N)$ allows us to cancel the second term on the
640: r.h.s. of (\ref{eqevg}). Iterating relation (\ref{eqevg}),
641: we establish the counterpart of Lemma 2 for GUC: the value of $G$ at height
642: $[tN]$ and argument $x_2,x_3$ is equal to its (known) value at height 0
643: and argument $y_2,y_3$ times the product of factors $\frac 1{f_1}$, up to an
644: additive term, $A$, including iterates of the third and fourth terms
645: on the right hand side of (\ref{eqevg}).
646: $y_2,y_3$ are the values at 'time' $\tau=0$ of the solutions of
647: the ordinary differential equations (ODE) $dY_2/d\tau=- 2 m(Y_2)/(1-\tau)$,
648: $dY_3 /d\tau = - 3 ((1+Y_2)/2-Y_3)/(1-\tau)$
649: with 'initial' condition $Y_2(t)=x_2$, $Y_3(t)=x_3$
650: (recall that function $m$ is defined in Theorem 2). Eliminating 'time'
651: between $Y_2,Y_3$ leads to the ODE in Theorem 2.
652: The first term on the r.h.s. in the expression of $\omega
653: ^g$
654: (\ref{refiuy}) corresponds to the logarithm of the
655: product of factors $\frac 1{f_1}$ between heights $0$ and $T$.
656: The maximum over $y_2$ in expression (\ref{refiuy}) for $\omega ^g$
657: is equivalent to the maximum over the reduced height $t$ appearing
658: in
659: $\omega _C$ in Theorem 1 (see also Proposition~2).
660: Finally, choosing $\alpha > \alpha _u^g$ ensures that,
661: from the one hand, the additive term $A$ mentioned above
662: is asymptotically negligible and, from the other hand,
663: the ratio of the expected sizes of \#DPLL-GUC and DPLL-GUC is
664: asymptotically equal to unity (see proof of Corollary 1).
665:
666:
667: {\bf 3-COL}.
668: The uniformity expressed by Lemma 1 holds: the
669: subgraph resulting from the coloring of $T$ vertices is still
670: Erd\H{o}s-R\'enyi-like with edge probability $\frac cN$, conditioned to
671: the numbers $C_j$ of vertices with $j$ available colors \cite{mol}.
672: The generating function $G$ of the average
673: number of residual asignments equals $(x_3)^N$ at height $T=0$ and
674: obeys the reccurence relation, for $T<N$,
675: \begin{eqnarray}
676: \label{eqevgc}
677: G(x_1,x_2,x_3;T+1\,) &=& \frac 1{f_1}\; G \big( f_1,f_2,f_3;
678: T\,\big) + \bigg( \frac{2}{f_2} - \frac 1{f_1} \bigg) \;
679: G\big( 0, f_2,f_3; T\, \big) \nonumber \\ &+&
680: \bigg( \frac{3}{f_3} - \frac {2}{f_2} \bigg) \; G\big( 0, 0,f_3; T\, \big)
681: \end{eqnarray}
682: with $f_1=(1-\mu)x_1$, $f_2=(1-2\mu)x_2+2\mu x_1$, $f_3=(1-3\mu)x_3+3\mu x_2$,
683: and $\mu =c/(3N)$.
684: Choosing $f_1=\frac 12 f_2$ {\em i.e.}
685: $x_1=\frac 12 x_2+O(1/N)$ allows us to cancel the second term on the
686: r.h.s. of (\ref{eqevgc}). Iterating relation (\ref{eqevg}),
687: we establish the counterpart of Lemma 2 for GUC: the value of $G$ at height
688: $[tN]$ and argument $x_2,x_3$ is equal to its (known) value at height 0
689: and argument $y_2,y_3$ respectively,
690: times the product of factors $\frac 1{f_1}$, up to an
691: additive term, $A$, including iterates of the last term in (\ref{eqevgc}).
692: An explicit calculation leads to $G(\frac 12
693: x_2,x_2,x_3;[tN])=e^{N \gamma^h(x_2,x_3,t)+o(N)} +A$ for $x_2,x_3>0$, where
694: $\gamma^h(x_2,x_3,t) = \frac c6 t^2 - \frac c3 t +(1-t)\ln (x_2/2)+
695: \ln[3 + e^{-2ct/3}(2 x_2/x_3-3)]$. As in Proposition 2, we bound
696: from below (respectively, above) the number of contradiction leaves in
697: \#DPLL-GUC tree by the exponential of ($N$ times) the value of function
698: $\gamma ^h$ in $x_2=x_3=1$ at reduced height $t$ (respectively,
699: lower than $t$).
700: The maximum over $t$ in Theorem 3 is equivalent to the maximum over the
701: reduced height $t$ appearing in $\omega _C$ in Theorem 1
702: (see also Proposition 2). Finally,
703: we choose $c _u^h$ to make the additive term $A$ negligible.
704: Following the notations of Corollary 1, we use $L_{sat}\le 3^N$, and
705: $P_{sat}\le 3^N e^{-Nc/6 + o(N)}$, the expected number of 3-colorings
706: for random graphs from $G(N,c/N)$.
707:
708: \section{Conclusion and perspectives}
709:
710: We emphasize that the average \#DPLL tree size can be calculated for even more
711: complex heuristics e.g. making decisions based on
712: literal degrees \cite{Kap}. This task requires, in
713: practice, that one is able: first, to find the correct
714: conditioning ensuring uniformity along a branch (as
715: in the study of DPLL in the absence of backtracking);
716: secondly, to determine the asymptotic behaviour of the associated
717: generating function $G$ from the recurrence relation for $G$.
718:
719:
720: To some extent,
721: the present work is an analytical implementation of an
722: idea put forward by Knuth thirty years ago \cite{Knu,Coc2}. Knuth
723: indeed proposed to estimate the average computational effort required
724: by a backtracking procedure through successive runs of the
725: non--backtracking counterpart, each weighted in an appropriate
726: way \cite{Knu}. This weight is, in the language of Section II.B,
727: simply the probability of a branch (given the heuristic
728: under consideration) in \#DPLL search tree times
729: $2^S$ where $S$ is the number of splits \cite{Coc2}.
730:
731: Since the amount of backtracking seems to have a heavy tail
732: \cite{Gent,Jia},
733: the expectation is often not a good predictor in practice.
734: Knowledge of the second moment of the search tree size would be
735: very precious; its calculation, currently under way, requires us to treat
736: the correlations between nodes attached to distinct branches.
737: Calculating the second moment is a step towards the distant goal of
738: finding the expectation of the logarithm, which
739: probably requires a deep understanding of correlations as in
740: the replica theory of statistical mechanics.
741:
742: Last of all, \#DPLL is a complete procedure for enumeration.
743: Understanding its average-case operation will, hopefully, provide
744: us with valuable information not only on the algorithm itself but also
745: on random decision problems e.g. new bounds on the sat/unsat
746: or col/uncol thresholds,
747: or insights on the statistical properties of solutions.
748:
749: \noindent
750: {\bf Acknowledgments:}
751: The present analysis is the outcome of a work started four years ago
752: with S. Cocco to which I am deeply indebted \cite{Coc,Coc2}.
753: I am grateful to C. Moore for numerous and illuminating
754: discussions, as well as for a critical reading of the manuscript.
755: I thank J. Franco for his interest and support, and the referee
756: for pointing out Ref. \cite{ben}, the results of which agree with the
757: $\alpha ^{-1/(k-2)}$ asymptotic scaling of $\omega$ found here.
758:
759: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
760:
761: \begin{thebibliography}{}
762:
763: \bibitem{mol}
764: Achlioptas, D. and Molloy, M.
765: Analysis of a List-Coloring Algorithm on a Random Graph,
766: in {\em Proc. Foundations of Computer Science (FOCS)}, vol 97, 204 (1997).
767:
768: \bibitem{Achl}
769: Achlioptas, D.
770: Lower bounds for random 3-SAT via differential equations,
771: {\em Theor. Comp. Sci.} {\bf 265}, 159--185 (2001).
772:
773: \bibitem{Achl3}
774: Achlioptas, D., Beame, P. and Molloy, M.
775: A Sharp Threshold in Proof Complexity.
776: in {\em Proceedings of STOC 01}, p.337-346 (2001).
777:
778: \bibitem{Bea}
779: Beame, P., Karp, R., Pitassi, T. and Saks, M.
780: On the complexity of unsatisfiability of random $k$-CNF formulas.
781: In {\em Proceedings of the Thirtieth Annual ACM Symposium on Theory of
782: Computing (STOC98)}, p. 561--571, Dallas, TX (1998).
783:
784: \bibitem{Cris}
785: Beame, P., Culberson, J., Mitchell, D. and Moore, C.
786: The resolution complexity of random graph k-colorability.
787: To appear in {\em Discrete Applied Mathematics} (2003).
788:
789: \bibitem{ben}
790: Ben-Sasson, E. and Galesi, N.
791: Space Complexity of Random Formulae in Resolution,
792: {\em Random Struct. Algorithms} {\bf 23}, 92 (2003).
793:
794: \bibitem{fra2}
795: Chao, M.T. and Franco, J.
796: Probabilistic analysis of two heuristics for the 3-satisfiability problem,
797: {\em SIAM Journal on Computing} {\bf 15}, 1106-1118 (1986).
798:
799: \bibitem{Fra}
800: Chao, M.T. and Franco, J.
801: Probabilistic analysis of a generalization of the unit clause literal
802: selection heuristics for the k-satisfiability problem,
803: {\em Information Science} {\bf 51}, 289--314 (1990).
804:
805: \bibitem{Chv}
806: Chv{\'a}tal, V. and Szemer\'edi, E.
807: Many hard examples for resolution,
808: {\em J. Assoc. Comput. Mach.} {\bf 35}, 759--768 (1988).
809:
810: \bibitem{Coc}
811: Cocco, S. and Monasson, R.
812: Analysis of the computational complexity of solving random satisfiability
813: problems using branch and bound search algorithms, {\em Eur. Phys. J. B}
814: {\bf 22}, 505 (2001).
815:
816: \bibitem{Coc2}
817: Cocco, S. and Monasson, R.
818: Heuristic average-case analysis of the backtrack resolution
819: of random 3-Satisfiability instances.
820: {\em Theor. Comp. Sci.} {\bf 320}, 345 (2004).
821:
822: \bibitem{fra0}
823: Franco, J. and Paull, M.
824: Probabilistic analysis of the Davis-Putnam procedure for solving
825: the satisfiability problem.
826: {\em Discrete Appl. Math.} {\bf 5}, 77--87 (1983).
827:
828: \bibitem{Eindor}
829: Ein-Dor, L. and Monasson, R.
830: The dynamics of proving uncolourability of large random graphs: I.
831: Symmetric colouring heuristic.
832: {\em J. Phys. A} {\bf 36}, 11055-11067 (2003).
833:
834: \bibitem{Fra2}
835: Franco, J.
836: Results related to thresholds phenomena research in satisfiability:
837: lower bounds.
838: {\em Theor. Comp. Sci.} {\bf 265}, 147--157 (2001).
839:
840: \bibitem{Fri}
841: Frieze, A. and Suen, S.
842: Analysis of two simple heuristics on a random instance of k-SAT.
843: {\em J. Algorithms} {\bf 20}, 312--335 (1996).
844:
845: \bibitem{Gent}
846: Gent, I. and Walsh, T.
847: Easy problems are sometimes hard.
848: {\em Artificial Intelligence} {\bf 70}, 335 (1993).
849:
850: \bibitem{Jia}
851: Jia, H. and Moore, C.
852: How much backtracking does it take to color random graphs? Rigorous
853: results on heavy tails. In {\em Proc.\ 10th International Conference on
854: Principles and Practice of Constraint Programming} (CP '04) (2004).
855:
856: \bibitem{Kap}
857: Kaporis, A.C., Kirousis, L.M. and Lalas, E.G.
858: The Probabilistic Analysis of a Greedy Satisfiability Algorithm.
859: {\em ESA}, p. 574-585 (2002).
860:
861: \bibitem{Karp}
862: Karp, R.M.
863: The probabilistic analysis of some combinatorial search algorithms,
864: in J.F. Traub, ed. Algorithms and Complexity, Academic Press, New York
865: (1976).
866:
867: \bibitem{knu}
868: Knuth, D.E.
869: The art of computer programming, vol. 1: Fundamental algorithms,
870: Section 2.2.1, Addison-Wesley, New York (1968).
871:
872: \bibitem{Knu}
873: Knuth, D.E.
874: Estimating the efficiency of backtrack programs.
875: {\em Math. Comp.} {\bf 29}, 136 (1975).
876:
877: \bibitem{mejean}
878: M\'ejean, H-M., Morel, H. and Reynaud, G.
879: A variational method for analysing unit clause search.
880: {\em SIAM J. Comput.} {\bf 24}, 621 (1995).
881:
882: \bibitem{Mit}
883: Mitchell, D., Selman, B. and Levesque, H.
884: Hard and Easy Distributions of SAT Problems,
885: {\em Proc.\ of the Tenth Natl.\ Conf.\ on Artificial Intelligence
886: (AAAI-92)}, 440-446,
887: The AAAI Press / MIT Press, Cambridge, MA (1992).
888:
889: \bibitem{purd2}
890: Purdom, P.W.
891: A survey of average time analyses of satisfiability algorithms.
892: {\em J. Inform. Process.} {\bf 13}, 449 (1990).
893:
894: \end{thebibliography}
895:
896:
897: \end{document}
898:
899: