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 '18 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$ – David Monniaux Feb 27 '18 at 17:11

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.