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

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

<p>I am aware of Goldwasser et al.'s <em>Delegating Computation</em>, 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.</p>

<p>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!</p>

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

CC BY-SA 3.0
2018-02-27T16:40:06.957Z
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?
D.W.
CC BY-SA 3.0
2018-02-27T17:11:59.573Z
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?
David Monniaux
<np-complete><interactive-proofs><model-checking><pspace>
Practical interactive proof schemes for NP-hard problems
David Monniaux
# Practical interactive proof schemes for NP-hard problems

(Asked by: username_0 on 2018-02-26)

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

**Tags:** np-complete, interactive-proofs, model-checking, pspace

> **Comments:**
> **username_1**: 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?  
> **username_0**: 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?  

---

## 0 answers

