Model-checking (in the sense of reachability in a succinct graph) is PSPACE-complete. SAT is NP-complete. Both problems are considered intractable, yet there exist tools capable of solving them on many industrially relevant instances.

Since IP=PSPACE, I was wondering whether there are approaches capable of performing interactive proofs on "realistic" instances of co-NP-hard problems.

I am aware of Goldwasser et al.'s Delegating Computation, but they focus on tractable problems (prover in P) with a very fast verifier. I'm rather considering difficult problems, such as showing that a propositional formula is unsatisfiable.

Obviously, for model-checking, I could encode the problem into TQBF (using Savitch's construction), then use Shamir and Shen's reduction to IP. I believe, however, that this would not yet anything workable even on instances on which known model-checking algorithms (e.g. based on ROBDDs or IC3) would work. As far as I know, reducing model-checking of non-toy examples to TQBF yields formulas that none of the best QBF solvers can deal with!

I realize this is not truly a theory question, since I'm requesting an answer about "workable" solutions rather than something along the lines of "this would require a prover capable of solving intractable problems so it's impossible".

  • $\begingroup$ Co-NP-hard is a lower bound, not an upper bound. Can you give a more precise characterization of what problems you're looking to solve? Are you asking for a practical method for interactive proofs of TQBF? For instance, there are often-practical methods for (non-)interactive proofs of problems in co-NP (some SAT solvers can provide a proof of unsatisfiability; look up SAT solvers and refutation, unsatisfiable cores, resolution graphs, etc.), but here "co-NP" is different from "co-NP-hard". Is that the kind of thing you're looking for? $\endgroup$
    – D.W.
    Feb 27, 2018 at 16:40
  • $\begingroup$ The proofs of unsatisfiability produced by SAT solvers are quite large, even though the DRUP format is terser than resolution-based proofs. I would like something replacing those huge logs files by some interactive proofs. Similarly, one can ask a model-checker to provide an inductive invariant entailing a safety property, but it may be huge; would it be possible to replace it by an interactive proof? $\endgroup$ Feb 27, 2018 at 17:11


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.