9
$\begingroup$

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?

Improve this question
$\endgroup$
6
  • 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$
    – Joshua Grochow
    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

0

Reset to default

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.