# Examples of simulations in proof complexity that are not p-simulations

I am writing a paper on the complexity of some unorthodox proof systems, where I have two systems $$P$$ and $$Q$$ such that $$P$$ simulates $$Q$$ in the sense of it being possible to translate a $$Q$$-proof into an at most polynomially larger $$P$$-proof, but the best algorithm I can give for this simulation involves solving an $$\mathsf{NP}$$-complete problem. In the parlance of proof complexity, $$P$$ simulates $$Q$$ but I do not know whether $$P$$ p-simulates $$Q$$. I would like to comment in the paper on the peculiarity of this situation, saying that it is quite rare, because all the simulations I know of are also p-simulations. However, since this is a negative claim I cannot really point to a reference to support it, I can only point to a lack of similar examples.

Are there any other simulations of this kind or is it indeed a rare occurrence?

• This paper on "Effectively p-simulations" by Pitassi & Santhanam seems potentially relevant. In particular, from the abstract, they exhibit situations w/ effectively p-simulations but no p-simulations. conference.iiis.tsinghua.edu.cn/ICS2010/content/papers/29.html Feb 4 at 4:44
• Thank you. I am aware of this paper, but it does not directly relate to my question. To clarify, I am looking for examples where we know that a short translation of a proof exists, but the means by which we prove the existence of such a translation does not yield an efficient algorithm to find it. Pitassi & Santhanam instead show that some systems (e.g., various refinements of Resolution) that are separated with respect to p-simulations become equivalent under the looser notion of effectively p-simulations. Feb 4 at 5:13
• In "DRAT and Propagation Redundancy Proofs Without New Variables", it is shown that SPR- simulates PR- in size O(S⋅2^𝛿), where 𝛿 is a "discrepancy" measure of the PR proof. (If 𝛿 is logarithmically bounded, this is a p-simulation.) I'm not sure this is really along the same lines, though, being an "obvious" size increase rather than an inherently difficult conversion to a polynomially-sized proof. Feb 8 at 20:41
• I think there might be an example in Robert Reckhow's PhD thesis where these were originally defined. Feb 12 at 14:45
• @Kaveh Reckhow explicitly says on page 113 of his thesis that all simulations in the thesis are efficient. As for the paper by Filmus, Pitassi, and Santhanam I went through Section 4 and unless I missed something their simulation is also efficient in the sense that the running time is bounded by a polynomial in the size of the subexponential-size proof. Feb 12 at 20:33