<p>I recently read a paper that presented a proof calculus where the verification of whether a given proof is valid was NL-complete. The authors apparently decided that the checking procedure was not local enough, and defined a modified notion of proof where (practically speaking) the execution trace of the dynamic programming algorithm doing the NL-complete checking in polytime was part of the proof. That modified notion of proof could now obviously be verified by very local checks.</p>

<p>I was both negatively shocked and positively surprised by this:</p>

<ul>
<li>The negative shock was that this gratuitous size increase of the witness string of an NP problem during a reduction doesn't seem to be penalised or even noticed for the common notions of reduction. I wondered whether there is any way to fix this, but I guess this is a difficult question. But if you know how to fix this, please let me know.</li>
<li>The positive surprise was that their trick seems to be applicable to arbitrary problems from NP to make the verification of the witness string locally checkable. The idea is to just declare the execution trace of the PTime verification algorithm to be a part of the witness string.</li>
</ul>

<p>Is the observation correct that the extended witness string still satisfies the polynomial size bounds as required by the definition of NP? What is the correct notion to capture what is meant by "can be verified by very local checks"? I initially proposed ALogTime, but the comments by Kaveh and  Emil Jeřábek indicate that DLogTime-uniform AC<sup>0</sup> would be more appropriate (and that coNLogTime is already sufficient).</p>

<hr>

<p>Note that</p>

<blockquote>
  <p>coNLogTime $\subset$ DLogTime-uniform AC<sup>0</sup> $\subset$ ALogTime and<br>
  ALogTime = DLogTime-uniform NC<sup>1</sup> = $U_{E^*}$-uniform NC<sup>1</sup> $\subset$ L-uniform NC<sup>1</sup>.</p>
</blockquote>

<p>and that the abstract of <a href="http://www.math.ucsd.edu/~sbuss/ResearchWeb/Boolean/paper.pdf" rel="nofollow">The Boolean formula value problem is in ALOGTIME</a> by Sam Buss says</p>

<blockquote>
  <p>These results are optimal since the Boolean formula value problem is complete for alternating log time under deterministic log time reductions.</p>
</blockquote>

