1: \documentclass[11pt]{article}
2: \usepackage{amsfonts,latexsym,amssymb,epsfig}
3: \usepackage{amsmath,amsthm,amstext}
4: \usepackage{fullpage,flafter}
5: \parindent 0cm
6: \parskip 0.2cm
7:
8: \newcommand{\shlomo}[1]{}
9: \newcommand{\avner}[1]{}
10:
11:
12: \renewcommand{\topfraction}{.9}
13: \renewcommand{\bottomfraction}{.9}
14: \renewcommand{\textfraction}{.9}
15:
16: \begin{document}
17: \bibliographystyle{plain}
18: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
19: \newtheorem{theorem}{Theorem}
20: \newtheorem{proposition}[theorem]{Proposition}
21: \newtheorem{corollary}[theorem]{Corollary}
22: \newtheorem{note}[theorem]{Note}
23: \newtheorem{lemma}[theorem]{Lemma}
24: \newtheorem{definition}[theorem]{Definition}
25: \newtheorem{observation}[theorem]{Observation}
26: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
27: \newcounter{fignum}
28: \newcommand{\figlabel}[1]
29: {Figure \refstepcounter{fignum}\arabic{fignum}\label{#1}}
30: \newcommand{\ignore}[1]{}
31: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
32: \font\boldsets=msbm10
33: \def\Z{{\hbox{\boldsets Z}}}
34: \def\R{{\hbox{\boldsets R}}}
35: \def\half{\frac 1 2}
36: \def\F2{{\{0,1\}}}
37: \def\A{{\cal A}}
38: \def\K{{\cal K}}
39: \def\KM{{{\cal K}^{-}}}
40: \def\maxk{{20000}}
41: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
42: % log-like functions
43: \def \mixx {\mbox {mix}}
44: \newcommand{\rank} {\mbox {rank}}
45: \newcommand{\schreier} {\mbox {sc}}
46: \newcommand{\Oh} {\tilde{O}}
47: \newcommand{\G} {{\cal F}}
48: \newcommand{\gr}[9]{
49: \fbox{$\begin{array}{lll}#1\\#4\\#7	\end{array}$}
50: }
51: \def\hy{\hbox{-}\nobreak\hskip0pt} %write: $\alpha$\hy coloring
52: \newcommand{\SB}{\{\,}%
53: \newcommand{\SM}{\;{:}\;}%
54: \newcommand{\SE}{\,\}}%
55: \newcommand{\NP}{\text{\normalfont NP}}
56: \newcommand{\CNF}[1]{#1\text{\normalfont-CNF}}
57: \newcommand{\MU}{\text{\normalfont MU}}
58: \newcommand{\SAT}{\text{\normalfont SAT}}
59: \newcommand{\UNSAT}{\text{\normalfont UNSAT}}
60: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
61: \title{Families of unsatisfiable $k\CNF$ formulas with few occurrences per
62: variable}
63: \author{
64: \parbox{8cm}{\centering Shlomo Hoory\\[4pt]
65: \small Department of Computer Science\\
66: \small University of Toronto\\
67: Toronto, Ontario, Canada\\
68: \small\texttt{shlomoh@cs.toronto.edu}}
69: \parbox{8cm}{\centering Stefan Szeider\\[4pt]
70: \small Department of Computer Science\\
71: \small University of Durham\\
72: \small Durham, England, UK\\
73: \small \texttt{stefan.szeider@durham.ac.uk}}
74: }
75:
76: \maketitle
77:
78: \begin{abstract}
79: \sloppypar\noindent $(k,s)$-SAT is the satisfiability problem
80: restricted to instances where each clause has exactly $k$
81: literals and every variable occurs at most $s$ times. It is known
82: that there exists a function $f$ such that for
83: $s\leq f(k)$ all $(k,s)$-SAT instances are satisfiable, but
84: $(k,f(k)+1)$-SAT is already $\NP$\hy complete ($k\geq 3$).
85: The best known lower and upper bounds on $f(k)$ are $\Omega(2^k/k)$
86: and $O(2^k/k^\alpha)$, where $\alpha=\log_3 4 - 1 \approx 0.26$.
87: We prove that $f(k) = O(2^k \cdot \log k/k)$, which is tight up to
88: a $\log k$ factor.
89: \end{abstract}
90:
91: \section{Introduction}
92:
93: We consider CNF formulas represented as sets of clauses,
94: where each clause is a set of literals.
95: A literal is either a variable or a negated variable.
96: Let $k,s$ be fixed positive integers. We denote by $\CNF{(k,s)}$ the
97: set of formulas $F$ where every clause
98: of $F$ has \emph{exactly} $k$ literals and each variable occurs in
99: \emph{at most} $s$ clauses of $F$. We denote the sets of satisfiable
100: and unsatisfiable formulas by $\SAT$ and $\UNSAT$, respectively.
101:
102: It was observed by Tovey \cite{Tovey84} that all formulas in
103: $\CNF{(3,3)}$ are satisfiable, and that the satisfiability problem
104: restricted to $\CNF{(3,4)}$ is already $\NP$\hy complete. This was
105: generalized in Kratochv\'{\i}l, et al.\ \cite{KratochST93} where it is
106: shown that for every $k\geq 3$ there is some integer $s=f(k)$ such that
107: \begin{enumerate}
108: \item all formulas in $\CNF{(k,s)}$ are satisfiable, and
109: \item $(k,s+1)$-SAT, the SAT problem
110: restricted to $\CNF{(k,s+1)}$, is already $\NP$\hy complete.
111: \end{enumerate}
112: The function $f$ can be defined for $k \geq 1$ by the equation
113: \[f(k):=\max \SB s \SM \CNF{(k,s)}\cap \UNSAT=\emptyset \SE.\]
114: Exact values of $f(k)$ are only known for $k \leq 4$.
115: It is easy to verify that $f(1)=1$ and $f(2)=2$.
116: It follows from
117: \cite{Tovey84} that $f(3)=3$ and $f(k)\geq k$ in general.
118: Also, by~\cite{Stribrna94}, we know that $f(4)=4$.
119:
120: Upper and lower bounds for $f(k)$, $k=5,\ldots,9$, have been obtained
121: in~\cite{Dubois90,Stribrna94,BermanKarpinskiScott03,HoorySzeider04}.
122: For larger values of $k$, the best known lower bound,
123: a consequence of Lov\'asz Local Lemma,
124: is due to Kratochv\'{\i}l et al.~\cite{KratochST93}:
125: \begin{eqnarray}\label{lowerbound}
126: f(k) \geq \left\lfloor \frac{2^k}{e k} \right\rfloor.
127: \end{eqnarray}
128: The best known upper bound, due to Savick{\'y} and Sgall~\cite{SavickySgall00},
129: is given by
130: \begin{eqnarray}\label{savupperbound}
131: f(k) \leq O\left(\frac{2^k}{k^\alpha}\right),
132: \end{eqnarray}
133: where $\alpha=\log_3 4 - 1 \approx 0.26$.
134:
135: In this paper we asymptotically improve upon
136: (\ref{savupperbound}), and show
137: \begin{eqnarray}\label{ourupperbound}
138: f(k) = O\left(\frac{2^k \log k}{k}\right).
139: \end{eqnarray}
140: Our result reduces the gap between the upper and lower bounds to a $\log k$
141: factor.
142: It turns out that the construction yielding the upper bound
143: (\ref{ourupperbound}) can be generalized. We present a class of $k$-CNF
144: formulas, that is amenable to an exhaustive search using dynamic programming.
145: %We are able to exhibit
146: This enables us to calculate
147: upper bounds on $f(k)$ for values up to $k=\maxk$ improving upon
148: the bounds provided by the constructions underlying
149: (\ref{savupperbound}) and (\ref{ourupperbound}).
150:
151: The remainder of the paper is organized as follows.
152: In Section~\ref{constructI:section}, we start with a simple construction
153: that already provides an $O(2^k \log^2 k/k)$ upper bound on $f(k)$.
154: In Section~\ref{constructII:section} we refine our construction
155: and obtain the upper bound (\ref{ourupperbound}).
156: In the last section we describe the more general construction and
157: the results obtained using computerized search.
158:
159: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
160:
161: \section {The first construction}\label{constructI:section}
162:
163: We denote by $\K(x_1,\ldots,x_k)$ the complete unsatisfiable $k\CNF$ formula
164: on the variables $x_1,\ldots,x_k$. This formula consists of all $2^k$
165: possible clauses. Let
166: $\KM(x_1,\ldots,x_k) = \K(x_1,\ldots,x_k) \setminus \{\{ x_1,\ldots,x_k \}\}$.
167: The only satisfying assignment for $\KM(x_1,\ldots,x_k)$ is
168: the all-False-assignment.
169: Also, for two CNF formulas $F_1$ and $F_2$ on disjoint sets of variables,
170: define their product $F_1 \times F_2$ as
171: $\{ c_1 \cup c_2 : c_1 \in F_1 \mbox{ and } c_2 \in F_2 \}$.
172: Note that the satisfying assignments for $F_1 \times F_2$ are assignments
173: that satisfy $F_1$ or $F_2$.
174: In what follows, all logarithms are to the base of $2$.
175:
176: \def\kl{{\lfloor k/l \rfloor}}
177: \def\card{\sharp}
178:
179: \begin{lemma}\label{lemma1}
180: $f(k)
181: \leq 2^k \cdot \min_{1\leq l \leq k} \left( (1-2^{-l})^{\kl} + 2^{-l}\right)$.
182: \end{lemma}
183:
184: \begin{proof}
185:
186: We prove the lemma by constructing an unsatisfiable $(k,s)\CNF$ formula $F$
187: where $s=2^k \cdot ( (1-2^{-l})^{\kl} + 2^{-l})$.
188: Let $k,l$ be two integers such that $1\leq l \leq k$, and
189: let $u=\kl$ and $v=k-l \cdot u$.
190: Define the formula $F$ as the union
191: $F = F_0 \cup F_1 \cup \ldots \cup F_u$, where:
192: \begin{eqnarray*}
193: F_0
194: &=&
195: \K(z_1,\ldots,z_v) \times \prod_{i=1}^u \KM(x_1^{(i)},\ldots,x_l^{(i)}),\\
196: F_i
197: &=&
198: \K(y_1^{(i)},\ldots,y_{k-l}^{(i)})
199: \times \{ \{ x_1^{(i)},\ldots,x_l^{(i)} \} \}
200: \quad \mbox{for }i=1,\ldots,u.
201: \end{eqnarray*}
202:
203: Therefore, $F$ is a $k\CNF$ formula with $n$ variables and $m$ clauses, where
204: \begin{eqnarray}
205: n &=& k + u \cdot (k-l) \leq l + k^2/l,\label{vars}\\
206: m &=& 2^v \cdot (2^l-1)^u + u \cdot 2^{k-l}
207: = 2^k \cdot \left( (1-2^{-l})^\kl + \kl \cdot 2^{-l}\right).\label{clauses}
208: \end{eqnarray}
209:
210: To see that $F$ is unsatisfiable observe that any assignment satisfying $F_0$
211: must set all the variables $x_1^{(i)},\ldots,x_l^{(i)}$ to False for some $i$.
212: On the other hand, any satisfying assignment to $F_i$ must set at least one
213: of the variables $x_1^{(i)},\ldots,x_l^{(i)}$ to True.
214:
215: To bound the number of occurrences of a variable note that
216: the variables $z_j, y_j^{(i)}$, and $x_j^{(i)}$ occur
217: $|F_0|, |F_i|$, and $|F_0|+|F_i|$ times, respectively.
218: Since $|F_0| = 2^v \cdot (2^l-1)^u = 2^k \cdot (1-2^{-l})^\kl$
219: and $|F_i|=2^{k-l}$, we get the required result.
220:
221: \end{proof}
222:
223: For $k \geq 4$, let $l$ be the largest integer satisfying
224: $2^l \leq k \cdot \log e / \log^2 k$.
225: If follows that
226: \begin{eqnarray*}
227: (1-2^{-l})^{\kl} \leq \exp(-2^{-l} \cdot \kl)
228: &\leq&
229: \exp(-\frac{\log^2 k}{k \log e} \cdot (\frac{k}{l}+1))\\
230: &\leq&
231: \frac{1}{\sqrt e} \cdot \exp(-\frac{\log^2 k}{l \log e})
232: \leq
233: \frac{1}{\sqrt e} \cdot \exp(-\frac{\log k}{\log e})
234: =
235: \frac{1}{k\sqrt e},
236: \end{eqnarray*}
237: where the last inequality follows from the fact that $l \leq \log k$ for
238: $k \geq 4$.
239: Therefore, by Lemma~\ref{lemma1} there exists an unsatisfiable $k\CNF$ formula
240: $F$ where the number of
241: occurrences of variables is bounded by
242: \begin{eqnarray*}
243: 2^k \cdot (\frac{1}{k\sqrt e} + \frac{2 \log^2 k}{k \log e}).
244: \end{eqnarray*}
245: It may be of interest that by (\ref{vars}) and (\ref{clauses}),
246: the number of clauses in $F$ is $O(2^k \cdot \log k)$
247: and the number of variables is $O(k^2/\log k)$.
248:
249: \begin{corollary}
250: $f(k) = O(2^k\cdot \log^2 k/k).$
251: \end{corollary}
252:
253: \section {A better upper bound}\label{constructII:section}
254:
255: To simplify the subsequent discussion,
256: let us fix a value of $k$. We will only be concerned
257: with CNF formulas $F$ that have clauses of size at most $k$.
258: We call a clause of size less that $k$ an {\em incomplete} clause
259: and denote $F' = \{ c \in F : |c| < k \}$.
260: A clause of size $k$ is a {\em complete} clause,
261: and we denote $F'' = \{ c \in F : |c| = k \}$.
262:
263: \begin{lemma}\label{lemma2}
264: $f(k) \leq
265: \min\{ 2^{k-l+1} : l \in \{0,\ldots,k\} \mbox{ and }
266: l \cdot 2^l \leq \log e \cdot (k-2l) \}$.
267: \end{lemma}
268: \begin{proof}
269:
270: Let $l$ be in $\{0,\ldots,k\}$, satisfying $l \cdot 2^l \leq \log e
271: \cdot (k-2l)$, and set $s=2^{k-l+1}$. We will define a sequence of
272: CNF formulas, $F_0,\ldots,F_l$. We require that (i) $F_j$ is
273: unsatisfiable, (ii) $F'_j$ is a $(k-l+j)\CNF$ formula, (iii) $|F'_j|
274: \leq 2^{k-l}$, and that (iv) the maximal number of occurrences of a
275: variable in $F_j$ is bounded by $s$. It follows that $F_l$ is an
276: unsatisfiable $(k,s)$-CNF formula, implying the claimed upper bound.
277:
278: Set $k_j=k-l+j$ and $u_j = \lfloor (k-l+j)/(l-j+1)\rfloor$. We
279: proceed by induction on $j$. For $j=0$, we define $F_0 =
280: \K(x_1,\ldots,x_{k-l})$. It can be easily verified that $F_0$
281: satisfies the above four requirements. For $j>0$, assume a formula
282: $F_{j-1}$ on the variables $y_1,\ldots,y_n$, satisfying the
283: requirements. We define the formula $F_j = \bigcup_{i=0}^{u_j}
284: F_{j,i}$ as follows:
285: \begin{eqnarray}
286: F_{j,0} &=&
287: \K(z_1,\ldots,z_{k_j - u_j \cdot (l-j+1)}) \times
288: \prod_{i=1}^{u_j} \KM(x_1^{(i)},\ldots,x_{l-j+1}^{(i)}),\label{FPdef}\\
289: F_{j,i} &=&
290: F'_{j-1}(y_1^{(i)},\ldots,y_n^{(i)})
291: \times \{ \{ x_1^{(i)},\ldots,x_{l-j+1}^{(i)} \} \}
292: \cup F''_{j-1}(y_1^{(i)},\ldots,y_n^{(i)})
293: \quad \mbox{for }i=1,\ldots,{u_j}.
294: \end{eqnarray}
295:
296: It is easy to check that $F'_j$ is a $(k-l+j)\CNF$ formula.
297: To see that $F_j$ is unsatisfiable, observe that any assignment
298: satisfying $F_{j,0}$, must set all the variables
299: $x_1^{(i)},\ldots,x_{l-j+1}^{(i)}$ to False for some $i$.
300: On the other hand, for any satisfying assignment to $F_{j,i}$,
301: at least one of the variables $x_1^{(i)},\ldots,x_{l-j+1}^{(i)}$ must be set
302: to True.
303:
304: Let us consider the number of occurrences of a variable in $F_j$.
305: Consider first the $y$-variables.
306: These variables occur only in the $u_j$ duplicates of $F_{j-1}$
307: and therefore occur the same number of times as in $F_{j-1}$,
308: which is bounded by $s$ by induction.
309: The number of occurrences of an $x$- or $z$-variable is
310: $|F'_{j-1}|+|F_{j,0}|$ or $|F_{j,0}|$ respectively.
311: By induction, $|F'_{j-1}| \leq 2^{k-l}$.
312: Also,
313: \begin{eqnarray*}
314: |F_j'|
315: &=&|F_{j,0}|
316: = 2^{k_j - u_j \cdot (l-j+1)} \cdot (2^{l-j+1}-1)^{u_j}
317: = 2^{k_j} \cdot (1-2^{-l+j-1})^{u_j}\\
318: &\leq& 2^{k-l+j} \cdot \exp(-2^{-l+j-1} \cdot u_j)
319: \leq 2^{k-l+j} \cdot \exp(-2^{-l+j-1} \cdot (k-2l)/l).
320: \end{eqnarray*}
321: Taking logarithms, we get
322: \begin{eqnarray*}
323: \log|F_{j,0}|
324: &\leq& k-l+j - \log e \cdot 2^{-l+j-1} \cdot (k-2l)/l\\
325: &\leq& k-l+j - 2^{j-1} \leq k-l.
326: \end{eqnarray*}
327: Therefore, $F_l$ is an unsatisfiable $(k,s)\CNF$ formula for $s=2^{k-l+1}$,
328: as long as
329: \begin{eqnarray}\label{leq}
330: l \cdot 2^l \leq \log e \cdot (k-2l).
331: \end{eqnarray}
332:
333: \end{proof}
334:
335: Let $l$ be the largest integer satisfying
336: $2^l \leq \log e \cdot k / (2 \log k)$.
337: Then (\ref{leq}) holds for $k \geq 2$
338: and therefore we get the following:
339:
340: \begin{corollary}
341: $f(k) \leq 2^k \cdot 8 \log_e k / k\quad\mbox{for }k \geq 2$.
342: \end{corollary}
343:
344: \section{Even better upper bounds}\label{computer:section}
345:
346: One way to derive better upper bounds on $f(k)$ is to generalize the
347: construction of Section~\ref{constructII:section}.
348: To this end, we first define a special way to compose CNF formulas
349: capturing the essence of that construction.
350: \begin{definition}\label{compose:definition}
351: Let $F_1, F_2$ be unsatisfiable CNF formulas that have clauses of size at
352: most $k$ such that $F'_i$ is a $k_i\CNF$ formula for $i=1,2$.
353: Also, assume that $k_1 \leq k_2 < k$.
354: Then the formula $F_1 \circ F_2$ is defined as:
355: \begin{eqnarray*}
356: \left(
357: \bigcup_{c \in \KM(x_1,\ldots,x_{k-k_2})} F_{1,c}' \times c \cup F_{1,c}''
358: \right)
359: \cup
360: F'_2 \times \{\{x_{1},\ldots,x_{k-k_2}\}\} \cup F''_2,
361: \end{eqnarray*}
362: where the formulas $F_{1,c}$ are copies of $F_1$ on distinct sets of
363: variables.
364: \end{definition}
365:
366:
367: It is not difficult to verify the following:
368: \begin{lemma}\label{compose:lemma}
369: Let $F_1, F_2$ be formulas as above,
370: where the number of occurrences of a variable
371: is bounded by $s \geq (2^{k-k_2}-1) \cdot |F'_1| + |F'_2|$
372: and let $G=F_1 \circ F_2$.
373: Then $G$ is an unsatisfiable CNF formula
374: where each variable occurs at most $s$ times.
375: Furthermore, $G'$ is a $(k_1+k-k_2)\CNF$ formula,
376: and $|G'|=(2^{k-k_2}-1) \cdot |F'_1|$.
377: \end{lemma}
378:
379:
380: Given $k,s$, we ask whether we can obtain a $k\CNF$ formula using
381: the following derivation rules.
382: We start with the unsatisfiable formula $\{\emptyset\}$
383: as an axiom (this formula consists of one empty clause).
384: For a set of derivable formulas, one can apply one of the following rules:
385:
386: \begin{enumerate}
387: \item
388: If $F$ is a derived formula such that $s \geq
389: 2\cdot|F'|$,
390: then we can derive
391: $F' \times \{\{x\},\{\overline{x}\}\} \cup F''$, where $x$ is a new
392: variable.
393: \item
394: If $F_1, F_2$ are two derived formulas satisfying the conditions of
395: Lemma~\ref{compose:lemma}, then we can derive the formula $F_1 \circ F_2$.
396: \end{enumerate}
397:
398: \begin{note}
399: One can sometimes replace $F_1 \circ F_2$ in the second rule by a more
400: compact formula $F_1 \circ' F_2$ that avoids duplicating $F_1$.
401: Namely, the formula $F_1' \times \KM(x_1,\ldots,x_{k-k_2}) \cup F_1'' \cup
402: F'_2 \times \{\{x_{1},\ldots,x_{k-k_2}\}\} \cup F''_2$.
403: Although this can never reduce the number of occurrences of variables,
404: this modification reduces the number of clauses and variables.
405: In the construction of Section~\ref{constructII:section},
406: we always use $\circ'$ instead of $\circ$.
407: \end{note}
408:
409: Since any $k\CNF$ formula obtained using the above procedure is an
410: unsatisfiable $(k,s)\CNF$, one can define $f_2(k)$ as the maximal
411: value of $s$ such that no $k\CNF$ formula can be obtained using the
412: above procedure (clearly $f(k) \leq f_2(k)$). It turns out that the
413: function $f_2(k)$ is appealing from an algorithmic point of view.
414: Given a value for $s$, one can check if $f_2(k) \leq s$ using a simple
415: dynamic programming algorithm. For all $l=0,\ldots,k-1$, the
416: algorithm keeps as state the minimal size of $F'$ for a derivable
417: unsatisfiable formula $F$ where $F'$ is an $l\CNF$ formula. This approach
418: yields an algorithm that works well in practice and we were able to
419: calculate $f_2(k)$ for values up to $k=\maxk$ to get the results
420: depicted by the graph in Figure~\ref{graph}.
421:
422: \begin{figure}[h!]
423: \centering
424: \epsfig{file=f2.eps,height=8cm}\\
425: \caption{The bounds on $f(k) \cdot k/2^k$.
426: (a) Lower bound of Kratochv\'{\i}l et al. \cite{KratochST93},
427: $1/e$. (b) Upper bound (\ref{ourupperbound}) obtained in Section
428: 3 of the present paper, $8\log_e k$. (c) Upper bound $f_2(k)
429: \cdot k/2^k$, calculated by a computer program.
430: (d) The line $0.5 \log(k) + 0.23$. %0.2273xxx
431: }
432: \label{graph}
433: \end{figure}
434:
435: %% \begin{center}
436: %% \epsfig{file=f2.eps,height=8cm}\\
437: %% \raggedright
438: %% %\setlength{\leftmargin}{2cm}
439: %% %\setlength{\rightmargin}{2cm}
440: %% \figlabel{graph}:
441: %% The bounds on $f(k) \cdot k/2^k$.
442: %% (a) Lower bound of Kratochv\'{\i}l et al.\ \cite{KratochST93}, $1/e$.
443: %% (b) Upper bound (\ref{ourupperbound}) obtained in Section 3 of the present
444: %% paper, $8\log_e k$.
445: %% (c) Upper bound $f_2(k) \cdot k/2^k$, calculated by a computer program.
446: %% (d) The line $0.5 \log(k) + 0.23$.
447: %% \end{center}
448:
449:
450: The computed numerical values of $f_2(k)$ seem to indicates that
451: \begin{equation}
452: \label{eq:conjecture}
453: f_2(k) \cdot k/2^k = 0.5 \log(k) + o(\log(k))
454: \end{equation}
455: which is better than our upper bound by a constant factor of about
456: $11$. If (\ref{eq:conjecture}) indeed holds, then a better
457: analysis of the function $f_2$ may improve our upper bound by a
458: constant factor. However, such an approach cannot improve upon the
459: logarithmic gap left between the known upper and lower bounds on
460: $f(k)$.
461:
462: \bibliography{f2}
463: \end{document}
464: