Email Gateway (Apr 04 2026 at 17:01): Email Gateway (Apr 04 2026 at 17:01):From: Tobias Nipkow <nipkow@in.tum.de>
SAT is Not Solvable in Constant Time
Daniel Shea
This entry establishes that the Boolean Satisfiability Problem (SAT) cannot be
decided by a deterministic Turing machine in constant time. The core of the
argument rests on an indistinguishability invariant: a Turing machine bounded by
constant time can only ever read the first C+1 cells of its input tape.
Consequently, any language decided in constant time must be a prefix language.
We then show that SAT is not uniquely determined by any finite prefix, yielding
the impossibility result.
https://www.isa-afp.org/entries/SAT_Not_Const_Time.html
Enjoy!
Last updated: Apr 12 2026 at 02:50 UTC