A Lower Bound for Boolean Satisfiability on Turing Machines

TL;DR

This paper proves a fundamental lower bound on the number of moves a Turing machine needs to decide satisfiability for any full set of Boolean functions, highlighting inherent computational complexity.

Contribution

It establishes a universal lower bound for Turing machine complexity in Boolean satisfiability, applicable to all full representations of Boolean functions, regardless of formula minimization.

Findings

Lower bound of 2^n log_k 2 moves for satisfiability decision

Bound applies to any full representation of Boolean functions

Lower bound does not hold for certain restricted formulas like 2CNF, XOR-SAT, HORN-SAT

Abstract

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.