Time-space tradeoffs for counting NP solutions modulo integers

We prove the first time-space tradeoffs for counting the number of solutions to an NP problem modulo small integers, and also improve upon known time-space tradeoffs for SAT. Let m > 0 be an integer, and define MODm-SAT to be the problem of determining if a given Boolean formula has exactly km satisfying assignments, for some integer k. We show for all primes p except for possibly one of them, and for all c < 2cos(pi/7) approximate to 1.801, there is a d > 0 such that MODp-SAT is not solvable in n(c) time and n(d) space by general algorithms. That is, there is at most one prime p that does not satisfy the tradeoff. We prove that the same limitation holds for SAT and MOD6-SAT, as well as MODm-SAT for any composite m that is not a prime power. Our main tool is a general method for rapidly simulating deterministic computations with restricted space, by counting the number of solutions to NP predicates modulo integers. The simulation converts an ordinary algorithm into a "canonical" one that consumes roughly the same amount of time and space, yet canonical algorithms have nice properties suitable for counting.