SAT is Not Solvable in Constant Time

Daniel Shea 📧

March 26, 2026

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This entry establishes that the Boolean Satisfiability Problem (SAT) cannot be decided by a deterministic Turing machine in constant time \(O(1)\). The core of the argument rests on an indistinguishability invariant: a Turing machine bounded by constant time \(C\) 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.

License

BSD License

Topics

Session SAT_Not_Const_Time

Depends on

Cite

× 
@article{SAT_Not_Const_Time-AFP,
  author  = {Daniel Shea},
  title   = {SAT is Not Solvable in Constant Time},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/SAT_Not_Const_Time.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download