Verify correctness of quantifier elimination, using SAT

Question

Let $x=(x_1,\dots,x_n)$ and $y=(y_1,\dots,y_n)$ be $n$-vectors of boolean variables. I have a boolean predicate $Q(x,y)$ on $x,y$. I give my friend Priscilla $Q(x,y)$. In response, she gives me $P(x)$, a boolean predicate on $x$, and she claims that

$$P(x) \equiv \exists y . Q(x,y),$$

or in other words, that

$$\forall x . [P(x) \Leftrightarrow \exists y . Q(x,y)].$$

I would like to verify her claim somehow. How can Priscilla help me verify this claim?

You can assume that both $P$ and $Q$ are represented as CNF formulas, and that they're not too large (polynomial size, or something).

In an ideal world, it'd be awesome if I could reduce the problem of verifying this claim to SAT: I have a SAT solver, and it'd be great if I can use the SAT solver to verify this claim. However, I'm pretty sure that it's not going to be possible to formulate the problem of verifying this claim directly as a SAT instance; testing the validity of a 2QBF formula is almost certainly harder than SAT. (The $\Leftarrow$ direction is easy to formulate as a SAT instance, but the $\Rightarrow$ direction is hard because it inherently involves two alternating quantifiers.)

But suppose Priscilla could give me some additional evidence to support her claim. Is there some additional evidence or witness Priscilla could give me, which would make it easy for me to verify her claim? In particular, is there some additional evidence or witness she could give me, which would make it easy for me to formulate the problem of verifying her claim as an instance of SAT (which I can then apply my SAT solver to)?

One unusual aspect of my setting is that I'm assuming (heuristically) that I have an oracle for SAT. If you like complexity theory, you can think about it this way: I am taking the role of a machine that can compute things in $P^{NP}$ (i.e., in $\Delta^P_2$), and I'm looking to verify Priscilla's claim using an algorithm in $P^{NP}$. My thanks to mdx for this way of thinking about things.

---

My motivation/application: I'm looking to do formal verification of a system (e.g., symbolic model checking), and a key step in the reasoning involves quantifier elimination (i.e., starting from $Q$, obtain $P$). I'm hoping for some clean way to verify that the quantifier elimination was done correctly.

If there's no solution that works for all possible $P,Q$, feel free to suggest a solution that is "sound but not complete", i.e., a technique that for many $P,Q$ lets me verify the claimed equivalence. (Even if it fails to verify the claim on some $P,Q$ that do satisfy the claim, I can still try this as a heuristic, as long as it never inappropriately claims to have verified a false claim. On any given $P,Q$, it might work, or it might not; if it doesn't work, I'm no worse off than where I started.)

Answer 1

Here are two techniques I've been able to identify:

• Identify an explicit Skolem function. Suppose Priscilla can identify an explicit function $f$ such that

  $$\forall x . P(x) \Leftrightarrow Q(x,f(x))$$

  holds. Then it follows that Priscilla's claim is correct.

  This means that Priscilla can help us verify her claim by providing a function $f$ so that the above proposition holds. We can confirm that the above proposition holds by testing the following formula for satisfiability:

  $$\neg (P(x) \Leftrightarrow Q(x,f(x))).$$

  If this formula is not satisfiable, then Priscilla's claim has been verified.

  One caveat is that Priscilla needs to be able to identify a suitable function $f$. A further caveat is that we need $f$ to be concretely representable in some concise form, say, as a polynomial-sized boolean circuit. However, if those conditions are met, then this technique should work.

• A hybrid argument. Consider the special case of this problem, where we are quantifying over a one-bit variable (rather than a $n$-bit variable); it turns out the problem is easy to solve in this case. This suggests that we try to chain that technique $n$ times, each time removing one more bit of $y$. It turns out that this idea will sometimes work, but not always.

  Let me explain how to verify Priscilla's claim in the case where $y=(y_1)$ is a one-bit variable. Then $\exists y . Q(x,y)$ is equivalent to $Q(x,\text{False}) \lor Q(x,\text{True})$. The latter formula is at most twice as large as $Q$, so still polynomial sized. Now we can use our SAT solver to test whether $Q(x,\text{False}) \lor Q(x,\text{True})$ is equivalent to $P(x)$; the equivalence holds exactly if the following formula is not satisfiable:

  $$\neg (P(x) \Leftrightarrow (Q(x,\text{False}) \lor Q(x,\text{True}))).$$

  So, if we're quantifying over a single bit, this gives a way to verify that the quantifier elimination was done correctly.

  To solve the original problem, apply this multiple times. Priscilla's job will be to give us $n+1$ boolean predicates $R_0,R_1,R_2,\dots,R_n$ such that

  $$R_i(x,(y_{i+1},\dots,y_n)) \equiv \exists y_1,y_2,\dots,y_i . Q(x,y).$$

  Our task will be to verify whether all of these boolean predicates were correctly generated. We can do this by testing whether $Q(x,y) \equiv R_0(x,y)$, $P(x) \equiv R_n(x)$,

  $$R_{i+1}(x,(y_{i+2},\dots,y_n)) \equiv \exists y_{i+1} . R_i(x,(y_{i+1},\dots,y_n)) \qquad \text{for $i=1,2,\dots,n-1$}.$$

  Notice that the latter is an instance of quantifier elimination with a single bit, so we've already described how to test it was done correctly using a SAT solver. We can also test whether $Q \equiv R_0$ and $P \equiv R$ using a SAT solver straightforwardly. So, we can check whether Priscilla generated $R_0,\dots,R_n$ correctly. If she did, then we've verified that $P$ was generated suitably.

  One caveat is that Priscilla needs to be able to generate the $R_i$'s. A bigger caveat is that the size of all the $R_i$'s needs to be reasonable (say, polynomial-sized). If Priscilla generates the $R_i$'s naively, their size might grow exponentially with $i$, which is no good. So, Priscilla will need a way to simplify at each stage; there needs to exist some sequence of $R_0,\dots,R_n$ that are all polynomial-sized, and Priscilla needs to be able to find such a sequence. That is by no means guaranteed. That said, if Priscilla can do this, then this technique should work.

I'm not fully satisfied with these techniques -- they are incomplete heuristics, and they might fail on some/many problem instances -- so I would still be interested to see other ways of approaching this problem.