1: \documentclass[11pt]{article}
2: %\documentclass[times,10pt,twocolumn]{article}
3: \usepackage{latex8}
4: \usepackage{times}
5: \usepackage{xspace}
6: %\usepackage{algorithm}
7: %\usepackage{algorithmic}
8: \usepackage{paralist}
9: \usepackage{amsmath}
10:
11: \pagestyle{empty}
12:
13:
14: %\documentclass{llncs}
15: \usepackage{epsfig}
16: %\usepackage{latex8}
17:
18: \newtheorem{obs}{Observation}
19: \newtheorem{theorem}{Theorem}[section]
20: \newtheorem{proposition}[theorem]{Proposition}
21: \newtheorem{lemma}[theorem]{Lemma}
22: \newtheorem{claim}[theorem]{Claim}
23: \def\squarebox#1{\hbox to #1{\hfill\vbox to #1{\vfill}}}
24: \newcommand{\qed}{\hspace*{\fill}
25: \vbox{\hrule\hbox{\vrule\squarebox{.667em}\vrule}\hrule}\smallskip}
26: \newenvironment{proof}{\begin{trivlist}
27: \item[\hspace{\labelsep}{\bf\noindent Proof: }]
28: }{\qed\end{trivlist}}
29: %\newcommand{\eqref}[1]{(\ref{#1})}
30: \newcommand{\boldd}{{\bf d}}
31: \newcommand{\e}{{\rm e}}
32: \newcommand{\ex}{{\rm E}}
33: \newcommand{\ds}{{\rm d}s}
34: \newcommand{\dt}{{\rm d}t}
35: \newcommand{\eps}{\epsilon}
36: \newcommand{\smallspacing}{\baselineskip = 0.98\normalbaselineskip}
37: \newcommand{\normalspacing}{\baselineskip=.985\normalbaselineskip}
38: \newcommand{\goesto}{\rightarrow}
39: \def\PUR{{\rm PUR}}
40: \newcommand{\N}{{\cal N}}
41: \newcommand{\R}{{\cal R}}
42: \newcommand{\whp}{w.h.p.}
43:
44: \newcommand{\remove}[1]{}
45:
46: \begin{document}
47:
48: \title{A Continuous-Discontinuous Second-Order Transition in the Satisfiability of Random
49: Horn-SAT Formulas}
50:
51: \author{Cristopher Moore\thanks{
52: Department of Computer Science, University of New Mexico,
53: Albuquerque NM, USA,
54: {\tt moore@cs.unm.edu}}
55: \and Gabriel Istrate\thanks{
56: CCS-DSS, Los Alamos National Laboratory, Los Alamos NM 87545, USA,
57: {\tt istrate@lanl.gov}}
58: \and Demetrios Demopoulos\thanks{
59: Archimedean Academy, 10870 SW 113 Place, Miami, FL, USA,
60: {\tt demetrios\_demopoulos@archimedean.org}}
61: \and Moshe Y. Vardi\thanks{
62: Department of Computer Science, Rice University,
63: Houston TX, USA,
64: {\tt vardi@rice.edu}}
65: }
66:
67: \maketitle
68: \thispagestyle{empty}
69:
70: \begin{abstract}
71: We compute the probability of satisfiability of a class of
72: %fixed-clause-length
73: random Horn-SAT formulae, motivated by a connection
74: with the nonemptiness problem of finite tree automata.
75: In particular, when the maximum clause length is 3,
76: this model displays a curve in its parameter space along which
77: the probability of satisfiability is discontinuous,
78: ending in a second-order phase transition where it becomes continuous.
79: This is the first case in which a phase transition of this type has been
80: rigorously established for a random constraint satisfaction problem.
81: \end{abstract}
82:
83:
84: \section{Introduction}
85:
86: In the past decade, phase transitions, or {\em sharp thresholds}, have
87: been studied intensively in combinatorial problems. Although the idea
88: of thresholds in a combinatorial context was introduced as early as 1960~\cite{ER60},
89: in recent years it has been a major subject
90: of research in the communities of theoretical computer science,
91: artificial intelligence and statistical physics. Phase transitions
92: have been observed in numerous combinatorial problems in which they
93: the probability of satisfiability jumps from $1$ to $0$ when the density of constraints
94: exceeds a critical threshold.
95:
96: The problem at the center of this research is, of course, 3-SAT.
97: An instance of 3-SAT is a Boolean formula, consisting of a conjunction
98: of clauses, where each clause is a disjunction of three literals. The goal
99: is to find a truth assignment that satisfies all the clauses and thus the entire formula.
100: The {\em density} of a 3-SAT instance is the ratio of the number of clauses to the number of
101: variables. We call the number of variables the {\em size\/} of the instance.
102: Experimental studies~\cite{CA96,SML96,SK96}
103: show a dramatic shift in the probability of satisfiability
104: of random 3-SAT instances, from 1 to 0, located at a critical density $r_c \approx 4.26$.
105: However, in spite of compelling arguments from statistical physics~\cite{MZ02,MPZ02},
106: and rigorous upper and lower bounds on the threshold if it exists~\cite{DBM00,HajiaSorkin,KKL},
107: there is still no mathematical proof that a phase transition takes place at that density.
108: \remove{
109: A limitation on all the experimental studies is
110: imposed by the inherent difficulty of the problem, especially around the
111: phase-transition point. We can only study instances of limited size
112: (usually up to a few hundred) before the problems get too hard to be solved
113: in reasonable time using available computational resources.
114: }
115: % CM: this is a bit unfair given the success of Survey Propagation.
116: For a view variants of SAT the existence and location of
117: phase transitions have been established rigorously, in particular for
118: 2-SAT, 3-XORSAT, and 1-in-$k$ SAT~\cite{ACIM01,DM02,CDMM03,CR92,Goe96}.
119:
120: In this paper we prove the existence of a more elaborate type of
121: phase transition, where a curve of discontinuities in a two-dimensional parameter
122: space ends in a {\em second-order} transition where the probability of satisfiability
123: becomes continuous. We focus on a particular variant of 3-SAT, namely
124: Horn-SAT. A Horn clause is a disjunction of literals of which {\em at most one} is positive,
125: and a Horn-SAT formula is a conjunction of Horn clauses. Unlike 3-SAT, Horn-SAT is a
126: tractable problem; the complexity of the Horn-SAT is linear in
127: the size of the formula~\cite{DG84}. This tractability allows
128: one to study random Horn-SAT formulae for much larger input sizes
129: that we can achieve using complete algorithms for 3-SAT.%~\cite{CA96,HW94,SML96}.
130:
131: An additional motivation for studying random Horn-SAT comes from the fact
132: that Horn formulae are connected to several other areas of computer science
133: and mathematics~\cite{Mak87}. In particular, Horn formulae are connected to
134: automata theory, as the transition relation, the starting state, and the set
135: of final states of an automaton can be described using Horn clauses.
136: For example, if we consider automata on binary trees,
137: then Horn clauses of length three can be used to describe its
138: transition relation, while Horn clauses of length one can describe
139: the starting state and the set of the final states of the automaton.
140: (we elaborate on this below).
141: Then the question of the emptiness of
142: the language of the automaton can be translated to a question about the
143: satisfiability of the formula. Since automata-theoretic techniques have
144: recently been applied in automated reasoning~\cite{VW86a,VW86b},
145: the behavior of random Horn formulae might shed light on these applications.
146:
147: Threshold properties of random Horn-SAT problems have recently been
148: actively studied. The probability of satisfiability of random
149: Horn formulae in a \emph{variable}-clause-length
150: model was fully characterized in~\cite{Ist02,Ist04},
151: where it was shown that random Horn formulae have a {\em coarse} rather
152: than a sharp satisfiability threshold, meaning that the
153: problem does not have a phase transition in this model.
154: The variable-clause-length model used there is ideally suited to studying Horn
155: formulae in connection with knowledge-based systems~\cite{Mak87}.
156: Bench-Capon and Dunne~\cite{BCD01} studied
157: a \emph{fixed}-clause-length model, in which each Horn clause has
158: precisely $k$~literals, and proved a sharp threshold with respect to
159: assignments that have at least $k-1$ variables assigned to be true.
160:
161: Motivated by the connection between the automata emptiness problem and
162: Horn satisfiability, Demopoulos and Vardi~\cite{DV05} studied
163: the satisfiability of two types
164: of fixed-clause-length random Horn-SAT formulae. They considered
165: 1-2-Horn-SAT, where formulae consist of clauses of length one and two
166: only, and 1-3-Horn-SAT, where formulae consist of clauses of length one
167: and three only. These two classes can be viewed as the Horn analogue of
168: 2-SAT and 3-SAT. For 1-2-Horn-SAT, they showed experimentally
169: that there is a coarse transition
170: (see Figure~\ref{1-2-0.1}), which can be explained and analyzed
171: in terms of random digraph connectivity~\cite{Kar90}.
172: The situation for of 1-3-Horn-SAT is less clear cut. On one hand,
173: recent results on random undirected hypergraphs~\cite{DN05} fit the
174: experimental data of~\cite{DV05} quite well. On the other, a scaling analysis of the data
175: suggested that transition between the mostly-satisfiable and mostly-unsatisfiable regions
176: (the ``waterfall'' in Figure~\ref{fig:1-3}) is steep but continuous, rather than a step function.
177: It was therefore not clear if the model exhibits a phase transition, in spite of
178: experimental data for instances with tens of thousands of variables.
179: % CM: greatly rewritten from the previous version
180:
181: In this paper we generalize the fixed-clause-length model of
182: \cite{DV05} and offer a complete analysis of the probability of
183: satisfiability in this model. For a finite $k>0$ and
184: a vector $\boldd$ of~$k$ nonnegative real numbers
185: ${d_1,d_2,\ldots,d_k}$, $d_1 < 1$, let the random Horn-SAT formula
186: $H^k_{n,\boldd}$ be the conjunction of
187: \begin{itemize}
188: \item a single negative literal $\overline{x}_1$,
189: \item $d_1 n$ positive literals chosen uniformly without replacement from $x_2,\ldots,x_n$, and
190: \item for each $2 \le j \le k$, $d_j n$ clauses chosen uniformly from the
191: $j{n \choose j}$ possible Horn clauses with $j$ variables where one literal is positive.
192: \end{itemize}
193: Thus, the classes studied in~\cite{DV05}
194: are $H^2_{n,d_1,d_2}$ and $H^3_{n,d_1,0,d_3}$ respectively.
195:
196: \begin{figure}[tbh]
197: \begin{center}
198: \begin{minipage}[t]{2.5 in}
199: \begin{center}
200: \psfig{figure=3dplot.ps,height= 70 truemm,width=65 truemm}
201: \end{center}
202: \end{minipage}
203: \begin{minipage}[t]{2.8 in}
204: \begin{flushright}
205: \hspace{0.5in}\psfig{figure=hornwaterfall.eps,height= 70 truemm,width= 65 truemm}
206: \end{flushright}
207: \end{minipage}
208: \caption{Satisfiability probability of a random 1-3-Horn
209: formula of size 20000. Left, the experimental results of~\cite{DV05};
210: right, our analytic results.}
211: \label{fig:1-3}
212: \end{center}
213: \end{figure}
214:
215: With this model in hand, we settle
216: the question of sharp thresholds for 1-3-Horn-SAT. In particular, we show that
217: there are sharp thresholds in some regions of the $(d_1,d_3)$ plane in the
218: probability of satisfiability, although not from $1$ to $0$. We start with the following
219: general result for the $H^k_{n,\boldd}$ model.
220:
221: \begin{theorem}\label{thm:main}
222: %Call a real number $t_0$ {\em critical for vector $\boldd$} if
223: %$s_1^{\prime}(t_0)= 0$,
224: %where function $s_1$ is defined by $s_1(t)= 1-t - (1-d_1) \exp\left(-\sum_{j=2}^k d_j t^{j-1} \right)$.
225: Let $t_0$ be the smallest positive root of the equation
226: \begin{equation}
227: \label{eq:1}
228: \ln \frac{1-t}{1-d_1} + \sum_{j=2}^k d_j t^{j-1} = 0 \enspace .
229: \end{equation}
230: Call $t_0$ {\em simple} if it is not a double root of~\eqref{eq:1}, i.e., if the derivative of the left-hand-side of~\eqref{eq:1} with respect to $t$ is nonzero at $t_0$. If $t_0$ is simple,
231: the probability that a random formula from $H^k_{n,\boldd}$ is satisfiable in the limit
232: $n \to \infty$ is
233: \begin{equation}
234: \label{eq:prsat}
235: \Phi(\boldd):=
236: \lim_{n\goesto \infty} \Pr[H^k_{n,\boldd} \mbox{ is satisfiable}] =
237: \frac{1-t_0}{1-d_1}
238: \enspace .
239: \end{equation}
240: \end{theorem}
241:
242: %The next two consequences assume non-criticality of $t$.
243: % CM: no they don't.
244: Specializing this result to the case $k=2$ yields an exact formula
245: that matches the experimental results in~\cite{DV05}:
246: \begin{proposition}\label{prop:2}
247: The probability that a random formula from
248: $H^2_{n,d_1,d_2}$ is satisfiable in the limit $n \to \infty$ is
249: \begin{equation}
250: \label{eq:prop2}
251: \Phi(d_1,d_2):=
252: \lim_{n\goesto \infty} \Pr[H^2_{n,d_1,d_2} \mbox{ is satisfiable}] =
253: -\frac{W\bigl(-(1-d_1)d_2e^{-d_2}\bigr )}{(1-d_1)d_2}
254: \enspace .
255: \end{equation}
256: \end{proposition}
257: Here $W(\cdot)$ is Lambert's function, defined as the principal root of
258: the equation $W(x)e^{W(x)}=x$.
259:
260: For the case $k=3$ and $d_2=0$, we do not have a closed-form
261: expression for the probability of satisfiability, though numerically Figure~\ref{fig:1-3} shows
262: a very good fit to the experimental results of~\cite{DV05}.
263: In addition, we find an interesting phase transition behavior
264: in the $(d_1,d_3)$ plane, described by the following proposition.
265: \begin{proposition}\label{prop:3}
266: The probability of satisfiability $\Phi(d_1,d_3)$ that a random formula from $H^3_{n,d_1,0,d_3}$
267: is satisfiable is continuous for $d_3 < 2$ and discontinuous for $d_3 > 2$. Its discontinuities are given by a curve $\Gamma$ in the $(d_1,d_3)$ plane described by the equation
268: \begin{equation}
269: \label{eq:gamma}
270: d_1
271: = 1 - \frac{\exp\left( \frac{1}{4} \left( \sqrt{d_3} - \sqrt{d_3-2} \right)^2 \right)}{d_3 - \sqrt{d_3 (d_3-2)}}
272: \enspace .
273: \end{equation}
274: This curve consists of the points $(d_1,d_3)$ at which $t_0$ is a double root of~\eqref{eq:1}, and ends at the critical point
275: \[ (1-\sqrt{\e}/2,2) = (0.1756...,2) \enspace . \]
276: \end{proposition}
277:
278: The curve $\Gamma$ of discontinuities described in Proposition~\ref{prop:3} can be seen in the right part of Figure~\ref{fig:1-3}. The drop at the ``waterfall'' decreases as we approach the critical point $(0.1756...,2)$, where the probability of satisfiability becomes continuous (although its derivatives at that point are infinite). We can also see this in Figure~\ref{fig:contour}, which shows a contour plot; the contours are bunched at the discontinuity, and ``fan out'' at the critical point. In both cases our calculates closely match the experimental results of~\cite{DV05}.
279:
280: \begin{figure*}[tbh]
281: \begin{minipage}[t]{3.2 in}
282: \begin{center}
283: \psfig{figure=contour25.ps, height= 45 truemm, width= 50 truemm}
284: \end{center}
285: \end{minipage}
286: \begin{minipage}[t]{3.3 in}
287: \begin{flushright}
288: \hspace{0.5in}\psfig{figure=contour-cropped.ps,height= 58 truemm, width= 60 truemm}
289: \end{flushright}
290: \end{minipage}
291: \caption{Contour plots. Left, the experimental results of~\cite{DV05}. Right, our analytical results.}
292: \label{fig:contour}
293: \end{figure*}
294:
295: %\begin{figure}[ht]
296: %\centerline{
297: %\psfig{figure=critical.ps,angle = -90,width= 80truemm}
298: %}
299: %\caption{The critical curve}
300: %\label{critical:curve}
301: %\end{figure}
302:
303: \remove{
304: Unlike much of the work on phase transitions in computer science,
305: rather than varying a single parameter, we explore a ``phase plane'' of
306: two parameters, namely the density of 3-clauses and unit clauses in the
307: formula. In this plane we see a very interesting behavior. There is a
308: curve along which $\Pr[\mbox{SAT}]$ jumps
309: discontinuously from one value to another; however, this curve ends at
310: a particular point, at which $\Pr[\mbox{SAT}]$ becomes continuous
311: (although its derivatives at that point are infinite).
312: The endpoint $d_1=(1-\sqrt{\e}/2,2)$, $d_3=2$ of the discontinuity
313: curve marks a transition between two
314: regimes: for $d_3<2$ the probability of satisfiability is continuous, while
315: for $d_3>2$ the probability of satisfiability becomes discontinuous.
316: }
317:
318: In statistical physics, we would say that $\Gamma$ is a curve of
319: {\em first-order} transitions, in which the order parameter is
320: discontinuous, ending in a {\em second-order} transition at the tip of
321: the curve, at which the order parameter is continuous, but has a
322: discontinuous derivative (see e.g.~\cite{BDFN92}).
323: A similar transition takes place in the Ising
324: model, where the two parameters are the temperature $T$ and the
325: external field $H$; the magnetization is discontinuous at the
326: line $H=0$ for $T < T_c$ where $T_c$ is the transition temperature,
327: but there is a second-order transition at $(T_c,0)$ and the
328: magnetization is continuous for $T \ge T_c$.
329:
330: To our knowledge, this is the first time that a
331: continuous-discontinuous transition of this type has been
332: established rigorously in a model of random constraint satisfaction
333: problems. We note that a similar phenomenon is believed to take place
334: for $(2+p)$-SAT model at the triple point $p=2/5$;
335: %(similar to the point where the three phases of water
336: %meet in the termperature-pressure phase plane);
337: % CM: confusingly, in water something else is going on. this turns out not to be a good analogy.
338: here the order parameter is the size of the backbone, i.e.,
339: the number of variables that take fixed
340: values in every truth assignment~\cite{AKKK01,MZKST99}. Indeed,
341: in our model the probability of satisfiability is closely related to the
342: size of the backbone, as we see below.
343:
344: \remove{
345: Theorem~\ref{thm:main} allows us to settle the apparent
346: contradiction in~\cite{DV05}
347: between the conclusion sugegsted by scaling anaysis and those
348: suggested by the random undirected hypergraphs approximation.
349: As the scaling analysis suggests, there is a sharp theshold for
350: satisfiability, but as our analysis here shows, the transition
351: is not from 1 to 0.
352: }
353:
354:
355: \section{Horn-SAT and Automata}
356:
357: %moshe: cut for now
358: %Before discussing our main results on thresholds in Horn-SAT,
359: %let us review some definitions related to combinatorial phase
360: %transitions, and show explicitly the
361: %relationship between Horn-SAT and finite automata.
362: %
363: %We use $B(n,p)$ to denote a binomial random variable with parameters
364: %$n$ and $p$ and $U \stackrel{D}{=} V$ to denote the fact that two random
365: %variables $U,V$ have identical distributions.
366: %
367: %Let $X$ be a
368: %finite set and $|X|=n$. Let $A$ be a random subset of $X$ constructed
369: %by a random procedure according to the probability space
370: %$\Omega(n,m)$ with measure:
371: %% $\Omega(n,m)\stackrel{D}{=}(2^X,2^{2^X},\mbox{Pr})$, where $\mbox{Pr}$
372: %% is defined as :
373: %$$\mbox{Pr}_{\Omega(n,m)}(A)=\left\{\begin{array}{ll}
374: %1/
375: %{n \choose m^*}
376: %& \mbox{if }|A|=m^* \\
377: %0 & \mbox{otherwise}\end{array} \right. ,$$
378: %where $m$
379: %is an integer and
380: %$$m^*=\left\{\begin{array}{ll}
381: %0 & \mbox{if } m<0 \\
382: %m & \mbox{if } 0\leq m\leq n \\
383: %n & \mbox{if } m>n \end{array} \right.$$
384: %
385: %The random procedure consists of selecting $m^*$ elements of $X$
386: %without replacement. A (set) property $Q$ of $X$ is a subset
387: %of $2^X$, the power set of $X$ consisting of all subsets of $X$.
388: %$Q$ is increasing if $A\in Q$ and $A\subseteq B\subseteq X$
389: %implies $B\in Q$. $Q$ is non-trivial if $\emptyset\not\in Q$ and $X\in Q$.
390: %A property sequence $Q$ consists of a sequence of sets $\{X_n:n\geq 1\}$
391: %such that $|X_n|<|X_{n+1}|$ and a family $\{Q_n:n\geq 1\}$ where each
392: %$Q_n$ is a property of $X_n$. $Q$ is increasing if $Q_n$ is
393: %increasing for every $n\geq 1$, and $Q$ is
394: %non-trivial if $Q_n$ is non-trivial for every $n\geq 1$.
395: %
396: %Let $Q_n$ be an increasing non-trivial property sequence, and
397: %$\theta:\N\goesto \R^+$ be a strictly positive function. We say
398: %that $\theta$ is a threshold for $Q$ if for every
399: %$f:\N\goesto\N$ :
400: %\begin{enumerate}
401: %\item If $\lim_{n\rightarrow\infty} f(n)/\theta(n)=0$ then $\lim_{n\rightarrow\infty}\mbox{Pr}_{\Omega(n,f(n))}(Q_n)=0$
402: %\item If $\lim_{n\rightarrow\infty} f(n)/\theta(n)=\infty$ then
403: %$\lim_{n\rightarrow\infty}\mbox{Pr}_{\Omega(n,f(n))}(Q_n)=1$
404: %\end{enumerate}
405: %
406: %$\theta$ is a sharp threshold $Q$ if for every
407: %$f:\N\rightarrow\N^+$ :
408: %\begin{enumerate}
409: %\item If $\sup_{n\rightarrow\infty} f(n)/\theta(n)<1$ then $\lim_{n\rightarrow\infty}\mbox{Pr}_{\Omega(n,f(n))}(Q_n)=0$
410: %\item If $\inf_{n\rightarrow\infty} f(n)/\theta(n)>1$ then
411: %$\lim_{n\rightarrow\infty}\mbox{Pr}_{\Omega(n,f(n))}(Q_n)=1$
412: %\end{enumerate}
413: %We say that $Q$ exhibits a phase transition if it has a
414: %sharp threshold.
415: %Our interest is in satisfiability of Horn formulae. Thus, in our
416: %framework $X_n$ is the set of Horn clauses over a set with~$n$ Boolean
417: %variables. A set of Horn clauses is a Horn formula.
418:
419: Our main motivation for studying the satisfiability of Horn
420: formulae is the unusually rich type of phase transition described above,
421: and the fact that its tractability allows us to perform experiments on
422: formulae of very large size. However, the original motivation of~\cite{DV05} that led
423: to the present work is the fact that Horn formulae can be
424: used to describe finite automata on words and trees.
425:
426: A finite automaton $A$ is a 5-tuple
427: $A=(S,\Sigma,\delta,s,F)$, where $S$ is a finite set of states, $\Sigma$
428: is an alphabet, $s$ is a starting state, $F\subseteq S$ is the set of
429: final (accepting) states and $\delta$ is a transition relation.
430: In a word automaton, $\delta$ is a function from $S\times\Sigma$ to
431: $2^S$, while in a binary-tree automaton $\delta$ is a function from
432: $S\times\Sigma$ to $2^{S\times S}$.
433: Intuitively, for word automata $\delta$ provides a set of
434: successor states, while for binary-tree automata $\delta$
435: provides a set of successor state pairs.
436: A run of an automaton on a word
437: $a=a_1a_2\cdots a_n$ is a sequence of states $s_0s_1\cdots s_n$ such
438: that $s_0=s$ and $(s_{i-1},a_i,s_i)\in\delta$.
439: A run is succesful if
440: $s_n\in F$: in this case we say that $A$ accepts the word $a$. A run
441: of an automaton on a binary tree $t$ labeled with letters from
442: $\Sigma$ is a binary tree $r$ labeled with states from $S$ such that
443: root$(r)=s$ and for a node $i$ of $t$,
444: $(r(i),t(i),r(\mbox{left-child-of-}i),r(\mbox{right-child-of-}i))\in\delta$.
445: Thus, each pair in $\delta(r(i),t(i))$ is a possible labeling of
446: the children of~$i$.
447: A run is succesful if for all leaves $l$ of $r$, $r(l)\in F$: in this
448: case we say that $A$ accepts the tree $t$. The language $L(A)$ of a
449: word automaton $A$ is the set of all words $a$
450: for which there is a successful run of $A$ on $a$. Likewise, the
451: language $L(A)$ of a tree automaton $A$ is the set of all trees $t$
452: for which there is a successful run of $A$ on $t$.
453: An important question in automata theory, which is also of
454: great practical importance in the field of formal verification
455: \cite{VW86a,VW86b}, is: given an automaton $A$, is $L(A)$ non-empty?
456: We now show how the problem of non-emptiness of automata
457: languages translates to Horn satisfiability. Thus, getting a
458: better understanding of the satisfiability of Horn formulae
459: would tell us about the expected answer to automata nonemptiness
460: problems.
461:
462: Consider first a word automaton
463: $A=(S,\Sigma,\delta,s_0,F)$. Construct a Horn formula $\phi_A$ over the
464: set $S$ of variables as follows:
465: %moshe: to save space
466: %\begin{itemize}
467: %\item
468: create a clause $(\bar{s_0})$,
469: %\item
470: for each $s_i\in F$ create a clause $(s_i)$,
471: %\item
472: for each element $(s_i,a,s_j)$ of $\delta$ create a clause
473: $(\bar{s_j}, s_i)$,
474: %\end{itemize}
475: where $(s_i,\cdots,s_k)$ represents the clause $s_i\vee\cdots\vee s_k$
476: and $\bar{s_j}$ is the negation of $s_j$.
477: Similarly to the word automata case, we can show how to construct a Horn
478: formula from a binary-tree automaton. Let $A=(S,\Sigma,\delta,s_0,F)$ be
479: a binary-tree automaton. Then we can construct a Horn formula $\phi_A$
480: using the construction above with the only difference that since
481: $\delta$ in this case is a function from $S\times\{\alpha\}$ to
482: $S\times S$, for each element $(s_i,\alpha,s_j,s_k)$ of $\delta$ we
483: create a clause $(\bar{s_j},\bar{s_k},s_i)$.
484:
485: \begin{proposition}
486: {\rm~\cite{DV05}}
487: Let $A$ be a word or binary tree automaton and $\phi_A$ the Horn formula
488: constructed as described above. Then $L(A)$ is non-empty if and only if
489: $\phi_A$ is unsatisfiable.
490: \end{proposition}
491:
492: \section{Main Result}
493: \label{main}
494:
495: \begin{figure}[t]
496: \small{
497: \begin{center}
498: \noindent \fbox{
499: \begin{minipage}[p]{3.75in}
500: \small{
501: \smallspacing
502: \medskip
503: \noindent
504: {\bf Algorithm $\PUR$:}
505: \begin{asparaenum}
506: %\begin{enumerate}
507: \item while ($\phi$ contains positive unit clauses)
508: \item \hspace{5mm} choose a random positive unit clause $x$
509: \item \hspace{5mm} remove all other clauses in which $x$ occurs positively
510: in $\phi$
511: \item \hspace{5mm} shorten all clauses in which $x$ appears negatively
512: \item \hspace{5mm} label $x$ as ``implied'' and call the algorithm recursively.
513: \item if no contradictory clause was created
514: \item \hspace{5mm} accept $\phi$
515: \item else
516: \item \hspace{5mm} reject $\phi$.
517: \end{asparaenum}
518: }
519: \end{minipage}
520: }
521: \end{center}
522: \caption{\textbf{Positive Unit Resolution.}}
523: \label{pur}
524: }
525: \end{figure}
526:
527: \normalsize
528: \normalspacing
529: %\morespacing
530:
531: Consider the positive unit resolution algorithm $\PUR$ applied to a random formula $\phi$ (Figure~\ref{pur}). The proof of Theorem~\ref{thm:main} follows immediately from the following theorem, which establishes the size of the backbone of the formula with the single negative literal $\overline{x}_1$ removed: that is, the set of positive literals implied by the positive unit clauses and the clauses of length greater than $1$. Then $\phi$ is satisfiable as long as $x_1$ is not in this backbone.
532: %As a technicality, we say that $t$ is {\em critical} for $\boldd$ if
533: %$s^{\prime}(t)=0$,
534: %where $s(t)= 1-t - (1-d_1) \exp\left(-\sum_{j=2}^k d_j t^{j-1} \right)$.
535:
536: \begin{lemma}
537: \label{lem:gen}
538: Let $\phi$ be a random Horn-SAT formula $H^k_{n,\boldd}$ with $d_1 > 0$. Denote by $t_0$ the smallest positive root of Equation~\eqref{eq:1}, and suppose that $t_0$ is simple. Then, for any $\eps > 0$, the number $N_{\boldd,n}$ of implied positive literals, including the $d_1 n$ initially positive literals, satisfies \whp\ the inequality
539: \begin{equation}
540: \label{eq:implied}
541: (t_0-\eps) \cdot n < N_{\boldd,n} < (t_0+\eps) \cdot n,
542: \end{equation}
543: \end{lemma}
544:
545: \begin{proof}
546: First, we give a heuristic argument, analogous to the branching process argument for the size of the giant component in a random graph. %In $H^{1,k}_{n,d}$,
547: The number $m$ of clauses of length $j$ with a given literal $x$ as their implicate (i.e., in which $x$ appears positively) is Poisson-distributed with mean $d_j$. If any of these clauses have the property that all their literals whose negations appear are implied, then $x$ is implied as well. In addition, $x$ is implied if it is one of the $d_1 n$ initially positive literals. Therefore, the probability that $x$ is {\em not} implied is the probability that it is not one of the initially positive literals, and that, for all $j$, for all $m$ clauses $c$ of length $j$ with $x$ as their implicate, at least one of the $j-1$ literals whose negations appear in $c$ is not implied. Assuming all these events are independent, if $t$ is the fraction of literals that are implied, we have
548: \begin{align*}
549: 1-t & = (1-d_1) \prod_{j=2}^k
550: \left( \sum_{m=0}^{\infty} \frac{\e^{-d_j} d_j^{m}}{m!} (1-t^{j-1})^{m} \right) \\
551: & = (1-d_1) \prod_{j=2}^k \exp(-d_j t^{j-1}))
552: = (1-d_1) \,\exp\left( - \sum_{j=2}^k d_j t^{j-1}\right)
553: \end{align*}
554: yielding Equation~\eqref{eq:1}.
555:
556: To make this rigorous, we use a standard technique for proving results about
557: threshold properties: analysis of algorithms via differential equations~\cite{Wor95} (see~\cite{achreview} for a review). We analyze the while loop of $\PUR$ shown in Figure~\ref{pur}; specifically, we view $\PUR$ as working in {\em stages}, indexed by the
558: number of literals that are labeled ``implied.''
559: %That is, initially, only the $d_1 n$ positive literals are labeled.
560: % CM: no, they're not.
561: After $T$ steps of this process, $T$ variables are labeled as implied.
562: At each stage the resulting formula consists of a set of
563: Horn clauses of length $j$ for $1 \le j \le k$ on the $n-T$ unlabeled variables.
564: Let the number of distinct clauses of length $j$ in this formula be $S_j(T)$;
565: we rely on the fact that, at each stage $T$, conditioned on the values of $S_j(T)$
566: the formula is uniformly random. This follows from an easy induction argument
567: which is standard for problems of this type (see e.g.~\cite{Ist04}).
568:
569: \remove{
570: The technical result on which our analysis rests is the following
571: ``uniformity lemma'':
572: \begin{claim}
573: Conditional on the values of $S_j(T)$,
574: the formula at stage $T$ is random and uniform.
575: \end{claim}
576: }
577:
578: %Let us now derive recurrence relations for the expected values of the $S_j$.
579: Now, the variables appearing in the clauses present at stage $T$ are chosen
580: uniformly from the $n-T$ remaining variables, so the probability that the chosen variable $x$
581: appears in a given clause of length $j$ is $j/(n-T)$, and the probability
582: that a given clause of length $j+1$ is shortened to one of length $j$
583: (as opposed to removed) is $j/(n-T)$. A newly shortened clause is
584: distinct from all the others with probability $1-o(1)$ unless $j=1$,
585: in which case it is distinct with probability $(n-T-S_1)/(n-T)$.
586: Finally, each stage labels the variable in one of the $S_1(T)$ unit clauses as implied.
587: Thus the expected effect of each step is
588: \begin{eqnarray*}
589: \ex[S_j(T+1)] & =& S_j(T) + j \frac{S_{j+1}(T) - S_j(T)}{n-T} + o(1)
590: \quad \mbox{for all } 2 \le j \le k \\
591: \ex[S_1(T+1)] & =& S_1(T) + \left( \frac{n-T-S_1}{n-T} \right) \left( \frac{S_2(T)}{n-T} \right) - 1 + o(1)
592: \end{eqnarray*}
593: % CM: Gabi, all we need here is the expectation, not these distributions!
594: % also your difference equation for S_1 was wrong.
595:
596: \remove{
597: \begin{eqnarray*}
598: S_j(T+1)=S_j(T) & + & \Delta_{j+1}(T) - \Xi_{j}(T),
599: \quad \mbox{for all } 2 \le j \le k \\
600: S_1(T+1)=S_1(T) & - & 1+\Delta_{2}(T) - \Xi_{1}(T),
601: \end{eqnarray*}
602: where $S_{k+1}(T) = 0$ and parameters $\Delta_j(T+1), \Xi_j(T+1)$ have the following distributions:
603: \begin{eqnarray*}
604: \Delta_j(T)& \stackrel{D}{=} & B(S_j(T),(j-1)/(n-T)), \\
605: \Xi_j(T)& \stackrel{D}{=} & B(S_j(T),j/(n-T)).
606: \end{eqnarray*}
607: for $j\geq 2$, and
608: \begin{eqnarray*}
609: \Xi_1(T+1)\stackrel{D}{=} B(S_1(T),(n-T-S_1(T))/(n-T)).
610: \end{eqnarray*}
611: }
612:
613: \noindent
614: Setting $T=t \cdot n$ and $S_j(T)=s_j(t) \cdot n$, we rescale this to form a system of differential equations:
615: \begin{eqnarray}
616: \frac{\ds_j}{\dt} & = & j \,\frac{s_{j+1}(t)-s_j(t)}{1-t}
617: \quad \mbox{for all } 2 \le j \le k \nonumber \\
618: \frac{\ds_1}{\dt} & = & \left( \frac{1-t-s_1(t)}{1-t} \right) \left( \frac{s_2(t)}{1-t} \right) - 1
619: \enspace .
620: \label{eq:sys}
621: \end{eqnarray}
622: Then Wormald's Theorem tells us that, for any constant $\delta > 0$, for all $t$ such that $s_1 > \delta$, \whp\ we have $S_j(t \cdot n) = s_j(t) \cdot n + o(n)$ where $s_j(t)$ is the solution to the system~\eqref{eq:sys}. With the initial conditions $s_j(0) = d_j$ for $1 \le j \le k$, a little work shows that this solution is
623: \begin{eqnarray}
624: s_j(t) & = & (1-t)^j \,\sum_{\ell = j}^k {\ell-1 \choose j-1} \,d_\ell t^{\ell-j}
625: \quad \mbox{for all } 2 \le j \le k \nonumber \\
626: s_1(t) & = & 1-t - (1-d_1) \exp\left(-\sum_{j=2}^k d_j t^{j-1} \right) \enspace .
627: \label{eq:soln}
628: \end{eqnarray}
629:
630: Note that $s_1(t)$ is continuous, $s_1(0)=d_1>0$, and $s_1(1) < 0$ since $d_1 < 1$. Thus $s_1(t)$ has at least one root in the interval $(0,1)$. Since $\PUR$ halts when there are no unit clauses, i.e., when $S_1(T)=0$, we expect the stage at which it halts. Thus the number of implied positive literals, to be $T=t_0 n + o(n)$ where $t_0$ is the smallest positive root of $s_1(t)=0$, or equivalently, dividing by $1-d_1$ and taking the logarithm, of Equation~\eqref{eq:1}.
631:
632: However, the conditions of Wormald's theorem do not allow us to run the differential equations all the way up to stage $t_0 n$. We therefore choose small constants $\eps, \delta > 0$ such that $s_1(t_0-\eps) = \delta$ and run the algorithm until stage $(t_0 - \eps) n$. At this point $(t_0-\eps) n$ literals are already implied, proving the lower bound of~\eqref{eq:implied}.
633:
634: To prove the upper bound of~\eqref{eq:implied}, recall that by assumption $t_0$ is a simple root of~\eqref{eq:1}, i.e., the second derivative of the left-hand size of~\eqref{eq:1} with respect to $t$ is nonzero at $t_0$. It is easy to see that this is equivalent to $\ds_1/\dt < 0$ at $t_0$. Since $\ds_1/\dt$ is analytic, there is a constant $c > 0$ such that $\ds_1/\dt < 0$ for all $t_0 - c \le t \le t_0 + c$. Set $\eps < c$; the number of literals implied during these stages is bounded above by a subcritical branching process whose initial population is \whp\ $\delta n + o(n)$, and by standard arguments we can bound its total progeny to be $\eps' n$ for any $\eps' > 0$ by taking $\delta$ small enough.
635: % CM: I shortened this but I think it's ok --- this argument is standard except for the observation
636: % that we need t_0 to be a simple root.
637: \remove{
638: To obtain the second part of inequality~\ref{eq:implied} we bound the
639: number of literals labeled as implied after stage $T_\delta$.
640: \begin{claim}
641: For every $\delta^{\prime}>0$ one can choose a constant $\delta >0$ such that
642: \whp\ the number of literals labeled implied {\em after} stage $T_\delta$
643: is at most $\delta' \cdot n$.
644: \end{claim}
645: We outline the proof of the previous claim (details are left for the full
646: version). Note that the function $s_1$ is monotonically decreasing in the
647: neighbourhood of $t_0$, since $s_1$ is analytical, $s_1(0)=d_1>0$ and $t_0$ is the smallest root of $s_1$. Therefore $s_1^{\prime}(t_0)\le 0$ and, since $t_0$ is not critical, $\lambda := s_1^{\prime}(t_0)< 0$. We infer that there exists a neighbourhood $(t_1,t_2)$ of $t_0$ such that
648: $\forall t\in (t_1,t_2), s_1^{\prime}(t)<\lambda/2$.
649:
650: Then the number of literals implied at stages between $t_1 n$ and $t_2 n$ is then dominated by a branching process with $\delta n$ initial individuals and expected birth rate $1+\lambda/2 < 1$. Choosing $\delta$ small enough we can make the number of individuals in the dominating branching process that are
651: born before extinction is \whp\ at most $\delta' \cdot n$.
652: }
653: \end{proof}
654:
655: It is easy to see that the backbone of implied positive literals is a uniformly random subset of $\{x_1,\ldots,x_n\}$ of size $N_{\boldd,n}$. Since $x_1$ is guaranteed to not be among the $d_1 n$ initially positive literals, the probability that $x_1$ is not in this backbone is
656: \[
657: %\Pr[H^{1,k}_{n,d} \mbox{ is SAT}] =
658: \frac{n-N_{\boldd,n}}{(1-d_1)\cdot n}.
659: \]
660: By completeness of positive unit resolution for Horn satisfiability, this is
661: precisely the probability that the $\phi$ is satisfiable.
662: Applying Lemma~\ref{lem:gen} and taking $\epsilon \goesto 0$ proves equation~\eqref{eq:prsat} and completes the proof of Theorem~\ref{thm:main}.
663:
664: We make several observations. First, if we set $k=2$ and take the limit $d_1 \to 0$,
665: Theorem~\ref{lem:gen} recovers Karp's result {\rm~\cite{Kar90}} on the size
666: of the reachable component of a random directed graph with mean out-degree
667: $d=d_2$, the root of $\ln (1-t) + d t = 0$.
668:
669: Secondly, as we will see below, the condition that $t_0$ is simple is essential. Indeed, for the 1-3-Horn-SAT model studied in~\cite{DV05}, the curve $\Gamma$ of discontinuities, where the probability of satisfiability drops in the ``waterfall'' of Figure~\ref{fig:1-3}, consists exactly of those $(d_1,d_3)$ where $t_0$ is a double root, which implies $\ds_1/\dt = 0$ at $t_0$.
670:
671: Finally, we note that Theorem~\ref{lem:gen} is very similar to Darling and Norris's work on
672: identifiability in random undirected hypergraphs~\cite{DN05}, where the number of hyperedges of length $j$ is Poisson-distributed with mean $\beta_j$. Their result reads
673: \[ \ln (1-t) + \sum_{j=1}^{k} j \beta_j t^{j-1} = 0 \enspace . \]
674: We can make this match~\eqref{eq:1} as follows. First, since each hyperedge of length $j$ corresponds to $j$ Horn clauses, we set $d_j = j \beta_j$ for all $j \ge 2$. Then, since edges are chosen with replacement in their model, the expected number of distinct clauses of length $1$ (i.e., positive literals) is $d_1 n$ where $d_1 = 1-\e^{-\beta_1}$.
675:
676:
677: \section{Application to $H_{n,\boldd}^2$}
678:
679: For $H_{n,\boldd}^2$, Equation~\eqref{eq:1} can rewritten
680: as $1-t=(1-d_1)\cdot e^{-d_2\cdot t}$. Denoting $y=d_2(t-1)$,
681: this implies
682: \[
683: y\cdot e^{y} = d_2(t-1)\cdot e^{d_2\cdot (t-1)}= -d_2(1-d_1)\cdot e^{-d_2\cdot t}\cdot e^{d_2\cdot (t-1)}=-(1-d_1)d_2 e^{-d_2}.
684: \]
685: Solving this yields
686: \[ t_0 = 1 + \frac{1}{d_2} W\bigl( -(1-d_1) d_2 \e^{-d_2} \bigr) \]
687: and substituting this into~\eqref{eq:prsat}
688: \remove{
689: \begin{equation}
690: \label{eq:prop2}
691: \Phi(d_1,d_2)
692: = \lim_{n \to \infty} \Pr[H^2_{n,\boldd} \mbox{ is satisfiable}] =
693: -\frac{W\bigl( -(1-d_1) d_2 \e^{-d_2} \bigr)}{(1-d_1)d_2},
694: \end{equation}
695: }
696: proves Equation~\eqref{eq:prop2} and Proposition~\ref{prop:2}. In Figure~\ref{1-2-0.1}
697: %figures~\ref{1-2-0.1} and~\ref{1-2-0.01}
698: we plot the probability of satisfiability $\Phi(d_1,d_2)$ as a function of $d_2$ for $d_1=0.1$ and compare it with the experimental results of~\cite{DV05}; the agreement is excellent.
699:
700: \begin{figure}[tbh]
701: \begin{center}
702: \begin{minipage}[t]{2.2 in}
703: \begin{center}
704: \psfig{figure=fig3.eps,height=50truemm,width=50truemm}
705: \end{center}
706: \end{minipage}
707: \begin{minipage}[t]{2.3 in}
708: \begin{flushright}
709: \hspace{0.5in}\psfig{figure=01facts.ps,height=50truemm,width=45truemm}
710: \end{flushright}
711: \end{minipage}
712: \caption{The probability of satisfiability for 1-2-Horn formulae as a function
713: of $d_2$, where $d_1 = 0.1$. Left, our analytic results; right, the experimental data of~\cite{DV05}.}
714: \label{1-2-0.1}
715: \end{center}
716: \end{figure}
717:
718: %\begin{figure*}[tbh]
719: %\begin{minipage}[t]{2.2in}
720: %\begin{center}
721: %\psfig{figure=fig3.eps,height=60truemm,width=60truemm}
722: %\end{center}
723: %\end{minipage}
724: %\begin{minipage}[t]{2.3in}
725: %\begin{flushright}
726: %\hspace{0.5in}\psfig{figure=fixedfacts.ps,height=60truemm,width=55truemm}
727: %\end{flushright}
728: %\end{minipage}
729: %\caption{The probability a satisfiability for 1-2-Horn formulae, where $d_1 = 0.1, 0.01, 0.001,$ and $0.0001$. Compare to Fig.3 of~\cite{
730: %demopoulos:vardi:horn} (shown on the right-hand side). }
731: %\label{1-2-0.01}
732: %\end{figure*}
733:
734:
735:
736: \section{A continuous-discontinuous phase transition for
737: $H_{n,d_1,0,d_3}^3$}
738:
739: For the random model $H_{n,d_1,0,d_3}^3$ studied in~\cite{DV05},
740: an analytic solution analogous to~\eqref{eq:prop2} does not seem to exist.
741: Let us, however, rewrite~\eqref{eq:1} as
742: \begin{equation}
743: \label{eq:f}
744: 1-t = f(t) := (1-d_1) \e^{-d_3 t^2} \enspace .
745: \end{equation}
746: We claim that for some values of $d_1$ and $d_3$ there is a phase transition in the roots of~\eqref{eq:f}. For instance, consider the plot of $f(t)$ shown in Figure~\ref{first-f} for $d_1 = 0.1$ and $d_3 = 3$. Here $f(t)$ is tangent to $1-t$, so there is a bifurcation as we vary either parameter; for $d_3 = 2.9$, for instance, $f(t)$ crosses $1-t$ three times and there is a root of~\eqref{eq:f} at $t=0.185$, but for $d_3 = 3.1$ the unique root is at $t=0.943$. This causes the probability of satisfiability to jump discontinuously but from $0.905$ to $0.064$. The set of pairs $(d_1,d_3)$ for which $f(t)$ is tangent to $1-t$ is exactly the curve $\Gamma$ on which the smallest positive root $t_0$ of~\eqref{eq:1} or~\eqref{eq:f} is a double root, giving the ``waterfall'' of Figure~\ref{fig:1-3}.
747:
748: \begin{figure}[tbh]
749: \begin{center}
750: \begin{minipage}[t]{3 in}
751: \begin{center}
752: \psfig{figure=d1.eps,height= 60 truemm,width= 60 truemm}
753: \end{center}
754: \end{minipage}
755: \begin{minipage}[t]{3 in}
756: \begin{flushright}
757: \hspace{0.25in}\psfig{figure=horntrans.eps,height=60 truemm, width= 65 truemm}
758: \end{flushright}
759: \end{minipage}
760: \caption{Left, the function $f(t)$ of~\eqref{eq:f} when $d_1 = 0.1$ and $d_3 = 3$.
761: Right, the probability of satisfiability $\Phi(d_1,d_3)$ with $d_1$ equal to
762: $0.15$ (continuous), $0.1756$ (critical), and $0.2$ (discontinuous).}
763: \label{first-f}
764: \end{center}
765: \end{figure}
766:
767:
768: %\begin{figure}[ht]\label{first-f}
769: %\centerline{
770: %\psfig{figure=d1.eps,width=2in}
771: %}
772: %\caption{The function $f(t)$ of~\eqref{eq:f} when $d_1 = 0.1$ and $d_3 = 3$.}
773: %\label{fig:tangent}
774: %\end{figure}
775:
776: To find where this transition takes place, we set $f' = -1$, yielding $f(t) = 1/(2 d_3 t)$. Setting this to $1-t$ and solving for $t$ gives
777: \begin{equation}
778: \label{eq:d1a}
779: d_1 = 1 - \frac{\e^{d_3 t^2}}{2 d_3 t}
780: \end{equation}
781: where
782: \begin{equation}
783: \label{eq:t}
784: t = \frac{1}{2} \left( 1 - \sqrt{1-\frac{2}{d_3}} \right)
785: \end{equation}
786: Substituting~\eqref{eq:t} in~\eqref{eq:d1a} and simplifying gives~\eqref{eq:gamma},
787: \remove{
788: \begin{equation}
789: \label{eq:d1}
790: d_1 = 1 - \frac{\exp\left( \frac{1}{4} \left( \sqrt{d_3} - \sqrt{d_3-2} \right)^2 \right)}
791: {d_3 - \sqrt{d_3 (d_3-2)}},
792: \end{equation}
793: }
794: proving Proposition~\ref{prop:3}.
795:
796: %We plot this function in Figure~\ref{critical:curve}(right).
797: %It tracks closely the location of the experimental ``waterfall''
798: %(Figure~\ref{fig:1-3}).
799: The fact that $d_1$ is only real for $d_3 \ge 2$ explains why $\Gamma$
800: ends at $d_3 = 2$. At this extreme case we have
801: \[ d_1 = 1-\frac{\sqrt{\e}}{2} \approx 0.1756 \;\mbox{ and }\;
802: \frac{\partial d_1}{\partial d_3} = - \frac{\sqrt{\e}}{8} \enspace . \]
803: What happens for $d_3 < 2$? In this case, there are no real $t$ for which
804: $f'(t) = -1$, so the kind of tangency displayed in
805: Figure~\ref{first-f} cannot happen.
806: In that case,~\eqref{eq:f} (and equivalently~\eqref{eq:1}) has a unique
807: solution $t$, which varies continuously with $d_1$ and $d_3$, and therefore
808: the probability of satisfiability $\Phi(d_1,d_3)$ is continuous as well.
809: To illustrate this, in the right part of Figure~\ref{first-f} we plot
810: $\Phi(d_1,d_3)$ as a function of $d_3$ with three values of $d_1$.
811: For $d_1=0.15$, $\Phi$ is continuous; for $d_1 = 0.2$, it is discontinuous;
812: and for $d_1 = 0.1756...$, the critical value at the second-order transition,
813: it is continuous but has an infinite derivative at $d_3=2$.
814:
815: \remove{
816: The result in Theorem~\ref{thm:main} also recovers other behavior
817: experimentally observed in~\cite{DV05} for random 1-3-Horn-SAT:
818: for certain combinations of the parameter $(d_1,d_3)$,
819: the probability of satisfiability has a coarse threshold,
820: but the transition has a discontinuity that is
821: quite pronounced. For instance, in Figure~\ref{fig:contour},
822: we present the contour plots for the satisfiability of a random 1-3 formula
823: in the $(d_1,d_3)$ plane, and compare it to the contour plot obtained
824: experimentally in~\cite{DV05}. As we can see, the agreement is very good.
825: }
826:
827: %\begin{figure*}[tbh]
828: %\begin{center}
829: %\psfig{figure=1-3.ps, angle = -90, width=80 truemm}
830: %\label{1-3-compare}
831: %\end{center}
832: %\caption{The probability of satisfiability of a random 1-3-Horn-SAT formula with
833: %$d1=0.1$}
834: %\end{figure*}
835:
836:
837: %\begin{figure}[tbh]\label{fig:contour}
838: %\centerline{
839: %\psfig{figure=contour.ps,width=4in}
840: %}
841: %\caption{Something}
842: %\end{figure}
843:
844: \iffalse
845: \begin{figure}[ht]
846: \begin{center}
847: \begin{minipage}[t]{3.0in}
848: \begin{center}
849: \psfig{figure=1-3.ps, angle = -90, width=80 truemm}
850: \end{center}
851: \end{minipage}
852: \begin{minipage}[t]{3.0in}
853: \begin{center}
854: \psfig{figure=critical.ps,angle = -90,width= 80truemm}
855: \end{center}
856: \end{minipage}
857: \caption{(a) The probability of satisfiability of a random 1-3 Horn-SAT
858: formula with $d_1=0.1$, (b) The discontinuity curve}
859: \label{critical:curve}
860: \label{1-3-compare}
861: \end{center}
862: \end{figure}
863: \fi
864:
865:
866: %moshe: to save space for now
867: %\section{Acknowledgments}
868: %We thank Mark Newman for helpful conversations.
869: %This work has been supported by the U.S. Department of Energy
870: %under contract W-705-ENG-36 and by NSF grants PHY-0200909, EIA-0218563,
871: %and CCR-0220070.
872:
873: %\bibliographystyle{alpha}
874:
875: \newcommand{\etalchar}[1]{$^{#1}$}
876:
877: {\small
878: \begin{thebibliography}{MZK{\etalchar{+}}99}
879:
880: \bibitem{achreview}
881: D.~Achlioptas.
882: \newblock Lower Bounds for Random 3-{SAT} via Differential Equations.
883: \newblock {\em Theoretical Computer Science} 265 (1-2), 159--185, 2001.
884:
885: \bibitem{ACIM01}
886: D.~Achlioptas, A.~Chtcherba, G.~Istrate, and C.~Moore.
887: \newblock The phase transition in 1-in-$k$ {SAT} and {NAE} 3-{SAT}.
888: \newblock In {\em Proc.~12th ACM-SIAM Symp. on Discrete Algorithms}, 721--722, 2001.
889:
890: \bibitem{AKKK01}
891: D. Achlioptas, L.M. Kirousis, E. Kranakis, and D. Krizanc.
892: \newblock Rigorous results for random $(2+p)$-SAT.
893: \newblock {\em Theor. Comput. Sci.} 265(1-2): 109-129 (2001).
894:
895: \bibitem{BCD01}
896: T.~Bench-Capon and P.~Dunne.
897: \newblock A sharp threshold for the phase transition of a restricted
898: satisfiability problem for {H}orn clauses.
899: \newblock {\em Journal of Logic and Algebraic Programming}, 47(1):1--14, 2001.
900:
901: \bibitem{BDFN92}
902: J. J. Binney, N. J. Dowrick, A. J. Fisher and M. E. J. Newman.
903: {\em The Theory of Critical Phenomena.} Oxford University Press (1992).
904:
905: \bibitem{Bol85}
906: B.~Bollob\'{a}s.
907: \newblock {\em Random Graphs}.
908: \newblock Academic Press, 1985.
909:
910: \bibitem{CDMM03}
911: S.~Cocco, O.~Dubois, J.~Mandler, and R.~Monasson.
912: \newblock Rigorous decimation-based construction of ground pure states
913: for spin glass models on random lattices.
914: \newblock {\em Phys. Rev. Lett.}, 90, 2003.
915:
916: \bibitem{CR92}
917: V.~Chv\'{a}tal and B.~Reed.
918: \newblock Mick gets some (the odds are on his side).
919: \newblock In {\em Proc.~33rd IEEE Symp. on Foundations of Computer
920: Science}, IEEE Comput. Soc. Press, 620--627, 1992.
921:
922: %moshe: to save space
923: %\bibitem{CDSSV00}
924: %C.~Coarfa, D.D. Demopoulos, A.~San~Miguel Aguirre, D.~Subramanian, and
925: %M.Y. Vardi.
926: %\newblock Random 3-sat -- the plot thickens.
927: %\newblock In R.~Dechter, editor, {\em Proc. Principles and Practice of
928: %Constraint Programming (CP'2000)}, Lecture Notes in Computer Science
929: %1894, 143--159, 2000.
930:
931: \bibitem{CA96}
932: J.~M. Crawford and L.~D. Auton.
933: \newblock Experimental results on the crossover point in random 3-{SAT}.
934: \newblock {\em Artificial Intelligence}, 81(1-2):31--57, 1996.
935:
936: \bibitem{DG84}
937: W.~F. Dowling and J.~H. Gallier.
938: \newblock Linear-time algorithms for testing the satisfiability of
939: propositional {H}orn formulae.
940: \newblock {\em Logic Programming. (USA) ISSN: 0743-1066}, 1(3):267--284,
941: 1984.
942:
943: \bibitem{DBM00}
944: O.~Dubois, Y.~Boufkhad, and J.~Mandler.
945: \newblock Typical random 3-{SAT} formulae and the satisfiability theshold.
946: \newblock In {\em Proc.~11th ACM-SIAM Symp. on Discrete Algorithms}, 126--127, 2000.
947: %\newblock {\em Electronic Colloquium on Computational Complexity} {\bf 10(7)} (2003).
948:
949: \bibitem{DM02}
950: O.~Dubois and J.~Mandler.
951: \newblock The 3-{XORSAT} threshold.
952: \newblock In {\em Proc.~43rd IEEE Symp. on Foundations of Computer Science}, 769--778, 2002.
953:
954: \bibitem{DN05}
955: R.~Darling and J.R.~Norris.
956: \newblock Structure of large random hypergraphs.
957: \newblock {\em Annals of Applied Probability}, 15(1A), 2005.
958:
959: \bibitem{DV05}
960: D.~Demopoulos and M.~Vardi.
961: \newblock The phase transition in random 1-3 {H}ornsat problems.
962: \newblock In A.~Percus, G.~Istrate, and C.~Moore, editors, {\em Computational
963: Complexity and Statistical Physics}, Santa Fe Institute Lectures in the
964: Sciences of Complexity. Oxford University Press, 2005.
965: \newblock Available at {\tt http://www.cs.rice.edu/$^\sim$vardi/papers/}.
966:
967: \bibitem{ER60}
968: P.~Erd\"{o}s and A.~R\'{e}nyi.
969: \newblock On the evolution of random graphs.
970: \newblock {\em Publications of the Mathematical Institute of the Hungarian Academy of Science}, 5:17--61, 1960.
971:
972: \bibitem{Fri99}
973: E.~Friedgut.
974: \newblock Necessary and sufficient conditions for sharp threshold of graph
975: properties and the $k$-{SAT} problem.
976: \newblock {\em J. Amer. Math. Soc.}, 12:1917--1054, 1999.
977:
978: \bibitem{Goe96}
979: A.~Goerdt.
980: \newblock A threshold for unsatisfiability.
981: \newblock {\em J. Comput. System Sci.}, 53(3):469--486, 1996.
982:
983: \bibitem{HajiaSorkin}
984: M.~Hajiaghayi and G.B.~Sorkin.
985: \newblock The satisfiability threshold for random 3-SAT is at least 3.52.
986: \newblock IBM Technical Report , 2003.
987:
988: \bibitem{HW94}
989: T.~Hogg and C.~P. Williams.
990: \newblock The hardest constraint problems: A double phase transition.
991: \newblock {\em Artificial Intelligence}, 69(1-2):359--377, 1994.
992:
993: \bibitem{Ist02}
994: G.~Istrate.
995: \newblock The phase transition in random {H}orn satisfiability and its
996: algorithmic implications.
997: \newblock {\em Random Structures and Algorithms}, 4:483--506, 2002.
998:
999: \bibitem{Ist04}
1000: G.~Istrate.
1001: \newblock On the satisfiability of random $k$-{H}orn formulae.
1002: \newblock In P.~Winkler and J.~Nesetril, editors, {\em Graphs, Morphisms and
1003: Statistical Physics}, volume~64 of {\em AMS-DIMACS Series in Discrete
1004: Mathematics and Theoretical Computer Science}, 113--136, 2004.
1005:
1006: \bibitem{Kar90}
1007: R.~Karp.
1008: \newblock The transitive closure of a random digraph.
1009: \newblock {\em Random Structures and Algorithms}, 1:73--93, 1990.
1010:
1011: \bibitem{KKL}
1012: A.~Kaporis, L.~M. Kirousis, and E.~Lalas.
1013: \newblock Selecting complementary pairs of literals.
1014: \newblock In {\em Proceedings of LICS'03 Workshop
1015: on Typical Case Complexity and Phase Transitions}, June 2003.
1016:
1017: \bibitem{Mak87}
1018: J.~A. Makowsky.
1019: \newblock Why {H}orn formulae matter in {C}omputer {S}cience: Initial
1020: structures and generic examples.
1021: \newblock {\em JCSS}, 34(2-3):266--292, 1987.
1022:
1023: \bibitem{MZ02}
1024: M.~M\'{e}zard and R.~Zecchina.
1025: \newblock Random k-satisfiability problem: from an analytic solution to an efficient algorithm.
1026: \newblock {\em Phys. Rev. E}, 66:056126, 2002.
1027:
1028: \bibitem{MPZ02}
1029: M.~M\'{e}zard, G.~Parisi, and R.~Zecchina.
1030: \newblock Analytic and algorithmic solution of random satisfiability problems.
1031: \newblock {\em Science}, 297:812--815, 2002.
1032:
1033: \bibitem{MZKST99}
1034: R.~Monasson, R.~Zecchina, S.~Kirkpatrick, B.~Selman, and L.~Troyansky.
1035: \newblock $2+p$-{SAT}: Relation of typical-case complexity to the nature of the
1036: phase transition.
1037: \newblock {\em Random Structures and Algorithms}, 15(3--4):414--435, 1999.
1038:
1039: \bibitem{SML96}
1040: B.~Selman, D.~G. Mitchell, and H.~J. Levesque.
1041: \newblock Generating hard satisfiability problems.
1042: \newblock {\em Artificial Intelligence}, 81(1-2):17--29, 1996.
1043:
1044: \bibitem{SK96}
1045: B.~Selman and S.~Kirkpatrick.
1046: \newblock Critical behavior in the computational cost of satisfiability testing.
1047: \newblock {\em Artificial Intelligence}, 81(1-2):273--295, 1996.
1048:
1049: \bibitem{VW86a}
1050: M.Y. Vardi and P.~Wolper.
1051: \newblock Automata-Theoretic Techniques for Modal Logics of Programs
1052: \newblock {\em J. Computer and System Science} 32:2(1986), 181--221, 1986.
1053:
1054: \bibitem{VW86b}
1055: M.Y. Vardi and P.~Wolper.
1056: \newblock An automata-theoretic approach to automatic program
1057: verification (preliminary report).
1058: \newblock In {\em Proc.~1st IEEE Symp. on Logic in Computer Science}, 332--344, 1986.
1059:
1060: \bibitem{Wor95}
1061: N.~Wormald.
1062: \newblock Differential equations for random processes and random graphs.
1063: \newblock {\em Annals of Applied Probability}, 5(4):1217--1235, 1995.
1064:
1065: %\bibitem{Wor99}
1066: %N.~C. Wormald.
1067: %\newblock The differential equation method for random graph processes and greedy algorithms.
1068: %\newblock In M.~Karonski and H.J. Proemel, editors, {\em Lectures on Approximation and Randomized Algorithms}, 73--155. PWN, Warsaw, 1999.
1069:
1070: \end{thebibliography}
1071: }
1072: \end{document}
1073: