<p>Craig's Interpolation Theorem guarantees existence of an interpolant, but it does not guarantee that the interpolant can always be written down in size polynomial in the size of the original formulas. In fact, there are known examples where any interpolant (in standard propositional formula form such as CNF or DNF) must have exponential size. Consequently, if we insist on outputting the interpolant as a full-blown formula, then a polynomial-time (or even NP-oracle-polynomial-time) algorithm in the usual sense cannot produce that formula in the worst case—simply because writing down the output itself may require exponential space.</p>
<p>This exponential blow-up rules out the possibility that the &quot;compute an interpolant&quot; problem (with the interpolant given in straightforward formula notation) lies in the function class <span class="math-container">$\mathrm{FP}^{\mathrm{NP}}$</span>, whose definition demands that both:</p>
<ol>
<li>The running time is polynomial in the input size</li>
<li>The length of the output is at most polynomial in the input size</li>
</ol>
<p>If we need an output that can be exponentially large, no function class predicated on polynomial output length (including <span class="math-container">$\mathrm{FP}^{\mathrm{NP}}$</span>) can capture that task in a strict sense.</p>
<p>However, we can refine the question by asking about succinct representations. For instance, we can allow circuits or formulas with &quot;sharing of subexpressions&quot; (i.e., DAG representations) of size polynomial in the original input or in a proof of unsatisfiability. In many propositional proof systems (e.g., resolution), an interpolant can be extracted from a refutation in a manner that yields a polynomial-size circuit (or dag-like formula), even if the equivalent CNF or DNF might blow up exponentially. Under such a succinct representation, we can place the search problem into classes like <span class="math-container">$\mathrm{FP}^{\mathrm{NP}}$</span> or <span class="math-container">$\mathrm{FP}^{\mathrm{coNP}}$</span>, depending on how the refutation is accessed and verified.</p>
<p>Hence, the short answer is that if we require an explicit, textually fully expanded interpolant, the worst-case exponential size forces us out of the usual notion of &quot;polynomial-time computable function.&quot; By contrast, if we allow succinct or circuit-based output, then there are known methods (by extracting interpolants from proof objects) that operate in time polynomial in the input (plus oracle power appropriate to checking satisfiability/unsatisfiability). In that more liberal setting, the interpolation task can be placed in <span class="math-container">$\mathrm{FP}^{\mathrm{NP}}$</span> (or a closely related class). The essential subtlety is that the size of the output representation, rather than mere existence, dictates where the problem lands in the hierarchy of total function problems.​​​​​​​​​​​​​​​​</p>

