1: \documentstyle[prl,epsfig,aps]{revtex}
2: %\documentstyle[prl,epsfig,aps,twocolumn]{revtex}
3: %\documentstyle[prb,epsfig,aps,12pt]{revtex}
4: \input{psfig.sty}
5: \begin{document}
6: \pagenumbering{arabic}
7: \pagestyle{plain}
8: \title{
9: Trajectories in phase diagrams, growth processes and computational
10: complexity: \\
11: how search algorithms solve the 3-Satisfiability problem.}
12:
13: \author{Simona Cocco \footnote{Current address: Department of Physics,
14: The University of Illinois at Chicago, 845 W. Taylor St., Chicago
15: IL 60607.}
16: and R{\'e}mi Monasson \footnote{Current address: The James Franck Institute,
17: The University of Chicago,
18: 5640 S. Ellis Av., Chicago IL 60637.} }
19:
20: \address{CNRS-Laboratoire de Physique Th{\'e}orique de l'ENS,
21: 24 rue Lhomond, 75005 Paris, France }
22:
23: \maketitle
24:
25: \begin{abstract}
26: \widetext
27: Most decision and optimization problems encountered in practice fall
28: into one of two categories with respect to any particular solving
29: method or algorithm: either the problem is solved quickly (easy) or
30: else demands an impractically long computational effort (hard).
31: Recent investigations on model classes of problems
32: have shown that some global parameters, such as the ratio between the
33: constraints to be satisfied and the adjustable variables, are good
34: predictors of problem hardness and, moreover, have an effect analogous
35: to thermodynamical parameters, e.g. temperature, in predicting phases
36: in condensed matter physics [Monasson et al., Nature 400 (1999)
37: 133-137]. Here we show that changes in the values of such parameters
38: can be tracked during a run of the algorithm defining a trajectory
39: through the parameter space. Focusing on 3-Satisfiability, a
40: recognized representative of hard problems, we analyze trajectories
41: generated by search algorithms using growth processes statistical
42: physics. These trajectories can cross well defined phases,
43: corresponding to domains of easy or hard instances, and allow to
44: successfully predict the times of resolution.
45: \end{abstract}
46:
47: \vskip .5cm
48: PACS Numbers~: 05.10, 05.70, 89.80
49: \vskip .5cm
50:
51: %\twocolumn
52:
53: % 3-SAT, DPLL and search trees.
54:
55: Consider a set of $N$ Boolean variables (that can be either true
56: or false) and a set of $M=\alpha\; N$ constraints (called clauses),
57: each of which being the logical OR of three variables or of their
58: negations, see Figure~1. Then, try to figure out whether there
59: exists or not an assignment of variables satisfying all clauses
60: (called solution).
61:
62: This problem, called 3-Satisfiability (3-SAT), is among the most
63: difficult ones to solve as its size $N$ becomes large. It is a
64: fundamental conjecture of computer science that no method exists to
65: solve 3-SAT efficiently\cite{NPC}, {\em i.e.} in time growing at most
66: polynomially with $N$. In practice, one therefore resorts to methods
67: that need, {\em a priori}, exponentially large computational
68: resources. One of these algorithms, the ubiquitous
69: Davis--Putnam--Loveland--Logemann (DPLL) solving
70: procedure\cite{DP,Cra,Hay}, is illustrated in Figure~1. DPLL operates
71: by trials and errors, the sequence of which can be graphically
72: represented as a search tree made of nodes connected through edges,
73: see Figure~1. Examples of search trees for satisfiable (sat) or
74: unsatisfiable (unsat) instances are shown Figure~2. Computational
75: complexity is the amount of operations performed by the solving
76: algorithm; we follow the convention that it is measured by the size of
77: the search tree, {\em i.e.} the number of nodes.
78:
79:
80: % Models and random 3-SAT.
81:
82: Complexity may, in practice, vary enormously with the instance, that is, the
83: set of clauses, under
84: consideration. To understand why instances are easy or hard to solve,
85: computer scientists have focused on model classes of 3-SAT instances.
86: Probabilistic models, that define distributions of random instances
87: controlled by few parameters, are particularly useful to shed light on
88: the onset of complexity. An example, that has attracted a lot of
89: attention over the past years, is random 3-SAT: all clauses are drawn
90: randomly and each variable negated or left unchanged with equal
91: probabilities. Experiments\cite{Cra,AI} and theory\cite{MZ} indicate
92: that clauses can almost surely always (respectively never) be
93: simultaneously satisfied if $\alpha$ is smaller (resp. larger) than a
94: critical threshold $\alpha _C \simeq 4.3$ as soon as $M,N$ go to
95: infinity at fixed ratio $\alpha$. This phase transition\cite{Sta,MZ}
96: is accompanied by a drastic peak of hardness at
97: threshold\cite{Cra,AI}, see Figure~3. A complete understanding of
98: this pattern of complexity has been lacking so far.
99:
100: In this letter we argue that search algorithms induce a dynamical
101: evolution of the computational problem to be solved. We shall show
102: how this complex and non-Markovian dynamics can be closely related to
103: (surface) growth processes. Statistical mechanics concepts and tools
104: thus allow to predict analytically and understand computational
105: complexity. For the sake of clarity, we shall report technical details
106: in another and extended paper \cite{ric}.
107:
108: % DPLL turns 3-SAT into 2+p-SAT
109:
110: As shown in Figure~1, the action of DPLL on an instance of 3-SAT
111: causes the reduction of 3-clauses to 2-clauses. We use a mixed 2+p-SAT
112: distribution\cite{Sta}, where $p$ is the fraction of 3-clauses,
113: to model what remains of the input instance at a node of the
114: search tree. Using experiments and methods from statistical
115: mechanics\cite{MZ}, the threshold line $\alpha _C (p)$ may be obtained
116: with the results shown in Figure~4 (full line). The phase diagram of
117: 2+p-SAT is the natural space in which the DPLL dynamic takes place. An
118: input 3-SAT instance with ratio $\alpha$ shows up on the right
119: vertical boundary of Figure~4 as a point of coordinates $(p=1,\alpha
120: )$. Under the action of DPLL, the representative point moves aside
121: from the 3-SAT axis and follows a trajectory. The
122: location of this trajectory in the phase diagram allows a precise
123: understanding of the search tree structure and of complexity.
124: (in the following, we consider the trajectories generated by DPLL using
125: the GUC heuristics\cite{Fra} -- see caption of Figure~1 -- but our
126: calculation could be repeated for other rules\cite{Cra,AI,Fra,Fri}).
127:
128: % Simple branches.
129:
130: At sufficiently small ratios $\alpha < \alpha _L \simeq 3.003$, DPLL
131: easily finds a solution\cite{Fra,Fri}. The search tree has a unique
132: branch (sequence of edges joining the top node to the extremity).
133: This branch grows as the fraction $t$ of variables assigned by DPLL
134: increases and terminates with a solution, see Figure~2A. Each node
135: along the branch carries a 2+p-SAT instance with characteristic
136: parameters $p$ and $\alpha$. The knowledge of the latter as functions
137: of the ``depth'' $t$ of the node, first established by Chao and
138: Franco\cite{Fra}, allows us to draw the trajectory followed by the
139: instance under the action of DPLL in Figure~4. The trajectory,
140: indicated by a light dashed line, first heads to the left and then
141: reverses to the right until reaching a point on the 3-SAT axis at
142: small ratio without ever leaving the sat region. Further action of
143: DPLL leads to a rapid elimination of the remaining clauses and the
144: trajectory ends up at the right lower corner S, where a solution is
145: achieved. Thus, in the range of ratios $\alpha < \alpha _L \simeq
146: 3.003$, 3-SAT is easy to solve: the computational complexity scales
147: linearly with the size $N$, see Figure~3.
148:
149: % Trees.
150:
151: For ratios above threshold ($\alpha > \alpha _C\simeq 4.3$), instances
152: have (almost) never a solution but a considerable amount of
153: backtracking is necessary before proving that clauses are
154: incompatible. As shown in Figure~2B, a generic unsat tree includes
155: many branches. The number $B$ of branches is related to the number $Q$
156: of nodes through the relation $Q=B-1$ valid for any complete tree,
157: check Figure~2B. Complexity grows exponentially\cite{Chv} as $2^{N
158: \omega}$. We have experimentally counted directly $Q$ or,
159: alternatively, $B$, and averaged the corresponding logarithms $\omega$
160: over a large number of instances. Results have then be extrapolated to
161: the $N\to \infty$ limit \cite{ric} and are reported in Table~1.
162:
163: We have analytically computed $\omega$ as a function of $\alpha$,
164: extending to the unsat region the probabilistic analysis of DPLL. The
165: search tree of Figure~2B is the output of a sequential process: nodes
166: and edges are added by DPLL through successive descents and
167: backtrackings. We have imagined a different building up, that results
168: in the same complete tree but can be mathematically analysed: the tree
169: grows in parallel, layer after layer. A new layer is added by
170: assigning, according to DPLL heuristic, one more variable along each
171: living branch. As a result, some branches split, others keep growing
172: and the remaining ones carry contradictions and die out. At a given
173: depth (fraction of assigned variables) $t$ in the tree, each branch
174: carries a 2+p-SAT instance, with characteristic parameters
175: $p$,$\alpha$. Its further evolution can be well approximated by a
176: Markovian stochastic process that depends only on $p$ and
177: $\alpha$. This approximation permits to write an evolution equation
178: for the logarithm $\omega(p,\alpha;t)$ of the average number of
179: branches with parameters $p,\alpha$ as the depth $t$ increases,
180: \begin{equation}
181: \frac{\partial \omega } {\partial t} = {\cal H} \left[ p, \alpha,
182: \frac{\partial \omega } {\partial p} , \frac{\partial \omega }
183: {\partial \alpha} ,t \right] \qquad , \label{croi}
184: \end{equation}
185: ${\cal H}$ incorporates the details of the splitting
186: heuristics\cite{nota1}. Partial differential equation (\ref{croi}) is
187: analogous to growth processes encountered in statistical physics
188: \cite{Gro}. The surface $\omega$, growing with ``time'' $t$ above the
189: bidimensional plane $p,\alpha$, describes the whole branches
190: distribution. Exponentially dominant branches are given by the top of
191: the distribution; the coordinates $p(t),\alpha(t)$ of the maximum of
192: $\omega$ define the tree trajectories on Figure~4. The hyperbolic line
193: indicates the halt points, where contradictions prevent tree
194: trajectories from further growing. Along the trajectory, $\omega$
195: grows from 0, on the right vertical axis up to some final positive
196: value on the halt line. This value is our theoretical prediction for
197: the logarithm of the complexity (divided by $N$). Values of $\omega$,
198: obtained for $4.3<\alpha<20$ by solving equation (\ref{croi}) compare
199: very well with numerical results, see Table~1.
200:
201: % Mixed case and point G.
202:
203: The intermediate region $\alpha_L < \alpha<\alpha_C$ juxtaposes the
204: two previous behaviours, see tree Figure~2C. The branch trajectory,
205: started from the point $(p=1,\alpha)$ corresponding to the initial
206: 3-SAT instance, hits the critical line $\alpha_c(p)$
207: at some point G with coordinates ($p_G,\alpha_G$). The
208: algorithm then enters the unsat phase and generates 2+p-SAT instances
209: with no solution. A dense subtree, that DPLL has to go through
210: entirely, forms below G till the halt line, see tree trajectory in
211: Figure~4. From our theoretical framework, the logarithm $\omega$ of
212: the size of this subtree can be analytically predicted. G is the
213: highest backtracking node in the tree (see Figure~2C) reached back by
214: DPLL, since nodes above G are located in the sat phase and carry
215: 2+p-SAT instances with solutions. We have checked experimentally this
216: scenario for $\alpha =3.5$. The coordinates of the average highest
217: backtracking node, $(p_G\simeq 0.78, \alpha _G \simeq 3.0$), coincide with
218: the analytically computed intersection of the single branch
219: trajectory and the critical line $\alpha_c(p)$, see Figure~4. As for
220: complexity, experiments on 3-SAT instances at $\alpha = 3.5$ or on
221: 2+0.78-SAT instances at $\alpha _G =3.0$ are in good
222: agreement with theoretical calculations of $\omega$, see Table~1. As a
223: conclusion, the structure of search trees for 3-SAT reflects the
224: existence of a critical line for 2+p-SAT instances. The latter may be
225: found back as the locus of highest backtracking nodes reached from all
226: initial 3-SAT ratios $\alpha$ in the intermediate range.
227:
228: % Conclusions.
229:
230: In conclusion, we have shown that statistical physics tools can be
231: useful to study the solving complexity of branch and bound algorithms
232: \cite{NPC,Hay} applied to hard combinatorial optimization or decision
233: problems. The phase diagram of Figure~4 affords a qualitative
234: understanding of the probabilistic complexity of DPLL variants on
235: random instances. This view may reveal the nature of the complexity of
236: search algorithms for SAT and related NP-complete problems \cite{NPC}.
237: In the sat phase, branch trajectories are related to polynomial time
238: computations while in the unsat region, tree trajectories lead to exponential
239: calculations. Depending on the starting point (ratio $\alpha$ of the
240: 3-SAT instance), one or a mixture of these behaviours is observed.
241: Figure~4 furthermore gives some insights to improve the search
242: algorithm. In the unsat region, trajectories must be as horizontal as
243: possible (to minimize their length) but resolution is necessarily
244: exponential\cite{Chv}. In the sat domain, heuristics making
245: trajectories steeper could avoid the critical line $\alpha _C (p)$ and
246: solve 3-SAT polynomially up to threshold.
247:
248: \vskip .3cm \noindent
249: {\bf Acknowledgements:} We are grateful to J. Franco for his
250: encouragements and numerous suggestions in the writing of this work.
251: We also thank A. Hartmann and M. Weigt for their interest in our results.
252:
253: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
254: \begin{thebibliography}{99}
255:
256: \bibitem{NPC}
257: Garey, M. \& Johnson, D.S.
258: {\it Computers and Intractability;
259: A guide to the theory of NP--completeness}
260: (W.H. Freeman and Co., San Francisco, 1979).
261:
262:
263: \bibitem{Cra}
264: Crawford, J. \& Auton, L.
265: {\em Proc.\ 11th Natl.\ Conference on Artificial Intelligence
266: (AAAI-93),} 21--27
267: (The AAAI Press / MIT Press, Cambridge, MA, 1993).
268:
269: \bibitem{AI}
270: Hogg, T., Huberman, B.A. \& Williams, C. (eds.)
271: Frontiers in problem solving: phase transitions and complexity.
272: {\em Artificial Intelligence} {\bf 81}(I \& II) (1996).
273:
274: \bibitem{Hay}
275: Hayes, B.
276: {\em American Scientist} {\bf 85}(2), 108--112 (1996).
277: % http://www.amsci.org/amsci/issues/Comsci97/compsci9703.html
278:
279: \bibitem{Sta}
280: Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B. \&
281: Troyansky, L.
282: {\em Nature} {\bf 400}, 133--137 (1999).
283:
284: \bibitem{DP}
285: Davis, M. \& Putnam, H.
286: {\em J.\ Assoc.\ Comput.\ Mach.} {\bf 7}, 201--215 (1960).
287:
288: \bibitem{MPV}
289: M{\'e}zard, M., Parisi, G.. \& Virasoro, M.A.
290: {\em Spin Glass Theory and Beyond}
291: (World Scientific, Singapore, 1987) and references therein.
292:
293: \bibitem{Gro}
294: McKane, A., Droz, M., Vannimenus, J. \& Wolf, D. (eds.)
295: {\em Scale invariance, interfaces, and non--equilibrium dynamics.}
296: (Nato Asi Series B: Physics vol. 344, Plenum Press, New-York, 1995).
297:
298: \bibitem{Fra}
299: Chao, M.T. \& Franco, J.
300: {\em Information Science} {\bf 51}, 289--314 (1990).
301:
302: \bibitem{MZ}
303: Monasson, R. \& Zecchina, R.
304: {\em Phys. Rev.} {\bf E 56}, 1357-1370 (1997).
305:
306: \bibitem{Bea}
307: Beame, P., Karp, R., Pitassi, T. \& Saks, M.
308: {\em ACM Symp.\ on Theory of Computing (STOC98)}, 561--571
309: (Assoc. Comput. Mach., New York, 1998).
310:
311: \bibitem{Fri}
312: Frieze, A. \& Suen, S.
313: {\em Journal of Algorithms} {\bf 20}, 312--335 (1996).
314:
315: \bibitem{Chv}
316: Chv{\`a}tal, V. \& Szmeredi, E.
317: {\em Journal of the ACM} {\bf 35}, 759--768 (1988).
318:
319: \bibitem{nota1}
320: In terms of the densities of 2- and 3-clauses, $c_2\,=\,\alpha\,
321: (1-t)\,(1-p)$, $c_3\,=\,\alpha\ (1-t)\,p\;$, and of the partial
322: derivatives $z_2=\partial \omega/ \partial c_2$, $z_3=\partial \omega/
323: \partial c_3$, we have for the GUC heuristics ${\cal H} (c_2 ,c_3, z_2
324: , z_3 ; t )= \log_{2} \nu (z_2 ) + [3\; c_3\; ( e^{z_3}
325: (1+e^{-z_2})/2 -1 )+ c_2 \; (\nu (z_2) -2 ) ] / (1-t) /\log 2$
326: where $\nu (z_2 ) = e^{z_2} \left(1+\sqrt{4\,e^{-z_2}+1}\right)/2$.
327: We have solved eqn.~(\ref{croi}) by expanding ${\cal H}$ at the linear
328: order in $z_2,z_3$. Notice that theory concentrates on the
329: logarithm of the average number of branches. This annealed
330: approximation of $\omega$ is very accurate above threshold \cite{ric}.
331:
332: \bibitem{ric}
333: S. Cocco, R. Monasson, in preparation.
334:
335: \end{thebibliography}
336:
337: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
338: \newpage
339: \vskip 2cm
340: \begin{center}
341: {\Large TABLE}
342: \end{center}
343: \vskip 1cm
344:
345: \begin{table}
346: $$
347: \begin{array}{|c |c| c|c|}
348: \hline
349: \multicolumn{1}{|c}{\hbox{\rm Ratio} \ \alpha} &
350: \multicolumn{2}{|c}{\hbox{\rm Experiments}} &
351: \multicolumn{1}{|c|}{\hbox{\rm Theory}} \\
352: \hbox{\rm clause/var.} & \hbox{\rm nodes} & \hbox{\rm branches} & \\
353: \hline
354: 20& 0.0153 \pm 0.0002 & 0.0151 \pm 0.0001 & 0.0152 \\
355: 15& 0.0207 \pm 0.0002 & 0.0206 \pm 0.0001 & 0.0206 \\
356: 10& 0.0320 \pm 0.0005 & 0.0317 \pm 0.0002 & 0.0319 \\
357: 7 & 0.0482 \pm 0.0005 & 0.0477 \pm 0.0005 & 0.0477 \\
358: 4.3& 0.089 \pm 0.001 & 0.0895 \pm 0.001 & 0.0875 \\
359: \hline
360: 3.5& 0.045 \pm 0.005 & 0.044 \pm 0.005 & \\
361: \cline{1-1}
362: 3.0 & 0.042 \pm 0.002 & 0.041 \pm 0.003 & 0.0453 \\
363: (p=0.78) & & & \\
364: \hline
365: \end{array}
366: $$
367: \vskip 1cm
368: {\bf Table 1:}
369: Logarithm of the complexity $\omega$ from measures of search tree
370: sizes (nodes and branches) and theory\cite{nota1}. Experimental
371: results obtained for $\alpha =3.5$ (sat phase) are compared to the
372: complexity of the unsat tree built from hit point G
373: ($p_G=0.78$,$\alpha_G=3$), see Figure~4. Uncertainties on $\omega$ are
374: larger due to finite size critical fluctuations on the location of G.
375: For $\alpha \gg 1$, our theoretical prediction $\omega = (3+\sqrt{5})
376: [\ln ((1+\sqrt 5)/2)]^2/ (6\ln 2)/\alpha \simeq 0.292/\alpha$ seems to
377: be exact \cite{Bea}; indeed, the search tree becomes small enough to
378: justify the decorrelation of branches done in (\ref{croi}).
379:
380: \end{table}
381:
382: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
383: \newpage
384: \vskip 1cm
385: \begin{center}
386: {\Large FIGURE CAPTIONS}
387: \end{center}
388: \vskip 1cm
389: {\bf Figure 1:}
390: Example of 3--SAT instance and Davis--Putnam--Loveland--Logemann
391: resolution. {\bf Step~0.} The instance consists of $M=5$ clauses
392: involving $N=4$ variables that can be assigned to true (T) or false
393: (F). $\bar w$ means (NOT $w$) and v denotes the logical OR. The search
394: tree is empty. {\bf 1.} DPLL randomly selects a variable among the
395: shortest clauses and assigns it to satisfy the clause it belongs to,
396: e.g. $w=$T (splitting with the Generalized Unit Clause --GUC--
397: heuristic) [6,9].
398: A node and an edge symbolising respectively the variable chosen ($w$)
399: and its value (T) are added to the tree. {\bf 2.} The logical
400: implications of the last choice are extracted: clauses containing $w$
401: are satisfied and eliminated, clauses including $\bar w$ are
402: simplified and the remaining ones are left unchanged. If no unitary
403: clause ({\em i.e.} with a single variable) is present, a new choice of
404: variable has to be made. {\bf 3.} Splitting takes over. Another node
405: and another edge are added to the tree. {\bf 4.} Same as step 2 but
406: now unitary clauses are present. The variables they contain have to
407: be fixed accordingly. {\bf 5.} The propagation of the unitary
408: clauses results in a contradiction. The current branch dies out and
409: gets marked with C. {\bf 6.} DPLL backtracks to the last split
410: variable ($x$), inverts it (F) and creates a new edge. {\bf 7.} Same
411: as step 4. {\bf 8.} The propagation of the unitary clauses
412: eliminates all the clauses. A solution S is found and the instance is
413: satisfiable. For an
414: unsatisfiable instance, unsatisfiability is proven when backtracking
415: (see step 6) is not possible anymore since all split variables have
416: already been inverted. In this case, all the nodes in the final search
417: tree have two descendent edges and all branches terminate by a
418: contradiction C.
419:
420: \vskip 1cm \noindent
421: {\bf Figure 2:}
422: Types of search trees generated by the DPLL solving procedure.
423: {\bf A.} {\em simple branch:} the algorithm finds
424: easily a solution without ever backtracking. {\bf B.} {\em dense tree:}
425: in the absence of solution, the algorithm builds a ``bushy'' tree,
426: with many branches of various lengths, before stopping. {\bf C.} {\em
427: mixed case, branch + tree:} if many contradictions arise before
428: reaching a solution, the resulting search tree can be decomposed in a
429: single branch followed by a dense tree. The junction G is the highest
430: backtracking node reached back by DPLL.
431:
432: \vskip 1cm \noindent
433: {\bf Figure 3:}
434: Complexity of 3-SAT solving for three problem sizes and averaged
435: over 10,000 randomly drawn samples.
436:
437: \vskip 1cm \noindent
438: {\bf Figure 4:}
439: Phase diagram of 2+p-SAT and dynamical trajectories
440: of DPLL.
441: The threshold line $\alpha_C (p)$ (bold full line) separates sat
442: (lower part of the plane) from unsat (upper part) phases. Extremities
443: lie on the vertical 2-SAT (left) and 3-SAT (right) axis at coordinates
444: ($p=0,\alpha _C=1$) and ($p=1,\alpha _C\simeq 4.3$) respectively.
445: Departure points for DPLL trajectories are located on the
446: 3-SAT vertical axis and the corresponding values of $\alpha$ are
447: explicitly given. Dashed curves represent tree trajectories in the
448: unsat region (thick lines, black arrows) and branch
449: trajectories [9] in the sat phase (thin lines, empty
450: arrows). Arrows indicate the direction of "motion" along trajectories
451: parametrised by the fraction $t$ of variables set by DPLL. For small
452: ratios $\alpha < \alpha _L$, branch trajectories remain
453: confined in the sat phase and end in S of coordinates $(1,0)$, where a
454: solution is found. At $\alpha_L\simeq 3.003$, the single branch trajectory hits
455: tangentially the threshold line in T of coordinates $(2/5,5/3)$. In
456: the intermediate range $\alpha _L < \alpha < \alpha_C$, the branch
457: trajectory intersects the threshold line at some point G (that depends
458: on $\alpha$). A dense tree then grows in the unsat phase, as happens
459: when 3-SAT departure ratios are above threshold $\alpha > \alpha _C
460: \simeq 4.3$. The tree trajectory halts on the dot-dashed curve
461: $\alpha \simeq 1.259/(1-p)$ where the tree growth process stops, see text.
462: At this point, DPLL has reached back the highest backtracking node in
463: the serach tree, that is, the first node when $\alpha > \alpha _C$, or node G
464: for $\alpha _L < \alpha < \alpha_C$.
465: In the latter case, a solution can be reached from a new descending branch
466: while, in the former case, unsatisfiability is proven.
467:
468: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
469: \begin{center}
470: \begin{figure}
471: \includegraphics[width=330pt,angle=0]{algo.eps}
472: \vskip 2cm
473: {\bf Figure 1}
474: \end{figure}
475:
476: \newpage
477: \begin{figure}
478: \includegraphics[width=250pt,angle=-90]{trees.eps}
479: \vskip 2cm
480: {\bf Figure 2}
481: \end{figure}
482:
483: \newpage
484: \begin{figure}
485: \includegraphics[width=280pt,angle=-90]{tempi.eps}
486: \vskip 2cm
487: {\bf Figure 3}
488: \end{figure}
489:
490: \newpage
491: \begin{figure}
492: \includegraphics[width=330pt,angle=-90]{diag.eps}
493: \vskip 2cm
494: {\bf Figure 4}
495: \end{figure}
496: \end{center}
497:
498: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
499: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
500:
501:
502:
503:
504: \end{document}
505:
506:
507:
508:
509:
510:
511:
512:
513:
514:
515:
516: