8
$\begingroup$

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

Improve this question
$\endgroup$
2
  • $\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$
    – David Monniaux
    Feb 27, 2018 at 17:11

0

Reset to default

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.