Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Is there an oracle such that in the relativized world, bd-Frege (bounded depth Frege propositional proof system) has FIP (feasible interpolation property) but Frege does not have FIP?

Such an oracle will need to satisfy the following condition about DDH:

Is there an oracle such that in the relativized word, DDH$_n$ has subexponential $2^{O(n^{1 \over d})}$ size circuits but does not have polynomial ones?


Motivation:

We were talking with Yuval about the possibility of reducing FIP for Frege to FIP for bd-Frege. Up to cryptographic assumption about hardness of DDH (Decisional Diffie–Hellman problem) neither satisfies FIP. The hardness condition on DDH is (exponentially) stronger in the case of bd-Frege [BPR'00,BDGMP'04]. We wanted to see if we can weaken the hardness condition on DDH in the bd-Frege case to the same condition in the Frege case.

Note that the FIP for Frege would trivially imply the FIP for bounded-depth Frege since the former p-simulates the later. There are sub-exponential simulation results in the other direction [FPS'11], but it is not clear if one can obtain FIP for Frege implies FIP for bd-Frege.

On the other hand, for FIP it seems that we need to find the interpolant for cut rules in the proof which is close to finding a satisfying witness for a formula. The formula is of bounded depth in the case of bd-Frege, but the problem of finding a satisfying assignment is not easier than the general case of an arbitrary formula (the Frege case), both are $\mathsf{NP\text{-}complete}$.


Background:

One of the main problems in proof complexity is showing superpolynomial lowerbounds for propositional proof systems. If every propositional proof system has a family of formulas with superpolynomial proof size lowerbound, then it follows $\mathsf{NP} \neq \mathsf{coNP}$. So proving lowerbounds for propositional proof systems is similar to proving lowerbounds for circuit families (with the ultimate goal of showing a (general circuit) superpolynomial size lowerbound for some explicit function and separating $\mathsf{NP}$ from $\mathsf{P}/\mathsf{poly}$).

There is a nice correspondence between many propositional proof systems and circuit complexity classes: restrict the lines in the proof to circuits from the corresponding class.

But proving lowerbounds for propositional proof systems seems to be even more difficult than proving circuit lowerbounds, for example we still don't have a lowerbound for the propositional proof system with $AC^0[ 2 ]$ lines where as subexponential size lowerbound are known for $AC^0[ 2 ]$ circuits computing $\mod 3$. Therefore transferring the results from circuit complexity to proof complexity is not straightforward.

One of the few methods for proving proof complexity lowerbounds is showing that the proof system has FIP, and then use it to extract a reasonably small size circuit from the propositional proof of a formula coming from circuit complexity such that we know (or conjecture) the function computed by the interpolant is hard.

FIP for a propositional proof system $P$ means that if $P$ proves a disjunction $\varphi(\vec{x},\vec{y}) \lor \psi(\vec{x},\vec{z})$ then there is a small circuit that given values for $\vec{x}$, tell us which disjunct is true (think of each disjunct as a $\mathsf{coNP}$ set in input $\vec{x}$, and their union covers all possible values of $\vec{x}$, or equivalently the task is separating two provably disjoint $\mathsf{NP}$ sets using polynomial size circuits).

But unfortunately this doesn't work for even relatively weak systems like bd-Frege because up to cryptographic hardness assumptions mentioned above, these systems do not have FIP (they can prove cryptographic results such that an interpolant for the proof would break the cryptographic primitive).


References:

  1. Y. Filmus, T. Pitassi, R. Santhanam, Exponential lower bounds for AC0-Frege imply polynomial Frege lower bounds, ICALP 2011
  2. M.L. Bonet, T. Pitassi, and R. Raz, On interpolation and automatization for Frege systems, SIAM Journal on Computing, 2000.
  3. M.L. Bonet, C. Domingo, R. Gavalda, A. Maciel, and T. Pitassi, Non-automatizability of bounded-depth Frege proofs, Computational Complexity, 2004.

Originally posted on cstheory

share|improve this question
    
I’m not quite sure I understand the question. By FIP “in the relativized world”, do you mean that you ask for interpolants in standard F or F_d using poly-size oracle circuits, or do you want to relativize the pps as well? If so, how? Ditto for the second question: I have no idea how to relativize Diffie–Hellman, if that’s the intention. Note that if the unrelativized DDH has no poly-size oracle circuits wrt some oracle, then it also has no poly-size plain circuits, so you can’t expect to construct such an oracle unconditionally. –  Emil Jeřábek Jul 20 '11 at 15:57
    
@Email, good question, we don't have a general way of saying what a relativized formula means, so relativization depends on what we are trying to achieve. The main question is that can be weaken the subexponential hardness requirement on DDH for bdFrege case to the weaker hardness requirement on DDH in the Frege case. We want to show this is not the case (or at least not possible with the current method), so given an oracle (circuit gates) for FIP(bdFrege) we want to show that it is still possible that we cannot we don't have FIP(Frege), i.e. –  Kaveh Jul 21 '11 at 22:00
    
there are not oracle circuits of polynomial size for the interpolating Frege proofs. So I think we don't need to relativize the proof systems, i.e. relativization means that we have oracle gates for interpolating circuits. We can also do it with oracle pps but that would require us to prove the formula about DDH with oracles I think. And you are right, we still need the weaker hardness assumption on DDH. –  Kaveh Jul 21 '11 at 22:45
    
About relativizing DDH, it is also not clear to me (sorry). DDH is a hardness assumption about a very concrete object so yes, I don't know what I want exactly, I have to think about it. It seems to me that in separating crypto primites we can relativize two things: we can allow/disallow the crypto primitive to use the oracles gates and we can allow/disallow also adversaries to use the oracle gates directly. It seems that the first one is out of question so we can only relativize the adversaries. I have to think more about it to see if my question makes sense. –  Kaveh Jul 21 '11 at 23:16
add comment

Know someone who can answer? Share a link to this question via email, Google+, Twitter, or Facebook.

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.