Circuit Satisfiability Resists Small Space with Preprocessing
Statement: AI-written, not yet formalized. Proof: open – no attempt yet.
Interactive oracle proofs let a verifier be convinced by reading a few bits of the prover’s messages, and succinct ones keep the communication close to the size of the witness rather than the size of the computation. Strong impossibility results are known for succinct PCPs; for IOPs the picture is better, since relations decidable in small space do have them. Where is the limit? The source turns the question into one about circuit satisfiability with two resources: how much space, and how much time in a preprocessing phase that has not yet seen the instance. Its conjecture is that satisfiability cannot be decided in space polynomial in the number of inputs — which may be far fewer than the number of gates — however much preprocessing is allowed within a stated budget.
View PDF · LaTeX source · Formal statement — not yet formalized
The asymmetry that makes it interesting. Write \(\mathrm{CSAT}\) for satisfiability of a circuit of size \(n\) over \(m\) input bits. Since \(m\) can be much smaller than \(n\), \(\mathrm{poly}(m)\) space can be far less than the circuit itself, so this is not a restatement of any standard separation.
Conjecture (the source’s Conjecture 1.2). For a function class \(T\): \(\mathrm{CSAT}\) for circuits of size \(n\) over \(m\) input bits cannot be solved by an algorithm that uses \(\mathrm{poly}(m)\) space and \(t(n,m)\)-time probabilistic preprocessing, for any \(t \in T\).
What it buys (the source’s Corollary 1.3). Assuming the conjecture:
| Preprocessing budget \(t(n,m)\) | Ruled out for \(\mathcal{R}_{\mathrm{CSAT}}\) |
|---|---|
| \(\mathrm{poly}(n)\) | succinct IOP with constant rounds and \(O(\log n)\) query complexity |
| \(2^{\mathrm{polylog}(m)}\cdot\mathrm{poly}(n)\) | succinct IOP with \(\mathrm{polylog}(m)\) rounds and \(\mathrm{polylog}(m) + O(\log n)\) queries |
| \(2^{o(m)}\cdot\mathrm{poly}(n)\) | succinct IOP with \(o(m/\log m)\) rounds and \(o(m) + O(\log n)\) queries |
It is a family, and the members are not equally safe. The conjecture is stated relative to \(T\), so it is a scale of hypotheses. The source orders the consequences “from the weakest bound” and attaches decreasing confidence as \(T\) grows: it conjectures “that even probabilistic quasi-polynomial time preprocessing would not be sufficient, and taking things to an extreme, it is (arguably) unlikely that \((2^{o(m)}\cdot\mathrm{poly}(n))\)-time preprocessing is sufficient.” A resolution in either direction must name its \(T\): refuting the strongest setting says nothing about the weakest, and proving the weakest leaves the interesting IOP bounds untouched.
Why small space for \(\mathrm{CSAT}\) is not already known. From the source’s Appendix A: \(\mathrm{CVAL}\) is \(\mathsf{P}\)-complete under log-space reductions, so under the widely believed \(\mathsf{P} \not\subseteq \mathrm{Space}(\log)\) it cannot be solved in logarithmic space. But little is known even in sub-linear space — the best algorithm follows the pebbling approach and yields \(O(n/\log n)\) space, and “it was later proved that for general circuits, the pebbling approach cannot do much better”, an \(\Omega(n/\log n)\) bound against that technique. Since \(m\) can be far below \(n\), \(\mathrm{poly}(m)\) space is a different regime again.
What a refutation would mean. The source spells this out, and it is the best argument for the conjecture: if a circuit of size \(n\) over \(m\) variables could be solved in \(\mathrm{poly}(m)\) space with non-trivial probabilistic preprocessing, then “either it can be solved in a single phase; in \(\mathrm{poly}(m)\) space or non-trivial time, or it would imply a surprising interplay between space and time complexities and in particular, yield an interesting space-time trade-off for \(\mathrm{CSAT}\).” A refutation is forced to be a genuine space-time result.
Sources
- Nassar and Rothblum. Succinct Interactive Oracle Proofs: Applications and Limitations. IACR ePrint 2022/281. The source. Conjecture 1.2 and Corollary 1.3 are on page 5; the extended discussion including the \(\mathrm{CVAL}\) calibration is Appendix A on page 33.
- Hopcroft, Paul and Valiant. On Time Versus Space. Journal of the ACM, 1977. The pebbling approach giving the \(O(n/\log n)\)-space algorithm.
- Paul, Tarjan and Celoni. Space Bounds for a Game on Graphs. Mathematical Systems Theory, 1977. The \(\Omega(n/\log n)\) bound showing pebbling cannot do much better.
- Goldreich, Vadhan and Wigderson. On Interactive Proofs with a Laconic Prover. Computational Complexity, 2002. Limits on the communication complexity of interactive proofs, which the source positions its IOP limitations against.
View PDF — no proof written yet · LaTeX source — no proof written yet · Formal proof — not yet formalized
Open, and hard in the direction one would want.
Toward a proof. It is an unconditional space lower bound, which is the kind of statement complexity theory currently cannot deliver: even for \(\mathrm{CVAL}\), which is \(\mathsf{P}\)-complete, nothing better than the pebbling bound is known, and that bound is proved only against pebbling rather than in general. Adding preprocessing makes the target harder, not easier. Realistically, progress would come at the small-\(T\) end of the scale, and even \(t(n,m) = \mathrm{poly}(n)\) is not obviously within reach.
Toward a refutation. By the source’s own argument, an algorithm would either collapse into a single-phase algorithm — itself a surprising result — or exhibit a genuine space-time trade-off for \(\mathrm{CSAT}\). Either outcome would be independently interesting, which is why this is worth attacking from the positive side even by someone who expects the conjecture to be true.
Checked against the literature, 2026-08-28. No resolution at any setting of \(T\) found. Targeted check on this line and the space-complexity results the source cites, not an exhaustive sweep.
Where succinct IOPs currently stand. Succinct PCPs — length polynomial in the witness — face strong impossibility results. Succinct IOPs exist for the rich class of NP relations decidable in small space, which is the positive side, and Corollary 1.3 is the negative side conditional on this conjecture. The gap between those is what the conjecture would close.
The paper’s positive results run the other way. Using one-way functions it compiles IOPs into zero-knowledge proofs while nearly preserving proof length, complementing the line initiated by Ben Sasson et al. that compiles IOPs into super-succinct zero-knowledge arguments. Not this statement, and a resolution does not bear on it.
What a reviewer should be suspicious of, in order. First, which \(T\) a claimed result is about — without that the claim has no content. Second, whether a claimed succinct IOP beats the pairing of round count and query complexity in the relevant row of Corollary 1.3; loosening either alone does not contradict it. Third, whether the space bound is \(\mathrm{poly}(m)\) in the input count rather than in the circuit size, since the latter is the easy regime.