<p>I am writing a paper on the complexity of some unorthodox proof systems, where I have two systems <span class="math-container">$P$</span> and <span class="math-container">$Q$</span> such that <span class="math-container">$P$</span> simulates <span class="math-container">$Q$</span> in the sense of it being possible to translate a <span class="math-container">$Q$</span>-proof into an at most polynomially larger <span class="math-container">$P$</span>-proof, but the best algorithm I can give for this simulation involves solving an <span class="math-container">$\mathsf{NP}$</span>-complete problem. In the parlance of proof complexity, <span class="math-container">$P$</span> simulates <span class="math-container">$Q$</span> but I do not know whether <span class="math-container">$P$</span> p-simulates <span class="math-container">$Q$</span>. 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.</p>
<p>Are there any other simulations of this kind or is it indeed a rare occurrence?</p>

CC BY-SA 4.0
2022-02-04T04:44:22.043Z
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. https://conference.iiis.tsinghua.edu.cn/ICS2010/content/papers/29.html
Joshua Grochow
CC BY-SA 4.0
2022-02-04T05:13:52.653Z
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.
Emre Yolcu
CC BY-SA 4.0
2022-02-08T20:41:57.787Z
In ["DRAT and Propagation Redundancy Proofs Without New Variables"](https://arxiv.org/abs/1909.00520), 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.
GManNickG
CC BY-SA 4.0
2022-02-12T14:45:56.313Z
I think there might be an example in Robert Reckhow's PhD thesis where these were originally defined.
Kaveh
CC BY-SA 4.0
2022-02-12T14:54:00.490Z
Sub-exp simulation of Frege by bd-Frege is another good example I think, see the paper by Pitassi, Santhanam, and Filmus.
Kaveh
CC BY-SA 4.0
2022-02-12T20:33:31.810Z
@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.
Emre Yolcu
<cc.complexity-theory><reference-request><lo.logic><proof-complexity>
Examples of simulations in proof complexity that are not p-simulations
Emre Yolcu
# Examples of simulations in proof complexity that are not p-simulations

(Asked by: username_0 on 2022-02-03)

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?

**Tags:** cc.complexity-theory, reference-request, lo.logic, proof-complexity

> **Comments:**
> **username_1**: 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. https://conference.iiis.tsinghua.edu.cn/ICS2010/content/papers/29.html  
> **username_0**: 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.  
> **username_2**: In ["DRAT and Propagation Redundancy Proofs Without New Variables"](https://arxiv.org/abs/1909.00520), 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.  
> **username_3**: I think there might be an example in Robert Reckhow's PhD thesis where these were originally defined.  
> **username_3**: Sub-exp simulation of Frege by bd-Frege is another good example I think, see the paper by Pitassi, Santhanam, and Filmus.  
> **username_0**: @username_3 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.  

---

## 0 answers