CC BY-SA 4.0
2024-12-22T07:47:43.770Z
This is wrong. An interpolant can have size *exponential* in the size of the input formulas.
Emil Jeřábek
CC BY-SA 4.0
2024-12-22T18:36:21.323Z
@EmilJeřábek wouldn't that imply that the problem is not in TFNP? I'd be interested if that's the case, even if the precise complexity class is not known. What would be a reference for the fact that the size of the interpolant can be exponential?
user1868607
CC BY-SA 4.0
2024-12-22T19:35:33.307Z
@EmilJeřábek I'm a bit confused -- are you disagreeing with the answer, and if so what specifically is wrong?
Noam Zeilberger
CC BY-SA 4.0
2024-12-22T19:57:35.690Z
@user1868607 Any disjoint NP pair gives a sequence of polynomial-size tautological implications whose interpolants separate the disjoint pair. Thus, if you want the interpolant to be expressed by formula, it cannot be polynomial size in general unless every disjoint NP pair can be separated in $\mathsf{NC^1/poly}$; if you want it expressed by a circuit, it cannot be polynomial unless every disjoint NP pair can be separated in P/poly. It is widely expected that there are disjoint NP pairs that cannot be separated by circuits of subexponential size, but this has, of course, not been proved, ...
Emil Jeřábek
CC BY-SA 4.0
2024-12-22T20:01:11.550Z
... as it implies $\mathsf{P\ne NP}$. Indeed, if P = NP, then every implication has an interpolant definable by a (poly-time computable) poly-size circuits, hence such complexity-theoretic assumptions are unavoidable.
Emil Jeřábek
CC BY-SA 4.0
2024-12-22T20:07:38.727Z
@NoamZeilberger Note that my comment was written before the edit, that incorporated it. However, even after the edit, the answer is rather confused and misleading. The class $\mathsf{FP^{NP}}$ does not seem to actually have much to do with the complexity of the problem. On the one hand, even if you assume there *is* a polynomial-size interpolant, I see no reason it should be computable in $\mathsf{FP^{NP}}$: you cannot construct an unknown polynomial-size circuit by any kind of binary search; you would need to nondeterministically guess the circuit, and then verify that it gives a correct ...
Emil Jeřábek
CC BY-SA 4.0
2024-12-22T20:11:47.717Z
... interpolant, hence this only gives an $\mathsf{FNP^{NP}}$ search problem. On the other hand, in the part where it talks about proof systems with feasible interpolation: in the few proof systems that are known to have feasible interpolation, the interpolating circuit can be actually computed in polynmial time (i.e., FP) from the proof, so $\mathsf{FP^{NP}}$ is not needed. And, of course, it makes hardly any sense to write “$\mathsf{FP^{NP}}$ or $\mathsf{FP^{coNP}}$”, as $\mathsf{FP^{NP}}$ is the exact same thing as $\mathsf{FP^{coNP}}$.
Emil Jeřábek
CC BY-SA 4.0
2024-12-22T20:17:55.447Z
@EmilJeřábek Thanks that helps a lot.  I didn't notice that the post was edited after your comment, but all of your points about it make sense.
Noam Zeilberger
CC BY-SA 4.0
2024-12-22T21:55:15.737Z
@EmilJeřábek perhaps because the user is resorting to gen ai to produce such answers. These users target many communities like Physics, Maths, MO, CV, Quant, Cryptography and answer at a staggering rate. Please be cautious.
User1865345
CC BY-SA 4.0
2024-12-22T22:38:42.033Z
@User1865345 Ah. I suspected it might be so.
Emil Jeřábek
CC BY-SA 4.0
2024-12-23T03:26:37.333Z
Unfortunately @EmilJeřábek, this is not a one off phenomenon. Of late, there have been infestations of such users. Please whenever you see such lengthy posts that may look good, flag those for moderators attention. This user has already been banned in MO.
User1865345
CC BY-SA 4.0
2024-12-23T08:00:13.097Z
I would do that, but unfortunately, moderation is all but nonexistent on this site. The moderator attention flag I raised 18 days ago is still pending.
Emil Jeřábek
CC BY-SA 4.0
2024-12-23T12:45:47.893Z
Ohh @EmilJeřábek; I was not aware of that. Also strange that this community doesn't have an associated active general chat room which I could use (as I have for other communities where these users have targetted). Nevertheless, flagging is the right course of action, imo. Since you are one of the highly active contributors here, I would urge you to have a vigil eye as mere banning an account won't stop them making another and posting same things again.
User1865345
CC BY-SA 4.0
2024-12-22T05:48:41.590Z
2024-12-22T08:17:57.127Z
2024-12-22T08:17:57.127Z
Alex Rudimer
<p>Every pair of formulas in propositional logic have an interpolant by Craig's interpolation theorem. I was wondering where does this problem lie in the hierarchy of total function problems.</p>

<cc.complexity-theory><lo.logic>
In which class is the problem of computing propositional Craig interpolants?
user1868607
# In which class is the problem of computing propositional Craig interpolants?

(Asked by: username_0 on 2024-12-22)

Every pair of formulas in propositional logic have an interpolant by Craig's interpolation theorem. I was wondering where does this problem lie in the hierarchy of total function problems.

**Tags:** cc.complexity-theory, lo.logic

---

## 1 answers

### Answer by username_1 on 2024-12-22. Score: -3

Craig's Interpolation Theorem guarantees existence of an interpolant, but it does not guarantee that the interpolant can always be written down in size polynomial in the size of the original formulas. In fact, there are known examples where any interpolant (in standard propositional formula form such as CNF or DNF) must have exponential size. Consequently, if we insist on outputting the interpolant as a full-blown formula, then a polynomial-time (or even NP-oracle-polynomial-time) algorithm in the usual sense cannot produce that formula in the worst case—simply because writing down the output itself may require exponential space.

This exponential blow-up rules out the possibility that the "compute an interpolant" problem (with the interpolant given in straightforward formula notation) lies in the function class $\mathrm{FP}^{\mathrm{NP}}$, whose definition demands that both:

1. The running time is polynomial in the input size
2. The length of the output is at most polynomial in the input size

If we need an output that can be exponentially large, no function class predicated on polynomial output length (including $\mathrm{FP}^{\mathrm{NP}}$) can capture that task in a strict sense.

