We give the first nontrivial model-independent time-space tradeoffs for satisfiability. Namely we show that (SAT) over bar cannot be solved simultaneously in n(1+o(1)) time and n(1-epsilon) space for any epsilon > 0 on general random-access nondeterministic Turing machines. We also give several other related results. Our proof uses two basic ideas. First we show that if (SAT) over bar can be solved nondeterministically with a small amount of space then we can collapse a nonconstant number of levels of the polynomial-time hierarchy. Next we extend work of Nepomnjascii to show that a nondeterministic computation of super linear time and sublinear space can be simulated in alternating linear time. Combining these facts with 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.