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?

  • 1
    $\begingroup$ 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 $\endgroup$ Feb 4, 2022 at 4:44
  • 1
    $\begingroup$ 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. $\endgroup$
    – Emre Yolcu
    Feb 4, 2022 at 5:13
  • 2
    $\begingroup$ 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. $\endgroup$
    – GManNickG
    Feb 8, 2022 at 20:41
  • $\begingroup$ I think there might be an example in Robert Reckhow's PhD thesis where these were originally defined. $\endgroup$
    – Kaveh
    Feb 12, 2022 at 14:45
  • 2
    $\begingroup$ @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. $\endgroup$
    – Emre Yolcu
    Feb 12, 2022 at 20:33


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.