However, we can refine the question by asking about succinct representations. For instance, we can allow circuits or formulas with "sharing of subexpressions" (i.e., DAG representations) of size polynomial in the original input or in a proof of unsatisfiability. In many propositional proof systems (e.g., resolution), an interpolant can be extracted from a refutation in a manner that yields a polynomial-size circuit (or dag-like formula), even if the equivalent CNF or DNF might blow up exponentially. Under such a succinct representation, we can place the search problem into classes like $\mathrm{FP}^{\mathrm{NP}}$ or $\mathrm{FP}^{\mathrm{coNP}}$, depending on how the refutation is accessed and verified.

Hence, the short answer is that if we require an explicit, textually fully expanded interpolant, the worst-case exponential size forces us out of the usual notion of "polynomial-time computable function." By contrast, if we allow succinct or circuit-based output, then there are known methods (by extracting interpolants from proof objects) that operate in time polynomial in the input (plus oracle power appropriate to checking satisfiability/unsatisfiability). In that more liberal setting, the interpolation task can be placed in $\mathrm{FP}^{\mathrm{NP}}$ (or a closely related class). The essential subtlety is that the size of the output representation, rather than mere existence, dictates where the problem lands in the hierarchy of total function problems.​​​​​​​​​​​​​​​​

> **Comments:**
> **username_2**: This is wrong. An interpolant can have size *exponential* in the size of the input formulas.  
> **username_0**: @EmilJeřábek wouldn't that imply that the problem is not in TFNP? I'd be interested if that's the case, even if the precise complexity class is not known. What would be a reference for the fact that the size of the interpolant can be exponential?  
> **username_3**: @EmilJeřábek I'm a bit confused -- are you disagreeing with the answer, and if so what specifically is wrong?  
> **username_2**: @user1868607 Any disjoint NP pair gives a sequence of polynomial-size tautological implications whose interpolants separate the disjoint pair. Thus, if you want the interpolant to be expressed by formula, it cannot be polynomial size in general unless every disjoint NP pair can be separated in $\mathsf{NC^1/poly}$; if you want it expressed by a circuit, it cannot be polynomial unless every disjoint NP pair can be separated in P/poly. It is widely expected that there are disjoint NP pairs that cannot be separated by circuits of subexponential size, but this has, of course, not been proved, ...  
> **username_2**: ... as it implies $\mathsf{P\ne NP}$. Indeed, if P = NP, then every implication has an interpolant definable by a (poly-time computable) poly-size circuits, hence such complexity-theoretic assumptions are unavoidable.  
> **username_2**: @NoamZeilberger Note that my comment was written before the edit, that incorporated it. However, even after the edit, the answer is rather confused and misleading. The class $\mathsf{FP^{NP}}$ does not seem to actually have much to do with the complexity of the problem. On the one hand, even if you assume there *is* a polynomial-size interpolant, I see no reason it should be computable in $\mathsf{FP^{NP}}$: you cannot construct an unknown polynomial-size circuit by any kind of binary search; you would need to nondeterministically guess the circuit, and then verify that it gives a correct ...  
> **username_2**: ... interpolant, hence this only gives an $\mathsf{FNP^{NP}}$ search problem. On the other hand, in the part where it talks about proof systems with feasible interpolation: in the few proof systems that are known to have feasible interpolation, the interpolating circuit can be actually computed in polynmial time (i.e., FP) from the proof, so $\mathsf{FP^{NP}}$ is not needed. And, of course, it makes hardly any sense to write “$\mathsf{FP^{NP}}$ or $\mathsf{FP^{coNP}}$”, as $\mathsf{FP^{NP}}$ is the exact same thing as $\mathsf{FP^{coNP}}$.  
> **username_3**: @EmilJeřábek Thanks that helps a lot.  I didn't notice that the post was edited after your comment, but all of your points about it make sense.  
> **username_4**: @EmilJeřábek perhaps because the user is resorting to gen ai to produce such answers. These users target many communities like Physics, Maths, MO, CV, Quant, Cryptography and answer at a staggering rate. Please be cautious.  
> **username_2**: @User1865345 Ah. I suspected it might be so.  
> **username_4**: Unfortunately @EmilJeřábek, this is not a one off phenomenon. Of late, there have been infestations of such users. Please whenever you see such lengthy posts that may look good, flag those for moderators attention. This user has already been banned in MO.  
> **username_2**: I would do that, but unfortunately, moderation is all but nonexistent on this site. The moderator attention flag I raised 18 days ago is still pending.  
> **username_4**: Ohh @EmilJeřábek; I was not aware of that. Also strange that this community doesn't have an associated active general chat room which I could use (as I have for other communities where these users have targetted). Nevertheless, flagging is the right course of action, imo. Since you are one of the highly active contributors here, I would urge you to have a vigil eye as mere banning an account won't stop them making another and posting same things again.  

---

