  We establish a lower bound for deciding the satisfiability of the conjunction
of any two Boolean formulas from a set called a full representation of Boolean
functions of $n$ variables - a set containing a Boolean formula to represent
each Boolean function of $n$ variables. The contradiction proof first assumes
that there exists a Turing machine with $k$ symbols in its tape alphabet that
correctly decides the satisfiability of the conjunction of any two Boolean
formulas from such a set by making fewer than $2^nlog_k2$ moves. By using
multiple runs of this Turing machine, with one run for each Boolean function of
$n$ variables, the proof derives a contradiction by showing that this Turing
machine is unable to correctly decide the satisfiability of the conjunction of
at least one pair of Boolean formulas from a full representation of
$n$-variable Boolean functions if the machine makes fewer than $2^nlog_k2$
moves. This lower bound holds for any full representation of Boolean functions
of $n$ variables, even if a full representation consists solely of minimized
Boolean formulas derived by a Boolean minimization method. We discuss why the
lower bound fails to hold for satisfiability of certain restricted formulas,
such as 2CNF satisfiability, XOR-SAT, and HORN-SAT. We also relate the lower
bound to 3CNF satisfiability. The lower bound does not depend on sequentiality
of access to the tape squares and will hold even if a machine is capable of
non-sequential access.
