Minimal unsatisfiable 3-SAT example

The 3-SAT problem defined here is a stricter version than elsewhere, in the sense that each clause must contain exactly three literals. Some versions permit 1 or 2 literals.

To obtain a minimal unsatisfiable 3-SAT example, we start with a two-clause contradiction representing \( u_1 \wedge \neg u_1 \) as the base case. This base case is not 3-SAT. We then grow the clause as follows: suppose \( C_{i-1} \) containing \( i-1 \) variables is unsatisfiable, then let \( C_i = \left\{ c \vee u_i, c \vee \neg u_i \mid c \in C_{i-1} \right\} \), and \( C_i \) is also unsatisfiable.

To carry out the algorithm, we start with the base case.

• \( u_1 \)
• \( \neg u_1 \)

Then we add another variable to each clause:

• For \( u_1 \):
• \( u_1 \vee u_2 \)
• \( u_1 \vee \neg u_2 \)
• For \( \neg u_1 \):
• \( \neg u_1 \vee u_2 \)
• \( \neg u_1 \vee \neg u_2 \)

Then we add another variable to each clause:

• For \( u_1 \vee u_2 \)
• \( u_1 \vee u_2 \vee u_3 \)
• \( u_1 \vee u_2 \vee \neg u_3 \)
• For \( u_1 \vee \neg u_2 \)
• \( u_1 \vee \neg u_2 \vee u_3 \)
• \( u_1 \vee \neg u_2 \vee \neg u_3 \)
• For  \( \neg u_1 \vee u_2 \)
• \( \neg u_1 \vee u_2 \vee u_3 \)
• \( \neg u_1 \vee u_2 \vee \neg u_3 \)
• For \( \neg u_1 \vee \neg u_2 \)
• \( \neg u_1 \vee \neg u_2 \vee u_3 \)
• \( \neg u_1 \vee \neg u_2 \vee \neg u_3 \)

And here we have an unsatisfiable 3SAT example with 3 variables and 8 clauses.

Oversized tablet

Presumably, one could put together a Planar 32" multi-touch monitor (manual, datasheet) mounted on one of the VESA 400x200 monitor stands and hook the monitor up to one of the NVIDIA development boards with TEGRA processor, such as the Toradex Colibri T30 (announced but not available yet), install Android, and get a giant 32 inch tablet. Such system, along with some custom software, would make it a nice interactive kiosk either at a museum or at home for about $3000 material cost.

Building autotools from git

For developing GNU software, it is often needed to create the autoconf, automake, and libtool toolchain at the exact version specified, but it's not too hard to build them from source. In my case, I simply did:

• git clone git://git.sv.gnu.org/autoconf.git
• git clone git://git.sv.gnu.org/automake.git
• git clone git://git.sv.gnu.org/libtool.git

And this will let me do a git checkout vN.NN to obtain the specific version of these tools. However, building them from upstream pristine source is different than building from tarball distribution. You will already need a recent version of these autotools to bootstrap the source's build system. Run:

git clean -f -X

will restore the working tree to the pristine condition.

To build autoconf from source:

• aclocal -I m4 && automake --add-missing && autoconf
• rm INSTALL

The aclocal -I m4 addresses the following issues:

• automake complains:

  Makefile.am:40: MAKE_CASE_SENSITIVE does not appear in AM_CONDITIONAL

• autoconf complains:

  configure.ac:116: error: possibly undefined macro: AC_PROG_GNU_M4
        If this token and others are legitimate, please use m4_pattern_allow.
        See the Autoconf documentation.
  configure.ac:184: error: possibly undefined macro: AC_PROG_MAKE_CASE_SENSITIVE
  

The rm INSTALL addresses the following issue during make, caused by build-aux/missing wanting to overwriting a symlink created by automake --add-missing before, pointing to a system INSTALL file (this would be pretty nasty if you ran make as the same user that installed the automake you used for bootstrapping autoconf, since you would never notice the overwriting).

Making all in .
/bin/sh something/autoconf/build-aux/missing --run makeinfo --no-headers --no-validate --no-split  --plaintext -o something/autoconf/INSTALL \
   something/autoconf/doc/install.texi
something/autoconf/INSTALL: Permission denied

Here are the specific versions of these autotools I needed for binutils:

• autoconf v2.64, automake v1.11.1

In general, for the autoconf version, look for AC_PREREQ in configure.ac or configure.in; for the automake version, look for AM_AUTOMAKE_VERSION in aclocal.m4.

Some notes for porting Fink packages to 10.7

For all .info file:

• Add 10.7 to Distribution as a comma separated list.

  Distribution: 10.4, 10.5, 10.6, 10.7

• Add x86_64 to Architecture

  Architecture: powerpc, i386, x86_64

If this is not done correctly, Fink would say "no package found for specification..." since the .info files are filtered by distribution and architecture. On 10.7, the Intel architecture is x86_64.

Specific to gcc43:

• Change all gmp dependencies to gmp5 (and get rid of >= version constraints).
• Change all libmpfr1 dependencies to libmpfr4 (and get rid of >= version constraints).
• Change ecj-latest.jar MD5 to d7cd6a27c8801e66cbaa964a039ecfdb
• Remove ln -s ... %i/bin/$binfile-4 and remove Conflicts and Replaces. There is no other reason why gcc 4.x cannot coexist.
• Replace all traces of i686 with %m. Optionally change --with-tune=generic to --with-tune=core2.
• To workaround build failure “error: redefinition of a 'extern inline' function 'xxx' is not supported in C99 mode.” Per clang instruction, set CC='gcc -std=gnu89' to workaround it. Another issue surfaced in the second stage is undefined symbol for architecture x86_64 '___builtin___stpncpy_chk' which is resolved by adding -D_FORTIFY_SOURCE=0 to CFLAGS.

  SetCC: gcc -std=gnu89
  SetCFLAGS: -D_FORTIFY_SOURCE=0

• To resolve ld: duplicate symbol _init_inline_once issue, remove redundant tree-inline.o from CXX_C_OBJS in ${SRCDIR}/gcc/cp/Make-lang.in.
• Add --enable-libgcj to the ConfigureParams. For some reason this flag is missing, and libgcj is not, but is expected, to be built.
• Remove Type: -64bit and redundant references of the %lib expansion, particular those in the SplitOff.

The end.

Better upper bound for factorial?

Tonight I was puzzled by the question, if an algorithm \( \Pi \) has running time \( O(n!) \), does \( \Pi \) belong to EXPTIME? To rehash, EXPTIME contains all algorithms that has running time \( O(2^{n^k}) \). For brevity, I use the notation \( f(x) \prec g(x) \) to denote that \( f(x) \) grows slower than \( g(x) \). We know that \( 2^n \prec n! \prec n^n \) but I don't think I can show that \( n^n \) belongs to EXPTIME. I need a tighter bound.

It turns out that \( n! \prec 2^{n^2} \).

Proof.

• The growth of \( n! \) is \( \frac{(n+1)!}{n!} = n+1 \).
• The growth of \( 2^{n^2} = (2^n)^n \) is \[
  \begin{eqnarray}
  \frac{(2^{n+1})^{n+1}}{(2^n)^n}
    & = & \frac{(2 \cdot 2^n)^{n+1}}{(2^n)^n} \\
    & = & \frac{(2 \cdot 2^n)^n \cdot (2 \cdot 2^n)}{(2^n)^n} \\
    & = & \frac{2^n \cdot \cancel{(2^n)^n} \cdot (2 \cdot 2^n)}{\cancel{(2^n)^n}} \\
    & = & 2 \cdot 2^{2n} = 2^{2n+1} \\
  \end{eqnarray}
  \]

Since \( n+1 < 2^{2n+1} \) for all \( n \), therefore \( n! \prec 2^{n^2} \).

\( \Box \)

So it turns out that an \( O(n!) \) algorithm belongs to the class \( O(2^{n^k}) \) where \( k = 2 \), so such algorithm indeed belongs to EXPTIME.

---

Update (June 7, 2012): it turns out that showing \( n^n \) belongs to EXPTIME isn't that hard.

The growth of \( n^n \) is \[
\begin{eqnarray}
\frac{(n+1)^{n+1}}{n^n}
  & = & \frac{(n+1)^n (n+1)}{n^n} \\
  & = & \left( \frac{n+1}{n} \right)^n (n+1) \\
  & = & \left( 1 + \frac{1}{n} \right)^n (n + 1) \\
  & \approx & (n+1)e \\
\end{eqnarray}
\]

And that's because \( \lim_{n \to \infty} \left( 1 + \frac{1}{n} \right)^n = e \).  So \( n^n \) even grows slower than \( 2^{n^2} \).