CC BY-SA 3.0
2016-10-23T15:36:57.930Z
Yes it can, if well-known, even AC^0 is sufficient. Just look at the NP-compeleteness proof of CNF-SAT. This is essentially the trick to reduce SAT to CNF-SAT.
Kaveh
CC BY-SA 3.0
2016-10-23T16:56:44.170Z
@Kaveh Ah, now I understand for the first time why people here keep emphasising AC^0 reductions. But I'm not sure yet whether AC^0 is really sufficient, because I don't know whether the reduction from SAT to CNF-SAT is in AC^0, and I don't know whether the reduction from NP to SAT is in AC^0 (or at least whether the reductions are verifiable in AC^0). The abstract from Sam Buss' paper seems to indicate that AC^0 won't be enough.
Thomas Klimpel
CC BY-SA 3.0
2016-10-23T17:32:53.533Z
All known reductions between NP-complete problems are actually in uniform $\mathsf{AC}^0_2$, see "[Reducing the Complexity of Reductions](ftp://athos.rutgers.edu/http/http/cs/pub/allender/stoc97.pdf)".
Kaveh
CC BY-SA 3.0
2016-10-23T17:41:50.093Z
Regarding Sam's paper, it was the first result showing that BFV is in ALogTime, but BFE is complete even under AC0. The main difficulty of evaluating formulas in ALogTime is balancing formulas, if a formula is balanced there is a trivial ALogTime algorithm. But because of Sam's algorithm we know that [formula balancing is in AC0](http://cstheory.stackexchange.com/q/14892/). What Sam means by optimality of this result is that BFV is hard for ALogTime so it cannot be in a smaller class.
Kaveh
CC BY-SA 3.0
2016-10-24T06:30:03.640Z
For the definition of NP, it is enough to require that witnesses can be checked in coNLogTime.
Emil Jeřábek
CC BY-SA 3.0
2016-10-24T11:57:07.780Z
@Ricky that's the same paper that I linked to above. Yes, they indeed give a construction to build such NP-complete problems. (I was referring to all known natural NP-complete problems.)
Kaveh
<cc.complexity-theory><reductions>
Can coNLogTime verification be used instead of PTime verification when characterising NP?
Thomas Klimpel
# Can coNLogTime verification be used instead of PTime verification when characterising NP?

(Asked by: username_0 on 2016-10-23)

I recently read a paper that presented a proof calculus where the verification of whether a given proof is valid was NL-complete. The authors apparently decided that the checking procedure was not local enough, and defined a modified notion of proof where (practically speaking) the execution trace of the dynamic programming algorithm doing the NL-complete checking in polytime was part of the proof. That modified notion of proof could now obviously be verified by very local checks.

I was both negatively shocked and positively surprised by this:

* The negative shock was that this gratuitous size increase of the witness string of an NP problem during a reduction doesn't seem to be penalised or even noticed for the common notions of reduction. I wondered whether there is any way to fix this, but I guess this is a difficult question. But if you know how to fix this, please let me know.
* The positive surprise was that their trick seems to be applicable to arbitrary problems from NP to make the verification of the witness string locally checkable. The idea is to just declare the execution trace of the PTime verification algorithm to be a part of the witness string.

Is the observation correct that the extended witness string still satisfies the polynomial size bounds as required by the definition of NP? What is the correct notion to capture what is meant by "can be verified by very local checks"? I initially proposed ALogTime, but the comments by Kaveh and Emil Jeřábek indicate that DLogTime-uniform AC0 would be more appropriate (and that coNLogTime is already sufficient).

---

Note that

> coNLogTime $\subset$ DLogTime-uniform AC0 $\subset$ ALogTime and  
> ALogTime = DLogTime-uniform NC1 = $U\_{E^\*}$-uniform NC1 $\subset$ L-uniform NC1.

and that the abstract of [The Boolean formula value problem is in ALOGTIME](http://www.math.ucsd.edu/~sbuss/ResearchWeb/Boolean/paper.pdf) by Sam Buss says

> These results are optimal since the Boolean formula value problem is complete for alternating log time under deterministic log time reductions.

**Tags:** cc.complexity-theory, reductions
> **Comments:**
> **username_1**: Yes it can, if well-known, even AC^0 is sufficient. Just look at the NP-compeleteness proof of CNF-SAT. This is essentially the trick to reduce SAT to CNF-SAT.  
> **username_0**: @Kaveh Ah, now I understand for the first time why people here keep emphasising AC^0 reductions. But I'm not sure yet whether AC^0 is really sufficient, because I don't know whether the reduction from SAT to CNF-SAT is in AC^0, and I don't know whether the reduction from NP to SAT is in AC^0 (or at least whether the reductions are verifiable in AC^0). The abstract from Sam Buss' paper seems to indicate that AC^0 won't be enough.  
> **username_1**: All known reductions between NP-complete problems are actually in uniform $\mathsf{AC}^0_2$, see "[Reducing the Complexity of Reductions](ftp://athos.rutgers.edu/http/http/cs/pub/allender/stoc97.pdf)".  
> **username_1**: Regarding Sam's paper, it was the first result showing that BFV is in ALogTime, but BFE is complete even under AC0. The main difficulty of evaluating formulas in ALogTime is balancing formulas, if a formula is balanced there is a trivial ALogTime algorithm. But because of Sam's algorithm we know that [formula balancing is in AC0](http://cstheory.stackexchange.com/q/14892/). What Sam means by optimality of this result is that BFV is hard for ALogTime so it cannot be in a smaller class.  
> **username_2**: For the definition of NP, it is enough to require that witnesses can be checked in coNLogTime.  
> **username_1**: @Ricky that's the same paper that I linked to above. Yes, they indeed give a construction to build such NP-complete problems. (I was referring to all known natural NP-complete problems.)  

---

## 0 answers

