1: \documentclass{kluwer}
2: \input{psfig.sty}
3:
4: \begin{document}
5:
6: \begin{article}
7: \begin{opening}
8: \title{Restart method and exponential acceleration of random 3-SAT
9: instances resolutions: a large deviation analysis of the
10: Davis--Putnam--Loveland--Logemann algorithm.}
11:
12: \author{Simona \surname{Cocco} $^{1}$ and R{\'e}mi \surname{Monasson} $^{2,3}$}
13: \runningauthor{S. Cocco, R. Monasson}
14: \runningtitle{Restarts and Large deviations of DPLL}
15:
16: \institute{$^1$ CNRS-Laboratoire de Dynamique des Fluides Complexes,
17: 3 rue de l'Universit{\'e}, \\67000 Strasbourg, France.\\
18: $^{2}$ CNRS-Laboratoire de Physique Th{\'e}orique de l'ENS,
19: 24 rue Lhomond, \\75005 Paris, France. \\
20: $^{3}$ CNRS-Laboratoire de Physique Th{\'e}orique,
21: 3 rue de l'Universit\'e, \\67000 Strasbourg, France. }
22:
23: \begin{abstract}
24: The analysis of the solving complexity of random 3-SAT instances using
25: the Davis-Putnam-Loveland-Logemann (DPLL) algorithm slightly below threshold
26: is presented. While finding a solution for such instances demands
27: exponential effort with high probability, we show that an
28: exponentially small fraction of resolutions require a computation
29: scaling linearly in the size of the instance only. We compute
30: analytically this exponentially small probability of easy resolutions
31: from a large deviation analysis of DPLL with the Generalized
32: Unit Clause search heuristic,
33: and show that the corresponding exponent is smaller
34: (in absolute value) than the growth exponent of the typical
35: resolution time. Our study therefore gives some quantitative
36: basis to heuristic restart solving procedures, and suggests a natural
37: cut-off cost (the size of the instance) for the restart.
38: \end{abstract}
39: \keywords{restart, satisfiability, DPLL, large deviations.}
40: \end{opening}
41:
42:
43: \section{Introduction.}
44:
45: Being a NP-complete problem, 3-SAT is not thought to be solvable in an
46: efficient way, {\em i.e.} in time growing at most polynomially with
47: $N$. In practice, one therefore resorts to methods that need, {\em a
48: priori}, exponentially large computational resources. One of these
49: algorithms is the ubiquitous Davis--Putnam--Loveland--Logemann (DPLL)
50: solving procedure\cite{DP,survey}. DPLL is a complete search algorithm
51: based on backtracking. The sequence of assignments of variables made
52: by DPLL in the course of instance solving can be represented as a
53: search tree, whose size $Q$ (number of nodes) is a convenient measure
54: of the instance hardness. Some examples of search trees are presented
55: in Figure~1.
56:
57: In the past few years, many experimental and theoretical progresses
58: have been made on the probabilistic analysis of 3-SAT\cite{AI,Hans}.
59: Distributions of random instances controlled by few parameters are
60: particularly useful in shedding light on the onset of complexity. An
61: example that has attracted a lot of attention is
62: random 3-SAT: the three literals in a clause are randomly chosen
63: variables, or their negations with equal probabilities, among a set of
64: $N$ Boolean variables; clauses are drawn independently of each other.
65: Experiments\cite{AI,Mit,Cra,Kir} and theory\cite{Friedgut,Dubtcs}
66: indicate that clauses can almost surely always (respectively never) be
67: simultaneously satisfied if $\alpha$ is smaller (resp. larger) than a
68: critical threshold $\alpha _C \simeq 4.3$ as soon as $M,N$ go to
69: infinity at fixed ratio $\alpha$. This phase transition\cite{Sta} is
70: accompanied by a drastic peak in hardness at
71: threshold\cite{AI,Mit,Cra}. The emerging pattern of complexity is as
72: follows. At small ratios $\alpha < \alpha _L$, where $\alpha _L$
73: depends on the heuristic used by DPLL, instances are a.s. satisfiable
74: (sat). Finding a solution requires a tree whose size $Q$ scales only
75: linearly with the size $N$, and almost no backtracking is present
76: (Figure \ref{tree}A). Above the critical ratio, instances are
77: a.s. unsatisfiable (unsat) and proofs of refutation are obtained
78: through massive backtracking, leading to an exponential hardness $Q =
79: 2^{N\omega}$ with $\omega >0$\cite{Chv,Bea}.
80:
81: Recently, a quantitative understanding of the pattern of complexity
82: was proposed to estimate $\omega$ in the unsat regime as a function of
83: the ratio $\alpha$ of clauses per variables of the 3-SAT instance to
84: be solved, and to unveil the structure of DPLL's search tree in the
85: upper sat phase (Figure~\ref{tree}B), {\em i.e.} for ratios
86: $\alpha _L < \alpha < \alpha _C$ \cite{Coc1}.
87: In the latter range, instances are a.s. sat, but
88: their resolution requires with high probability an exponentially large
89: computational effort $(\omega >0)$ \cite{Coc1,Vardi1,Vardi2,Achl3}.
90: Theoretical predictions for $\omega$ as a function of $\alpha$ were
91: derived \cite{Coc1}, extending to the upper sat phase the calculations
92: of the unsat phase.
93:
94: In this paper, we study in more detail the upper sat phase, and more
95: precisely the distribution of resolutions complexities of randomly
96: drawn instances with ratios $\alpha _L < \alpha < \alpha _C$. Using
97: numerical experiments and analytical calculations, we show that,
98: though complexity $Q$ a.s. grows as $2^{N\omega}$,
99: there is a finite but exponentially small probability $2^{-N
100: \zeta}$ that $Q$ is bounded from above by $N$ only. In other words,
101: while finding solutions to these sat instances is almost always
102: exponentially hard, it is very rarely easy (polynomial time). Taking
103: advantage of the fact that $\zeta$ is smaller than $\omega$, we show
104: how systematic restarts of the heuristic may decrease substantially
105: the overall search cost. Our study therefore gives some theoretical
106: basis to incomplete restart techniques known to be efficient to solve
107: satisfiable instances\cite{Dubois,Gomes}, and suggests a natural
108: cut-off cost for the restart.
109:
110: We first start by recalling our previous framework for studying resolutions
111: taking place with high probability, which is helpful to understand rare
112: resolutions too (Section II). Numerical experiments are presented in
113: Section III. Section IV is devoted to the analytical calculation of
114: $\zeta$, and we present some conclusions in Section V. We have tried to
115: highlight the different status of the statements
116: and results presented: rigorous, expected to be exact
117: but proof lacking, approximate, or experimental. We hope
118: this effort will benefit the reader and make our work more accessible.
119:
120:
121: \begin{figure}
122: \begin{center}
123: \psfig{figure=trees.eps,width=320pt,height=200pt,angle=-90}
124: \end{center}\vskip .5cm
125: \caption{Types of search trees generated by the DPLL solving procedure
126: on satisfiable instances.
127: {\bf A.} {\em lower sat phase, $\alpha < \alpha _L$:} the algorithm finds
128: easily a solution with almost no backtracking. {\bf B.} {\em
129: upper sat phase, $\alpha _L < \alpha < \alpha _C$:}
130: many contradictions (c) arise before
131: reaching a solution, and backtracking enters massively into play.
132: Junction G is the highest node in the tree reached back by DPLL.
133: D denotes the first contradiction detected by DPLL, located at the
134: leaf of the first descent in the tree.}
135: \label{tree}
136: \end{figure}
137:
138:
139: \section{Resolution trajectories: the high probability scenario.}
140:
141: In this section, we briefly recall the main features of the resolution
142: by DPLL of satisfiable instances of size $N$, occurring with large
143: probability as $N\to\infty$\cite{fra2,Fra,Achl,Coc1}.
144:
145: The action of DPLL on an instance of 3-SAT causes the changes of the
146: overall numbers of variables and clauses, and thus of the ratio
147: $\alpha$. Furthermore, DPLL reduces some 3-clauses to 2-clauses. We
148: use a mixed 2+p-SAT distribution\cite{Sta}, where $p$ is the fraction
149: of 3-clauses, to model what remains of the input instance at a node of
150: the search tree. Using experiments and methods from statistical
151: mechanics\cite{Sta}, the threshold line $\alpha _C (p)$, separating
152: sat from unsat phases, may be estimated with the results shown in
153: Figure~\ref{diag}. For $p \le p_T = 2/5$, {\em i.e.} left to point $T$,
154: the threshold line is given by $\alpha _C(p)=1/(1-p)$, and saturates
155: the upper bound for the satisfaction of 2-clauses\cite{Sta,Achl}.
156: Above $p_T$, no exact expression for $\alpha _C (p)$ is known.
157:
158: The phase diagram of 2+p-SAT is the natural space in which the DPLL
159: dynamic takes place. An input 3-SAT instance with ratio $\alpha$ shows
160: up on the right vertical boundary of Figure~\ref{diag} as a point of
161: coordinates $(p=1,\alpha )$. Under the action of DPLL, the
162: representative point moves aside from the 3-SAT axis and follows a
163: trajectory which depends on the splitting heuristic implemented in
164: DPLL. We consider here the so-called Generalized Unit-Clause (GUC)
165: heuristic proposed by Franco and Chao\shortcite{fra2,Fra}
166: \cite{Francotcs,Achl}. Literals
167: are picked up randomly among one of the shortest available
168: clauses. This heuristic does not induce any bias nor correlation in
169: the instances distribution\cite{fra2}. Such a statistical
170: ``invariance'' is required to ensure that the dynamical evolution
171: generated by DPLL remains confined to the phase diagram of
172: Figure~\ref{diag}.
173:
174: Chao and Franco were able to analyze rigorously resolutions
175: corresponding to initial ratios $\alpha < \alpha _L \simeq
176: 3.003$. Their analysis consists in monitoring the evolution of the
177: densities (numbers divided by $N$) $c_2$ and $c_3$ of 2- and 3-clauses
178: respectively as more and more variables are assigned by DPLL. Both
179: densities become highly concentrated around the averages as the size
180: $N$ goes to infinity. Calling $t$ the fraction of assigned variables,
181: $c_2(t)$ and $c_3(t)$ obeys a set of coupled ordinary differential
182: equations (ODE),
183: \begin{eqnarray}
184: \frac {d c_3 (t)} {dt} &=& - \frac{3}{1-t} c_3 (t) - \rho _3 (t)
185: \nonumber \\
186: \frac {d c_2 (t)} {dt} &=& \frac{3}{2(1-t)} c_3 (t) -
187: \frac{2}{1-t} c_2 (t) - \rho _2 (t) \quad ,
188: \label{diff}
189: \end{eqnarray}
190: where $\rho_2 (t), \rho_3(t)$ are the probabilities that the split is
191: made from a 2-, 3-clause respectively. For GUC and an initial ratio
192: $\alpha_0 >2/3$, $\rho_2(t) = 1 - c_2(t)/(1-t), \rho_3(t)=0$.
193:
194: To obtain the single branch trajectory in the phase diagram of Figure~2,
195: we solve the ODEs (\ref{diff}) with initial conditions $c_2(0)=0,
196: c_3(0)=\alpha_0$, and perform the change of variables
197: \begin{equation}
198: \alpha (t) = \frac{c_2(t)+c_3(t)}{1-t} \qquad , \qquad
199: p(t) = \frac{c_3(t)}{c_2(t)+c_3(t)} \qquad ,
200: \label{change}
201: \end{equation}
202: to obtain
203: \begin{equation}
204: \alpha (t) =\frac{\alpha _0}4 (1-t)^2 + \frac {3\alpha _0}4
205: +\ln (1-t) \quad , \quad
206: p (t) = \frac{\alpha _0 (1-t)^2 }{\alpha (t)}
207: \quad .
208: \label{diff6}
209: \end{equation}
210:
211: Results are shown for the GUC heuristics and starting ratios $\alpha_0 =2$
212: and 2.8 in Figure~\ref{diag}. The trajectory,
213: indicated with a dashed line, first heads to the left and then
214: reverses to the right until reaching a point on the 3-SAT axis at
215: a small ratio. Further action of
216: DPLL leads to a rapid elimination of the remaining clauses and the
217: trajectory ends up at the right lower corner S, where a solution is
218: found. Note that for initial ratios $\alpha _0<2/3$, only the second
219: part of the trajectory restricted to the $p=1$ axis subsists.
220:
221: Frieze and Suen \shortcite{Fri}
222: have shown that, for ratios $\alpha _0 < \alpha _L \simeq 3.003$
223: (for the GUC heuristics), the full search tree essentially reduces
224: to a single branch, and is thus entirely described by the ODEs (\ref{diff}).
225: The amount of backtracking necessary to reach a solution is bounded from above
226: by a power of $\log N$. The average size of the branch $Q$ scales linearly
227: with $N$ with a multiplicative factor $\gamma (\alpha _0)=Q/N$ that can
228: be computed exactly\cite{Coc1}.
229:
230: The boundary $\alpha _L$ of this easy sat region can be defined as the largest
231: initial ratio $\alpha _0$ such that the branch trajectory $p(t),\alpha (t)$
232: issued from $\alpha _0$ never leaves the sat phase in the course of DPLL
233: resolution. Indeed, as $\alpha _0$ increases up to $\alpha_L$,
234: the trajectory gets closer and closer to the threshold line $\alpha _C
235: (p)$. Finally, at $\alpha _L \simeq 3.003$, the trajectory touches the
236: threshold curve tangentially at point $T$.
237:
238:
239: The concept of trajectory helps to understand how resolution takes
240: place in the upper sat phase, that is for ratios $\alpha _0$ ranging
241: from $\alpha _L$ to $\alpha _C$. The branch trajectory,
242: started from the point $(p=1,\alpha _0)$ corresponding to the initial
243: 3-SAT instance, hits the critical line $\alpha_c(p)$
244: at some point G with coordinates ($p_G,\alpha_G$) after $N\;t_G$ variables
245: have been assigned by DPLL, see Figure~\ref{diag}. The
246: algorithm then enters the unsat phase and generates 2+p-SAT instances
247: with no solution. Backtracking will appear as soon as a contradiction
248: is detected by DPLL. This may occur at any point along the trajectory
249: \cite{Fri}, but no further than the crossing point $D$ with
250: the $\alpha=1/(1-p)$ line (beyond $D$, unit-clauses are created at a
251: rate larger than their elimination through unit-propagation, and
252: opposite literals will appear w.h.p.). Later,
253: massive backtracking enters into play
254: \cite{Coc1} until $G$ is reached back by DPLL. $G$ is indeed the
255: highest backtracking node in the tree, since nodes above $G$
256: are located in the sat phase and carry 2+p-SAT instances with
257: solutions (Figure~\ref{tree}B). DPLL will eventually reach
258: a solution $S$ (Figure~\ref{tree}B).
259:
260: \begin{center}
261: \begin{figure}
262: \psfig{figure=diag.eps,width=340pt,angle=-90}
263: \vskip .5cm
264: \caption{Phase diagram of 2+p-SAT and dynamical trajectories
265: of DPLL for satisfiable instances.
266: The threshold line $\alpha_C (p)$ (bold full line) separates sat
267: (lower part of the plane) from unsat (upper part) phases. Extremities
268: lie on the vertical 2-SAT (left) and 3-SAT (right) axis at coordinates
269: ($p=0,\alpha _C=1$) and ($p=1,\alpha _C\simeq 4.3$) respectively.
270: Departure points for DPLL trajectories are located on the
271: 3-SAT vertical axis (empty circles)
272: and the corresponding values of $\alpha$ are explicitly given.
273: Arrows indicate the direction of "motion" along trajectories (dashed curves)
274: parametrized by the fraction $t$ of variables set by DPLL. For small
275: ratios $\alpha < \alpha _L$, branch trajectories remain
276: confined in the sat phase, end in S of coordinates $(1,0)$, where a
277: solution is found. At $\alpha_L$ ($\simeq 3.003$ for the GUC heuristic,
278: see text), the single branch trajectory hits
279: tangentially the threshold line in T of coordinates $(2/5,5/3)$. In
280: the range $\alpha _L < \alpha < \alpha_C$, the branch
281: trajectory intersects the threshold line at some point $G$ (that depends
282: on $\alpha$). With high probability, a contradiction arises before the
283: trajectory crosses the dotted curve $\alpha =1/(1-p)$ (point D);
284: through extensive backtracking, DPLL later reachs back the highest
285: backtracking node in the search tree ($G$) and find a solution
286: at the end of a new descending branch, see Figure~1B. With
287: exponentially small probability, the trajectory (dot-dashed curve, full
288: arrow) is able to cross
289: the "dangerous" region where contradictions are likely to occur; it
290: then exits from this contradictory region (point $D'$) and
291: ends up with a solution (lowest dashed curve, light arrow).}
292: \label{diag}
293: \end{figure}
294: \end{center}
295:
296:
297: \section{Numerical experiments.}
298:
299: In this section we present some numerical experiments on large but finite
300: instance sizes, showing some deviations from the high probability
301: scenario exposed above.
302:
303: \subsection{Instance-to-instance distribution of complexities.}
304:
305: We have first performed some experiments to understand the
306: distribution of instance-to-instance fluctuations of the solving
307: times\cite{runtorun,runtorun2,distribution}.
308: We draw randomly a large number of instances at fixed ratio
309: $\alpha =3.5$ and size $N$ and, for each of them, run DPLL until
310: a solution is found (a small number of unsat instances can
311: be present and are discarded). We show in Figure~\ref{histolog}
312: the normalized histogram of the logarithms $\omega$
313: of the corresponding complexities $Q=2^{N\omega}$.
314: The histogram is made of a narrow peak (left side) followed by a
315: wider bump (right side). As $N$ grows, the right peak acquires more
316: and more weight, while the left peak progressively disappears.
317: The abscissa of the center of the right peak gets slightly
318: shifted to the left, but seems to reach a finite value
319: $\omega ^* \simeq 0.035$ as $N\to \infty$\cite{Coc1}. This right peaks
320: thus corresponds to the core of exponentially hard resolutions: w.h.p.
321: resolutions of instances require a time scaling as
322: $2^{N \omega ^*}$ as the size of the instance gets larger and larger,
323: in agreement with the discussion of Section~II.
324:
325: \begin{center}
326: \begin{figure}
327: \psfig{figure=histon2.eps,width=330pt,angle=-90}
328: \vskip .5cm
329: \caption{Probability distribution of the logarithm $\omega$ of the complexity
330: (base 2, and divided by $N$) for $\alpha=3.5$ and for different sizes $N$.
331: Histograms are normalized to unity and obtained from 400,000 ($N=100$),
332: 50,000 ($N=200$), 20,000 ($N=300$), and 5,000 ($N=400$) samples}
333: \label{histolog}
334: \end{figure}
335: \end{center}
336:
337: On the contrary, the location of the maximum of the left peak
338: seems to vanish as $\log_2(N)/N$ when the size $N$ increases,
339: indicating that the left peak accounts for polynomial
340: (linear) resolutions. We have thus replotted the data shown in
341: Figure~\ref{histolog}, changing the scale of the horizontal
342: axis $\omega = \log_2(Q)/N$ into $Q/N$. Results are shown in
343: Figure~\ref{histolin}. We have limited ourself to $Q/N<1$, the range
344: of interest to analyse the left peak of Figure~\ref{histolog}.
345: The maximum of the distribution is located at $Q/N\simeq 0.2-0.25$,
346: with weak dependence upon $N$. The cumulative probability $P_{lin}$ to have a
347: complexity $Q$ less than, or equal to $N$, {\em i.e.} the integral of
348: Figure~\ref{histolin} over $0<Q/N<1$, decreases very quickly with $N$.
349: We find an exponential decrease, $P_{lin}= 2 ^{-N \zeta}$,
350: see Inset of Figure~\ref{histolin}. The rate $\zeta \simeq 0.011
351: \pm 0.001$ is determined from the slope of the logarithm of the probability
352: shown in the Inset.
353:
354: \begin{center}
355: \begin{figure}
356: \psfig{figure=istolin.eps,height=250pt,angle=-90}
357: \vskip .2cm
358: \caption{Probability distributions of the complexity $Q$ (divided by the
359: size $N$) for sizes $N=100$ (full line), $N=200$ (dashed line),
360: $N=300$ (dotted line), $N=400$ (dashed-dotted line).
361: Distributions are not shown for complexities larger than $N$.
362: Inset: Minus logarithm of the cumulative probability
363: of complexities smaller or equal to $N$ as a function of $N$, for sizes
364: ranging from 100 to 400 (full line); logarithm of the number of
365: restarts necessary to find a solution for sizes ranging from 100 to
366: 1000 (dotted line). Slopes are equal to $\zeta = 0.0011$ and $\bar
367: \zeta = 0.00115$ respectively.}
368: \label{histolin}
369: \end{figure}
370: \end{center}
371:
372: \subsection{Locus of highest backtracking points.}
373:
374: To gain some intuition on the origin of fast, linear resolutions, we
375: have looked for the locus of the highest backtracking nodes $G$ in the
376: search trees. In the infinite size limit, $G$ is located w.h.p. at the
377: crossing $G^*$ of the resolution trajectory and the critical sat/unsat
378: line (Section~II). In Figure~\ref{locus} we show numerical evidence
379: for the link between complexity and trajectories in the phase diagram
380: for finite instance sizes. We have run 20,000 instances ($\alpha=3.5,
381: N=300$), and reported for each of them the coordinates $p_G,\alpha_G$
382: of the highest backtracking point, and the logarithm $\omega$ of the
383: corresponding complexity. Large complexities ($\omega \ge 0.3$, right
384: bump of Figure~\ref{histolog}) are associated to points $G$ forming a
385: cloud centered around $G^*$ in the phase diagram of the 2+p-SAT model,
386: while points $G$ related to small complexities ($\omega \le 0.2$, left
387: peak of Figure~\ref{histolog}) are much more scattered in the phase
388: diagram. Notice the strong correlation between the value of $\omega$
389: and the average location of $G$ along the branch trajectory of Section
390: II. In the following we will concentrate on linear resolutions only. A
391: complementary analysis of the distribution of exponential
392: resolutions for the problem of the vertex covering of random graphs
393: was recently done by Montanari and Zecchina \shortcite{Mont}.
394:
395:
396: Figure~\ref{locus} shows that easy resolutions correspond to
397: trajectories capable of trespassing the contradiction line
398: $\alpha=1/(1-p)$. This, in addition to the linear scaling of the
399: corresponding complexities, indicates that easy resolutions coincide
400: with first descents in the search tree ending with a contradiction
401: located far beyond $D$ in the phase diagram, and then requiring a very
402: limited amount of backtracking before a solution is found.
403:
404: This statement is supported by the analysis of the number of
405: unit-clause generated during easy resolutions. We have measured the
406: maximal number $(C_1)_{max}$ of unit-clauses generated along the last branch
407: in the tree, leading to the solution $S$ (Figure~\ref{tree}B).
408: We found that $(C_1)_{max}$ scales linearly with $N$ with an extrapolated
409: ratio $(C_1)_{max}/N \simeq 0.022$ for $\alpha =3.5$. This linear scaling of
410: the number of unit-clauses is an additional proof of the trajectory
411: entering the "dangerous" region $\alpha >1/(1-p)$ of the phase
412: diagram where unit-clauses accumulate. In presence of a $O(N)$ number
413: of 1-clauses, the probability of survival of the branch (absence of
414: contradictory literals among the unit-clauses) will be exponentially
415: small in $N$, in agreement with scaling of the left peak weight in
416: Figure~\ref{histolog}.
417:
418: \begin{center}
419: \begin{figure}
420: \psfig{figure=diag2.eps,height=250pt,angle=-90}
421: \vskip .2cm
422: \caption{Locus of highest backtracking points $G$ in the phase diagram of
423: the 2+p-SAT model for 20,000 instances with $N=300$.
424: The bold gray line represent the first branch trajectory for $\alpha=3.5$.
425: Colors reflect the complexities of the instances, whose
426: logarithms $\omega$ range from 0.01 to 0.09, and are divided into 8
427: intervals of width $\Delta \omega=0.01$ and increasing darkness.
428: Filled triangles are the center of masses of points $G$
429: for each of the 8 intervals (the larger $\omega$,
430: the closer to the $p=1$ axis).}
431: \label{locus}
432: \end{figure}
433: \end{center}
434:
435: \subsection{Run-to-run fluctuations and restart experiments.}
436:
437: We have so far considered the instance-to-instance fluctuations of the
438: complexity, that is the distribution of complexity obtained from
439: one run of DPLL on each of a large number of instances.
440: In Figure~\ref{historun}, we now show the histogram of complexities for
441: a large number of runs on a unique, random instance. After each run,
442: clauses and variables are randomly relabeled to avoid any correlation
443: between different runs. Figure~\ref{historun} shows that these
444: run-to-run distributions are qualitatively independent of the particular
445: instances, and similar to the instance-to-instance distribution of
446: Figure~\ref{historun}\cite{runtorun,runtorun2}.
447: %The location of the linear resolution peak is
448: %largely instance independent, while its weight seems to exhibit some
449: %dependence upon instance.
450:
451: \begin{center}
452: \begin{figure}
453: \psfig{figure=historun.eps,height=220pt,width=290pt,angle=-90}
454: \vskip .5cm
455: \caption{Probability distributions of the logarithm $\omega$ of the
456: resolution complexity from 20,000 runs of DPLL. Each one of the five
457: distribution corresponds
458: to one randomly drawn instance of size $N=300$. The black curve is the
459: instance-to-instance fluctuations of the complexity shown on Figure~3.}
460: \label{historun}
461: \end{figure}
462: \end{center}
463:
464: The similarity between run-to-run and instance-to-instance
465: fluctuations for large sizes speaks up for the use of a systematic
466: stop-and-restart heuristic to speed up resolution: if a solution is
467: not found before $N$ splits, DPLL is stopped and launched again after
468: some random permutations of the variables and clauses. Intuitively,
469: the expected number of restarts necessary to find a solution should
470: indeed be equal to the inverse of the weight of the linear complexity
471: peak in Figure~\ref{histolog}, with a resulting total complexity
472: scaling as $N \; 2^{\,0.011\,N}$, and much smaller than the one-run
473: complexity $2^{\,0.035 \, N}$ of DPLL (Section II).
474:
475: We check the above reasoning by measuring the number $N_{rest}$ of
476: restarts performed before a solution is finally reached with the
477: stop-and-restart heuristic, and averaging $\log_2 (N_{res})$ over a
478: large number of random instances. Results are reports in the Inset of
479: Figure~\ref{histolin}. The typical number $N_{rest}= 2^{N\bar \zeta}$
480: of required restarts clearly grows exponentially as a function of the
481: size $N$ with a rate $\bar \zeta = 0.0115 \pm 0.001$. To the accuracy of
482: the experiments, $\zeta$ and $\bar \zeta$ coincide as expected.
483:
484: \section{Large deviation analysis of the first descent in the tree.}
485:
486: \subsection{Evolution equation for the instance.}
487:
488: Hereafter we compute the probability $\tilde P(C_1,C_2,C_3; T)$ that
489: the first branch of the tree carries an instance with $C_j$
490: $j$-clauses ($j=1,2,3$) after $T$ variables have
491: been assigned (and no contradiction has occurred).
492: Let us call ${\bf C}$ the vector $(C_1,C_2,C_3)$.
493: $P$ obeys a Markovian evolution
494: \begin{equation}
495: \tilde P({\bf C}; T+1) = \sum _{\bf C'} K ({\bf C},{\bf C'}; T)
496: \tilde P({\bf C'}; T)
497: \quad , \label{markov}
498: \end{equation}
499: where the entries of the transition matrix $K$ are equal to (for
500: the GUC heuristic),
501: \begin{eqnarray}
502: \label{bbra}
503: && K ({\bf C},{\bf C'}; T) = {C_3' \choose C_3'-C_3} \; \left
504: (\frac 3{2M}\right)^{C_3'-C_3} \; \left(1-\frac 3M\right)^{C_3}
505: \times \nonumber \\
506: && \sum_{w_2=0}^{C_3'-C_3}
507: {C_3'-C_3\choose w_2} \left \{(1 - \delta _{C'_1} )\;
508: \sum_{z_2=0}^{C_2'} {C_2' \choose z_2} \left (\frac
509: 1{M}\right)^{z_2}\, \left (1- \frac 2M\right)^{C_2'-z_2} \right.
510: \times \nonumber \\ &&
511: \sum_{w_1=0}^{z_2} {z_2\choose w_1} \sum_{z_1=0}^{C_1'-1}
512: {C_1'-1\choose z_1}\left (\frac {1} {2M}\right)^{z_1}
513: \left( 1- \frac 1 M\right)^{C_1'-1-z_1}\; \times
514: \nonumber \\
515: && \delta_{C_2-C_2'-w_2+z_2}
516: \;\delta_{C_1-C_1'-w_1+z_1+1} +\; \delta_{C_1'}
517: \sum_{z_2=0}^{C_2'-1} {C_2'-1 \choose z_2} \left (\frac
518: 1{M}\right)^{z_2}\,
519: \times \nonumber \\
520: &&\left( 1- \frac 2{M}\right)^{C_2'-1-z_2}
521: \left. \sum_{w_1=0}^{z_2} {z_2\choose w_1}\;
522: \delta_{C_2-C_2'-w_2+z_2+1} \; \delta_{C_1-w_1}
523: \right\} \ ,
524: \end{eqnarray}
525: and $\delta _C$ denotes the Kronecker delta function:
526: $\delta _C=1$ if $C=0$, $\delta _C=0$ otherwise. $M\equiv N-T$ is the
527: number of unassigned variables.
528:
529: We then define the generating function $P(\,{\bf y}\,;T\,)$ of
530: the probabilities $\tilde P(\,{\bf C}\,;T\,)$
531: where ${\bf y}\equiv(y_1,y_2,y_3)$, through
532: \begin{equation}
533: \label{gener}
534: {P}(\,{\bf y}\,;T\,) =\sum_{\bf C}\; e^{\,{\bf y} \cdot
535: {\bf C}}\; \tilde P(\,{\bf C}\,,T\,)\;
536: \end{equation}
537: where $\cdot $ denotes the scalar product.
538: Evolution equation (\ref{markov}) can be rewritten in term of the
539: generating function $P$,
540: \begin{eqnarray}
541: \label{eqev}
542: {P}(\,{\bf y}\,;T+1\,) &=& e^{-g_1({\bf y})} \; {P}\big(
543: \,{\bf g}({\bf y})\,; T\,\big) + \nonumber \\
544: && \left ( e^{- g_2({\bf y})}- e^{- g_1({\bf y})}\right) \;
545: {P}\big(-\infty,\,g_2({\bf y}),\,g_3({\bf y})\,; T\, \big)
546: \end{eqnarray}
547: where ${\bf g}$ is a vectorial function of argument ${\bf y}$ whose
548: components read
549: \begin{eqnarray}
550: g_1 ({\bf y}) &=&y_1+\ln\left[1+\frac 1 {N-T} \left
551: (\frac{e^{-y_1}}{2}-1\right)\right]
552: \nonumber\\
553: g_2({\bf y})&=&y_2+\ln\left[1+\frac 2 {N-T} \left (\frac{e^{-y_2}}{2}
554: \left(1+ e^{y_1}\right) -1\right)\right]
555: \nonumber \\
556: g_3 ({\bf y})&=&y_3+\ln\left[1+\frac 3 {N-T} \left (\frac{e^{-y_3}}{2}
557: \left(1+ e^{y_2}\right) -1\right)\right]
558: \end{eqnarray}
559: We now solve equation (\ref{eqev}) by making some hypothesis on the scaling
560: behavior of $P$ for large sizes.
561:
562: \subsection{Hypothesis for the large $N$ scaling of the probability.}
563:
564: Calculations leading to equation (\ref{eqev}) are rigorous. We shall
565: now make some hypothesis on $\tilde P, P$ that we believe to be correct
566: in the large size $N$ limit, but without providing rigorous proofs
567: for their validity. Our approach, common in statistical mechanics, may
568: be seen as a practical way to establish conjectures.
569:
570: First, each time DPLL assigns variables through splitting or
571: unit-propagation, the numbers $C_j$ of clauses of length $j$ undergo
572: $O(1)$ changes. It is thus sensible to assume that after a number $T = t\,
573: N$ of variables have been assigned, the densities $c_j=C_j/N$ of
574: clauses have been modified by $O(1)$. This translates into a scaling
575: Ansatz for the probability $\tilde P$,
576: \begin{equation}
577: \label{scalinghyp}
578: \tilde P({\bf C};T ) = e ^{ \,N \, \tilde \varphi ( c_1, c_2, c_3 ; t\,)}
579: \qquad \qquad (\tilde \varphi \le 0 )
580: \end{equation}
581: up to non exponential in $N$ corrections. From equations (\ref{gener})
582: and (\ref{scalinghyp}), we obtain the following scaling hypothesis for
583: the generating function $P$,
584: \begin{equation}
585: \label{scalinghyp2}
586: P({\bf y};T ) = e ^{\, N \, \varphi ( \,{\bf y}\, ; t\,)}
587: \end{equation}
588: up to non exponential in $N$ terms. Notice that $\varphi$ and $\tilde
589: \varphi$ are simply related to each other through Legendre transform,
590: \begin{eqnarray}
591: \varphi (\, {\bf y}\,;t\,) &=& \max _{\bf c} \bigg[ \tilde \varphi(\,
592: {\bf c} \, ; t\, ) + {\bf y} \cdot {\bf c}\bigg] \qquad ,
593: \\
594: \tilde \varphi (\, {\bf c}\,;t\,) &=& \min _{\bf y} \bigg[ \varphi(\,
595: {\bf y} \, ; t\, ) - {\bf y} \cdot {\bf c}\bigg]
596: \qquad . \label{inversion}
597: \end{eqnarray}
598: In particular, $\varphi ( {\bf y}={\bf 0};t)$ is the logarithm of the
599: probability (divided by $N$) that the first branch has not been hit by
600: any contradiction after a fraction $t$ of variables have been
601: assigned. The most probable values of the densities $c_j(t)$ of
602: $j$-clauses are then
603: obtained from the partial derivatives of $\varphi(\,{\bf y}\,;t\,)$ in
604: ${\bf y}={\bf 0}$: $c_j(t)=\partial \varphi/\partial y_j ({\bf y}={\bf 0})$.
605:
606: We now present the partial differential equations (PDE) obeyed by $\varphi$.
607: Two cases must be distinguished: the number $C_1$ of
608: unit-clauses may be bounded ($C_1=O(1), c_1=o(1)$), or of
609: the order of the instance size ($C_1=\Theta (N), c_1 = \Theta (1)$).
610:
611: \subsection{Case $C_1 = O(1)$: a large
612: deviation analysis around Chao and Franco's result.}
613:
614: When DPLL starts running on a 3-SAT instance, very few unit-clauses
615: are generated and splittings occur frequently. In other words, the
616: probability that $C_1=0$ is strictly positive when $N$ gets
617: large. Consequently, both terms on the r.h.s. of (\ref{eqev})
618: are of the same order, and we make the hypothesis that $\varphi$ does
619: not depend on $y_1$: $\varphi (y_1,y_2,y_3;t) = \varphi (y_2,y_3;t)$.
620: This hypothesis simply expresses that
621: $c_1=\partial \varphi/\partial y_1$ identically vanishes.
622:
623: Inserting expression (\ref{scalinghyp2}) into the evolution equation
624: (\ref{eqev}), we find\footnote{PDE (\ref{pde1}) is correct in the major
625: part of the $y_1,y_2,y_3$ space and, in particular, in the vicinity of
626: ${\bf y}={\bf 0}$ we focus on in this paper. It has however to be
627: to modified in a small region of the $y_1,y_2,y_3$ space; a complete
628: analysis of this case is not reported here but may be easily reconstructed
629: along the lines of
630: Appendix A in \cite{Coc2}.}
631: \begin{eqnarray} \label{pde1}
632: \frac{\partial \varphi}{\partial t} (y_2,y_3;t) = -y_2 &+& 2\, \gamma
633: (y_2,y_2;t)\; \frac{\partial \varphi}{\partial y_2} (y_2,y_3;t)
634: \nonumber \\ &+& 3 \, \gamma (y_2,y_3;t)\;
635: \frac{\partial \varphi}{\partial y_3} (y_2,y_3;t)
636: \end{eqnarray}
637: where function $\gamma$ is defined through,
638: \begin{equation}
639: \gamma (u,v;t) =\frac 1{1-t} \left (\frac{e^{-v}}{2}
640: \left(1+ e^{u}\right) -1\right) \qquad .
641: \label{gammas}
642: \end{equation}
643: PDE (\ref{pde1}) together with initial condition $\varphi({\bf y};
644: t=0) = \alpha _0\, y_3$ (where $\alpha _0$ is the ratio of clauses per
645: variable of the 3-SAT instance) can be solved exactly with the resulting
646: expression,
647: \begin{eqnarray} \label{ld}
648: \varphi (y_2,y_3;t) &=&
649: \alpha_0 \ln \left[ 1+ (1-t)^3 \left( e ^{y_3} - \frac 34 e ^{y_2} -
650: \frac 14 \right) + \frac {3 (1-t)}4 (e ^{y_2}-1) \right]
651: \nonumber \\ &+&
652: (1-t)\, y_2\, e ^{y_2} + (1-t) (e ^{y_2}-1) \ln(1-t)
653: \nonumber \\
654: &-&\left(e ^{y_2} +t-t \,e ^{y_2} \right)
655: \ln \left( e ^{y_2} +t-t\, e ^{y_2} \right)
656: \end{eqnarray}
657: Chao and Franco's analysis of the GUC heuristic may be recovered when
658: $y_2=y_3=0$ as expected. It is very easy to check that
659: $\varphi(y_2=0,y_3=0;t)=0$ (the probability of survival of the
660: branch is not exponentially small in $N$\cite{Fri}), and that the
661: derivatives $c_2(t), c_3(t)$ of $\varphi (y_2,y_3;t)$ with respect to
662: $y_2$ and $y_3$ coincide with the solutions of
663: (\ref{diff}). In addition, our calculation provides also a complete
664: description of rare deviations of the resolution trajectory from its
665: highly probable locus shown on Figure~\ref{diag}. As a simple
666: numerical example, consider DPLL acting on a 3-SAT instance of ratio
667: $\alpha_0 = 3.5$. Chao and Franco's analysis shows that, once e.g.
668: $t=20\%$ of variables have been assigned, the densities of 2- and
669: 3-clauses are w.h.p. equal to $c_2\simeq0.577$ and $c_3\simeq1.792$
670: respectively. Expression (\ref{ld}) gives access to the exponentially
671: small probabilities that $c_2$ and $c_3$ differ from their most
672: probable values. For instance, choosing $y_2=-0.1, y_3=0.05$, we find from
673: (\ref{ld}) and (\ref{inversion}) that there is a probability $e ^{-
674: 0.00567 N}$ that $c_2 =0.504$ and $c_3=1.873$ for the same fraction $t=0.2$ of
675: eliminated variables. By scanning all the values of $y_2,y_3$ we can
676: obtain a complete description of large deviations from Chao and
677: Franco's result\footnote{Though we are not concerned here with
678: subexponential (in $N$) corrections to
679: probabilities, let us mention that it is also possible to calculate the
680: probability of split ($C_1=0$) per unit of time, extending Frieze and
681: Suen's result \shortcite{Fri} to ${\bf y}\ne {\bf 0}$.}.
682:
683: The assumption $C_1= O(1)$ breaks down for the most probable
684: trajectory at some fraction $t_D$ e.g. $t_D\simeq 0.308$ for $\alpha
685: _0=3.5$ at which the trajectory hits point $D$ on Figure~\ref{diag}.
686: Beyond $D$, 1-clauses accumulate and the probability of survival of
687: the first branch is exponentially small in $N$.
688:
689: \subsection{Case $C_1 = O(N)$: passing through the "dangerous" region.}
690:
691: When the number of unit-clauses becomes of the order of $N$,
692: variables are a.s. assigned through unit-propagation. The first term
693: on the r.h.s. of equation (\ref{eqev}) is now exponentially dominant
694: with respect to the second one. The density of 1-clauses is strictly
695: positive, and $\varphi$ depends on $y_1$. We then obtain the following
696: PDE,
697: \begin{eqnarray} \label{pde2}
698: \frac{\partial \varphi}{\partial t} (y_1,y_2,y_3;t) &=& -y_1 + \gamma
699: (-\infty, y_1;t)\; \frac{\partial \varphi}{\partial y_1} (y_1,y_2,y_3;t)
700: \nonumber \\
701: &+& 2 \, \gamma (y_1,y_2;t)\; \frac{\partial \varphi}{\partial y_2}
702: (y_1,y_2,y_3;t) \nonumber \\
703: &+& 3 \, \gamma (y_2,y_3;t)\; \frac{\partial \varphi}
704: {\partial y_3} (y_1,y_2,y_3;t)
705: \end{eqnarray}
706: with $\gamma (u,v;t)$ given by equation (\ref{gammas}).
707: When $y_1=y_2=y_3=0$, equation (\ref{pde2}) simplifies to
708: \begin{equation} \label{pde3}
709: \frac{d z}{d t} (t) = -\frac{c_1(t)}{2(1-t)}
710: \qquad,
711: \end{equation}
712: where $c_1(t)$ is the most probable value of the density of unit-clauses,
713: and $z(t)$ is the logarithm of the probability that the branch has
714: not encountered any contradiction (divided by $N$).
715: The interpretation of (\ref{pde3}) is transparent. Each time a literal
716: is assigned through unit-propagation, there is a probability
717: $(1-1/2(N-T))^{C_1-1} \simeq e ^{-c_1/2/(1-t)}$ that no contradiction occurs.
718: The r.h.s. of (\ref{pde3}) thus corresponds to the rate of decay of
719: $z$ with "time" $t$.
720:
721: We have not been able to solve analytically PDE (\ref{pde2}), and have
722: resorted to an expansion of $\varphi$ in powers of ${\bf y}$.
723: To $k^{th}$ order, we approximate the solution of
724: (\ref{pde2}) by a polynomial of total degree $k$,
725: \begin{equation} \label{app}
726: \varphi ^{(k)} ({\bf y};t) = \sum _{e_1+e_2+e_3 \le k}
727: \varphi ^{(k)} _{e_1,e_2,e_3} (t) \; y_1 ^{e_1} \; y_2 ^{e_2} \; y_3 ^{e_3}
728: \end{equation}
729: and insert (\ref{app}) on the r.h.s. of (\ref{pde2}). We collect on
730: the l.h.s. the terms of degrees $\le k$ and obtain a set of ${\cal
731: N}_k=(k+3)(k+2)(k+1)/6$ first order coupled
732: linear ODEs for the coefficients $\varphi ^{(k)} _{e_1,e_2,e_3} (t)$ of the
733: polynomial (\ref{app}). This approximation gets better and better as
734: $k$ increases at a cost of more and more coupled ODEs to be solved.
735: The initial conditions for these ODEs are chosen to match the expansion of
736: the exact solution (\ref{ld}) at time $t_D$.
737:
738: \begin{table}
739: \begin{tabular}{ccccccc}
740: \hline
741: {\hbox{\rm order}}&
742: {\hbox{\rm $\zeta$}} & {\hbox{$(c_1) _{max}$}} &{\hbox {\rm$
743: t_{D'}$ }} &
744: {\hbox{$p_{D'}$}}& {\hbox {$\alpha_{D'}$}}&{\hbox {{$\gamma$}}}\\
745: \hline
746: 1 & .0384 & .0502 & .8878 & .0804 & .5477 & .1720 \\
747: 2 & .0036 & .0121 & .6553 & .2707 & 1.575 & .1990 \\
748: 3 & .0098 & .0227 & .7495 & .1901 & 1.201& .2069 \\
749: 4 & .0098 & .0226 & .7483 & .1911 & 1.206& .2069 \\
750: \hline
751: \end{tabular}
752: \caption{Results at different orders $k$ of approximation
753: for $\alpha _0=3.5$:
754: logarithm $\zeta$ of the probability that the first branch is not hit by any
755: contradiction, maximal density $(c_1)_{max}$ of unit-clauses ever
756: reached, fraction of eliminated variables $t_{D'}$
757: and coordinates $p_{D'}, \alpha_{D'}$ at point $D'$ {\em i.e.} when
758: the number of unit-clauses ceases to be $O(N)$,
759: complexity ratio $\gamma = Q/N$ of the corresponding linear
760: resolution.} \label{table}
761: \end{table}
762:
763: At the lowest order ($k=1$), we find a set of four coupled equations
764: for $z^{(1)}(t) \equiv \varphi ^{(1)} _{0,0,0} (t), c_1^{(1)}(t)
765: \equiv \varphi ^{(1)} _{1,0,0} (t), c_2^{(1)}(t)\equiv \varphi
766: ^{(1)} _{0,1,0} (t), c_3^{(1)}(t)\equiv \varphi
767: ^{(1)} _{0,0,1} (t)$ that read
768: \begin{eqnarray}
769: \frac {d c_1 ^{(1)}(t)} {dt} &=& -\frac{c_1^{(1)} (t)}{2(1-t)}
770: + \frac{c_2 ^{(1)}(t)}{1-t} \nonumber \\
771: \frac {d c_2 ^{(1)}(t)} {dt} &=& -\frac{2\,c_2 ^{(1)}(t)}{1-t}
772: +\frac{3\,c_3 ^{(1)}(t)}{2(1-t)} \nonumber \\
773: \frac {d c_3 ^{(1)}(t)} {dt} &=& - \frac{3 \, c_3 ^{(1)}(t)}{1-t}
774: \nonumber \\
775: \frac {d z ^{(1)}(t)} {dt} &=& - \frac{c_1 ^{(1)}(t)}{2(1-t)}
776: \quad , \label{diff2}
777: \end{eqnarray}
778: together with the initial conditions $c_1 ^{(1)}(t_D) = z
779: ^{(1)}(t_D)=0, c_2 ^{(1)}(t_D) = 1-t_D, c_2 ^{(1)}(t_D) = \alpha _0
780: (1-t_D)^3$, with $t_D$ uniquely determined from $\alpha_0$.
781: The solution of (\ref{diff2}) for $\alpha _0 =3.5$
782: shows that $c_1$ first increases and
783: reaches its top value $(c_1^{(1)})_{max}\simeq 0.05$. It then decreases
784: and vanishes at $t^{(1)}_{D'}\simeq 0.89$, where the trajectory exits
785: the "dangerous" region where contradictions occurs
786: w.h.p. (Figure~\ref{diag}). The probability of this event scales as
787: $2^{- N \zeta ^{(1)} }$ for large $N$, with $\zeta ^{(1)} = -
788: z ^{(1)}(t^{(1)}_{D'})/\ln 2 \simeq 0.038$. The end of the resolution
789: trajectory obeys Chao and Franco's equations (\ref{diff}).
790:
791: Results improve when going to higher orders in $k$, see
792: Table~\ref{table}. No sensible difference can be found between $k=3$ and
793: $k=4$ results. The calculated values of $\zeta \simeq 0.01, (c_1)
794: _{max}\simeq 0.022$ and $\gamma \simeq 0.21$ are in very good
795: agreement with the numerical experiments of Section~III.
796:
797: We report on Figure~\ref{autre} the experimental and theoretical
798: values of $\zeta$ found over the whole range $\alpha _L \le \alpha _0
799: \le \alpha_C$. Note the very good agreement between our
800: quantitative theory and simulations, which supports the scaling
801: hypothesis made above.
802:
803: \begin{center}
804: \begin{figure}
805: \psfig{figure=zeta.eps,height=260pt,angle=-90}
806: \vskip .5cm
807: \caption{Exponent $\zeta$ of the linear resolution probability
808: (simulations: filled squares, theory: full
809: line), and exponent $\omega$ of the typical complexity
810: (simulations: empty circles, theory from (Cocco, Monasson 2001b):
811: dotted line), as a function of the clause per variable ratio $\alpha$.}
812: \label{autre}
813: \end{figure}
814: \end{center}
815:
816: \section{Conclusions.}
817:
818: In this work, we have studied deviations from the typical ({\em i.e.}
819: occurring w.h.p.) solving complexity of satisfiable random 3-SAT
820: instances using DPLL algorithm with a simple splitting heuristic (GUC)
821: \cite{fra2,Fra}. For ratios $\alpha$ of clauses per variable in the
822: range $\alpha_L=3.003<\alpha<\alpha_C$, complexity grows almost surely
823: exponentially with the size $N$ of the instance, but resolution may
824: very rarely ({\em i.e.} with an exponentially small probability)
825: require a polynomial (linear) computational effort only. These linear
826: resolutions correspond to search tree reducing to a single branch
827: essentially (Figure~\ref{tree}A), and can be visualized as
828: trajectories that cross the unsat phase of the Figure~\ref{diag}
829: diagram without being stopped by any contradiction. Our approach
830: allowed us to calculate the large deviations from typical
831: resolutions, and the exponent $\zeta$ of the probability
832: $\tilde P \sim 2^{-\zeta\, N}$ of linear resolutions. Our
833: theoretical calculation predicts for instance that the exponent
834: corresponding to random 3-SAT instances with ratio $\alpha =3.5$
835: equals $\zeta \simeq 0.01$, in very good agreement with the values
836: extrapolated from the histogram of resolution time on different
837: instances (instance-to-instance distribution of complexities) and the
838: value $\bar \zeta$ extrapolated from the number of restarts necessary
839: to solve one random instance (Inset of Figure~\ref{histolin}).
840:
841: The computational effort to find a solution with the systematic
842: restart procedure, $N_{rest} \sim 1/ P _{lin} \sim 2^{N \zeta}$ turns out
843: to be exponentially smaller than the typical time to find a solution
844: $2^{N \omega}$ without restart (e.g. $\omega=0.035$ for $\alpha
845: =3.5$). Our calculation gives thus some theoretical support to the use
846: of restart-like procedures (see also \cite{Mont} for recent
847: theoretical results), empirically known to speed up considerably
848: resolutions\cite{Dubois,Gomes}. To be more concrete, while, without restarts,
849: we were able to solve with DPLL algorithm instances with 500
850: variables in about one day of CPU (for $\alpha =3.5$), the restart
851: procedure allows to solve instances with 1000 variables in 15 minutes
852: with the same computer and splitting heuristic (GUC).
853:
854: The present work suggests that the cut-off time, at
855: which the search is halted and restarted, need not be precisely tuned
856: but is simply given by the size of the instance. This conclusion could
857: be generic and apply to other combinatorial decision
858: problems and other heuristics. More precisely, if a combinatorial
859: problem admits some efficient (polynomial) search heuristic for some
860: values of control parameter (e.g. the ratio $\alpha$ here, or the
861: average adjacency degree for the coloring problem of random graphs),
862: there might be an exponentially small probability that the heuristic
863: is still successful (in polynomial time) in the range of parameters
864: where resolution almost surely requires massive backtracking and exponential
865: effort. When the decay rate of the polynomial time
866: resolution probability $\zeta$ is smaller than the growth rate
867: $\omega$ of the typical exponential resolution time, stop-and-restart
868: procedures with a cut-off in the search equal to a polynomial of the
869: instance size will lead to an exponential speed up of resolutions.
870:
871: It would be interesting to extend the previous approach to more
872: sophisticated and powerful search e.g. satz of chaff heuristics.
873: It is however not clear how a full analytical study could be worked out
874: without resorting to approximate expressions for the transition matrix.
875: Another natural extension of the present work would be to focus on
876: other decisions problems e.g. graph coloring for which
877: the high probability behaviour of simple heuristics is well understood
878: \cite{Achl4}.
879:
880: \acknowledgements
881: R. M. is supported in part by the ACI Jeunes Chercheurs
882: ``Algorithmes d'optimisation et syst{\`e}mes d{\'e}sordonn{\'e}s quantiques''
883: from the French Ministry of Research.
884:
885:
886: \begin{thebibliography}{}
887: \bibitem[\protect\citeauthoryear{Achlioptas and Molloy}{1997}]{Achl4}
888: Achlioptas, D. and Molloy, M.
889: Analysis of a List-Coloring Algorithm on a Random Graph,
890: in {\em Proceedings of FOCS 97}, p.204-212 (1997).
891:
892: \bibitem[\protect\citeauthoryear{Achlioptas et al.}{2001a}]{Achl1}
893: Achlioptas, D., Kirousis, L., Kranakis, E. and Krizanc, D.
894: Rigorous results for random (2+p)-SAT, {\em Theoretical Computer
895: Science} {\bf 265}, 109-129 (2001).
896:
897: \bibitem[\protect\citeauthoryear{Achlioptas}{2001b}]{Achl}
898: Achlioptas, D.
899: Lower bounds for random 3-SAT via differential equations,
900: {\em Theoretical Computer Science} {\bf 265}, 159--185 (2001).
901:
902: \bibitem[\protect\citeauthoryear{Achlioptas, Beame and Molloy}{2001c}]{Achl3}
903: Achlioptas, D., Beame, P. and Molloy, M.
904: A Sharp Threshold in Proof Complexity.
905: in {\em Proceedings of STOC 01}, p.337-346 (2001).
906:
907: \bibitem[\protect\citeauthoryear{Beame et al.}{1998}]{Bea}
908: Beame, P., Karp, R., Pitassi, T. and Saks, M.
909: {\em ACM Symp.\ on Theory of Computing (STOC98)}, 561--571
910: Assoc. Comput. Mach., New York (1998).
911:
912: \bibitem[\protect\citeauthoryear{Chao and Franco}{1986}]{fra2}
913: Chao, M.T. and Franco, J.
914: Probabilistic analysis of two heuristics for the 3-satisfiability problem,
915: {\em SIAM Journal on Computing} {\bf 15}, 1106-1118 (1986).
916:
917: \bibitem[\protect\citeauthoryear{Chao and Franco}{1990}]{Fra}
918: Chao, M.T. and Franco, J.
919: Probabilistic analysis of a generalization of the unit-clause literal
920: selection heuristics for the k-satisfiability problem,
921: {\em Information Science} {\bf 51}, 289--314 (1990).
922:
923: \bibitem[\protect\citeauthoryear{Chv{\`a}tal and Szmeredi}{1988}]{Chv}
924: Chv{\`a}tal, V. and Szmeredi, E. Many hard examples for resolution,
925: {\em Journal of the ACM} {\bf 35}, 759--768 (1988).
926:
927: \bibitem[\protect\citeauthoryear{Coarfa et al.}{2000}]{Vardi1}
928: Coarfa, C., Dernopoulos, D.D., San Miguel Aguirre, A., Subramanian, D.
929: and Vardi, M.Y. Random 3-SAT: The plot thickens. In R. Dechter, editor,
930: {\em Proc. Principles and Practice of Constraint Programming
931: (CP'2000)}, Lecture Notes in Computer Science 1894, 143-159 (2000);
932:
933: \bibitem[\protect\citeauthoryear{Cocco and Monasson}{2001}]{Coc1}
934: Cocco, S. and Monasson R.
935: Trajectories in phase diagrams, growth processes
936: and computational complexity: how search algorithms solve the
937: 3-Satisfiability problem, {\em Phys. Rev. Lett.} {\bf 86}, 1654 (2001)
938:
939: \bibitem[\protect\citeauthoryear{Cocco and Monasson}{2001b}]{Coc2}
940: Cocco, S. and Monasson, R.
941: Analysis of the computational complexity of solving random satisfiability
942: problems using branch and bound search algorithms, {\em
943: Eur. Phys. J. B} {\bf 22}, 505 (2001).
944:
945: \bibitem[\protect\citeauthoryear{Crawford and Auton}{1996}]{Cra}
946: Crawford, J. and Auton, L.
947: Experimental Results on the Cross-Over Point in Satisfiability Problems,
948: {\em Proc.\ 11th Natl.\ Conference on Artificial Intelligence
949: (AAAI-93),} 21--27, The AAAI Press / MIT Press, Cambridge, MA (1993);
950: {\em Artificial Intelligence} {\bf 81} (1996).
951:
952: \bibitem[\protect\citeauthoryear{Davis, Logemann and Loveland}{1962}]{DP}
953: Davis, M., Logemann, G. and Loveland, D.
954: {A machine program for theorem proving.}
955: {\em Communications of the ACM} {\bf 5}, 394-397 (1962).
956:
957: \bibitem[\protect\citeauthoryear{Dubois et al.}{1993}]{Dubois}
958: Dubois, O., Andre, P., Boufkhad, Y. and Carlier, J.
959: SAT versus UNSAT, {\em DIMACS Series in Discrete Math. and Computer
960: Science}, 415--436 (1993).
961:
962: \bibitem[\protect\citeauthoryear{Dubois et al.}{2001}]{Dubtcs}
963: Dubois, O., Monasson, R., Selman, B. and Zecchina, R. (eds)
964: Phase transitions in combinatorial problems.
965: {\em Theor. Comp. Sci.} {\bf 265} (2001).
966:
967: \bibitem[\protect\citeauthoryear{Franco}{2001}]{Francotcs}
968: Franco, J.
969: Results related to thresholds phenomena research in satisfiability:
970: lower bounds.
971: {\em Theoretical Computer Science} {\bf 265}, 147--157 (2001).
972:
973: \bibitem[\protect\citeauthoryear{Friedgut}{1999}]{Friedgut}
974: Friedgut, E.
975: Sharp thresholds of graph properties, and the k-sat problem,
976: {\em Journal of the A.M.S.} {\bf 12}, 1017 (1999).
977:
978: \bibitem[\protect\citeauthoryear{Frieze and Suen}{1996}]{Fri}
979: Frieze, A. and Suen, S.
980: Analysis of two simple heuristics on a random instance of k-SAT,
981: {\em Journal of Algorithms} {\bf 20}, 312--335 (1996).
982:
983: \bibitem[\protect\citeauthoryear{Gent and Walsh}{1994}]{distribution}
984: Gent, I.P. and Walsh, T. Easy problems are sometimes hard,
985: {\em Artificial Intelligence} {\bf 70}, 335-345 (1994).
986:
987: \bibitem[\protect\citeauthoryear{Gent, van Maaren and Walsh}{2000}]{Hans}
988: Gent, I., van Maaren, H. and Walsh, T. (eds),
989: SAT2000: Highlights of Satisfiability Research in the Year 2000,
990: {\em Frontiers in Artificial Intelligence and Applications},
991: vol. 63, IOS Press, Amsterdam (2000).
992:
993: \bibitem[\protect\citeauthoryear{Gomes et al.}{2000}]{Gomes}
994: Gomes, C.P., Selman, B., Crato, N. and Kautz, H. {\em J. Automated
995: Reasoning} {\bf 24}, 67 (2000).
996:
997: \bibitem[\protect\citeauthoryear{Gu, Purdom, Franco and Wah}{1997}]{survey}
998: Gu, J., Purdom, P.W., Franco, J. and Wah, B.W.
999: Algorithms for satisfiability (SAT) problem: a survey.
1000: {\em DIMACS Series on Discrete Mathematics
1001: and Theoretical Computer Science} {\bf 35}, 19-151,
1002: American Mathematical Society (1997).
1003:
1004: \bibitem[\protect\citeauthoryear{Hartmann and Weigt}{2001}]{Wei}
1005: Hartmann, A. and Weigt, M.
1006: Typical solution time for a vertex-covering algorithm on
1007: finite-connectivity random graphs,
1008: {\em Phys. Rev. Lett.} {\bf 86}, 1658 (2001).
1009:
1010: \bibitem[\protect\citeauthoryear{Hogg and Williams}{1994}]{runtorun}
1011: Hogg, T. and Williams, C.P. The hardest constraint problems: a double
1012: phase transition, {\em Artificial Intelligence} {\bf 69}, 359-377
1013: (1994).
1014:
1015: \bibitem[\protect\citeauthoryear{Hogg, Huberman and Williams}{1996}]{AI}
1016: Hogg, T., Huberman, B.A. and Williams, C. (eds)
1017: Frontiers in problem solving: phase transitions and complexity.
1018: {\em Artificial Intelligence} {\bf 81} I \& II (1996).
1019:
1020: \bibitem[\protect\citeauthoryear{Kirkpatrick and Selman}{1994}]{Kir}
1021: Kirkpatrick, S., and Selman, B.
1022: Critical Behavior in the Satisfiability of Random Boolean Expressions.
1023: {\em Science} {\bf 264}, 1297--1301 (1994).
1024:
1025: \bibitem[\protect\citeauthoryear{Mitchell, Selman and Levesque}{1992}]{Mit}
1026: Mitchell, D., Selman, B. and Levesque, H.
1027: Hard and Easy Distributions of SAT Problems,
1028: {\em Proc.\ of the Tenth Natl.\ Conf.\ on Artificial Intelligence
1029: (AAAI-92)}, 440-446,
1030: The AAAI Press / MIT Press, Cambridge, MA (1992).
1031:
1032: \bibitem[\protect\citeauthoryear{Monasson et al.}{1999}]{Sta}
1033: Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B. and Troyansky, L.
1034: Determining computational complexity from characteristic 'phase transitions'.
1035: {\em Nature} {\bf 400}, 133--137 (1999);
1036: 2+p-SAT: Relation of Typical-Case Complexity to the Nature of
1037: the Phase Transition,
1038: {\em Random Structure and Algorithms} {\bf 15}, 414 (1999).
1039:
1040: \bibitem[\protect\citeauthoryear{Montanari and Zecchina}{2002}]{Mont}
1041: Montanari, A., and Zecchina, R. Boosting search by rare events,
1042: {\em Phys. Rev. Lett.} {\bf 88}, 178701 (2002).
1043:
1044: \bibitem[\protect\citeauthoryear{San Miguel Aguirre et al.}{2001}]{Vardi2}
1045: San Miguel Aguirre, A. and Vardi, M.Y. Random 3-SAT and BDDs: The plot
1046: thickens further, (CP'2001) (2001).
1047:
1048: \bibitem[\protect\citeauthoryear{Selman and Kirkpatrick}{1996}]{runtorun2}
1049: Selman, B. and Kirkpatrick, S.
1050: Critical behavior in the computational cost
1051: of satisfiability testing, {\em Artificial Intelligence} {\bf 81},
1052: 273-295 (1996).
1053: \end{thebibliography}
1054:
1055: \end{article}
1056: \end{document}
1057: