Loading ...
Sorry, an error occurred while loading the content.

[My Computational Complexity Web Log] Is Satisfiability Checkable?

Expand Messages
  • Lance Fortnow
    Time for another of my favorite open questions: Is Boolean Formula Satisfiability (SAT) checkable? The best notion of program checking comes from a paper by
    Message 1 of 1 , Mar 23, 2004
    • 0 Attachment
      Time for another of my favorite open questions: Is Boolean Formula Satisfiability (SAT) checkable?

      The best notion of program checking comes from a paper by Manuel Blum and Sampath Kannan. Let P be a program claiming to compute a language L. A program checker M for L is a probabilistic polynomial-time Turing machine with access to P as an oracle that outputs either "P(x)=L(X)" or "P incorrectly computes x on some input."

      We say L is checkable if for all oracle P and inputs x,

      1. If P(x)≠L(x) then with high probability MP(x) outputs "P incorrectly computes x on some input", and
      2. If P=L then with high probability MP(x) outputs "P(x)=L(x)".
      If P is correct on x and incorrect somewhere else, MP(x) can output either answer.

      Blum and Kannan show a nice connection to interactive proofs. We say a language L has a function-restricted interactive proof (FRIP) if there is a PCP for L where the proof for x in L is computable with an oracle for L. We have the following equivalence for all languages L

      1. L is checkable.
      2. Both L and L have FRIPs.
      Checkable languages include Graph Isomorphism, the Permanent and all of the PSPACE-complete and EXP-complete sets.

      Back to whether SAT is checkable. SAT has a FRIP by using self-reduction. So whether SAT is checkable is equivalent to whether SAT has a FRIP.

      All of the known PCPs for SAT seem to require counting, a prover hard for #P or at least ModkP for some k. Whether one can find a PCP for SAT that is even in the polynomial-time hierarchy remains open.

      Perhaps one can show some consequence of the checkability of SAT perhaps that the polynomial-time hierarchy collapses. Bogdanov and Trevisan have the best result in this direction; they show that if SAT has a non-adaptive self-corrector then PH collapses to third level. Though many checking results use self-correction there still could be some completely different way to show SAT is checkable.

      --
      Posted by Lance Fortnow to My Computational Complexity Web Log at 3/23/2004 06:25:58 AM

    Your message has been successfully submitted and would be delivered to recipients shortly.