4
$\begingroup$

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 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.

Improve this question
$\endgroup$
7
  • 1
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Commented Oct 23, 2016 at 15:36
  • $\begingroup$ @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. $\endgroup$
    – Thomas Klimpel
    Commented Oct 23, 2016 at 16:56
  • 1
    $\begingroup$ All known reductions between NP-complete problems are actually in uniform $\mathsf{AC}^0_2$, see "Reducing the Complexity of Reductions". $\endgroup$
    – Kaveh
    Commented Oct 23, 2016 at 17:32
  • 1
    $\begingroup$ 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. What Sam means by optimality of this result is that BFV is hard for ALogTime so it cannot be in a smaller class. $\endgroup$
    – Kaveh
    Commented Oct 23, 2016 at 17:41
  • 4
    $\begingroup$ For the definition of NP, it is enough to require that witnesses can be checked in coNLogTime. $\endgroup$
    – Emil Jeřábek
    Commented Oct 24, 2016 at 6:30

0

Reset to default

Your Answer

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

Browse other questions tagged or ask your own question.