Time-space tradeoffs for satisfiability

Abstract

We give the first nontrivial model-independent time-space tradeoffs for satisfiability. Namely, we show that SAT̄ cannot be solved in n1+o(1) time and n1-ε space for any ε>0 general random-access nondeterministic Turing machines. In particular, SAT cannot be solved deterministically by a Turing machine using quasilinear time and √n space. We also give lower bounds for log-space uniform NC1 circuits and branching programs. Our proof uses two basic ideas. First we show that if SAT̄ can be solved nondeterministically with a small amount of time then we can collapse a nonconstant number of levels of the polynomial-time hierarchy. We combine this work with a result of Nepomnjascii that shows that a nondeterministic computation of super-linear time and sublinear space can be simulated in alternating linear time. A simple diagonalization yields our main result. We discuss how these bounds lead to a new approach to separating the complexity classes NL and NP. We give some possibilities and limitations of this approach.