Vérifier l'exactitude de l'élimination du quantificateur, à l'aide de SAT

Laisser $x=(x_1,\dots,x_n)$ et $y=(y_1,\dots,y_n)$ être $n$-vecteurs de variables booléennes. J'ai un prédicat booléen$Q(x,y)$ sur $x,y$. Je donne mon ami Priscilla$Q(x,y)$. En réponse, elle me donne$P(x)$, un prédicat booléen sur $x$et elle prétend que

ou en d'autres termes, que

Je voudrais vérifier sa réclamation en quelque sorte. Comment Priscilla peut-elle m'aider à vérifier cette affirmation?

Vous pouvez supposer que les deux $P$ et $Q$ sont représentés comme des formules CNF, et qu'ils ne sont pas trop grands (taille polynomiale, ou quelque chose).

Dans un monde idéal, ce serait génial si je pouvais réduire le problème de vérification de cette réclamation auprès de SAT: j'ai un solveur SAT, et ce serait génial si je pouvais utiliser le solveur SAT pour vérifier cette réclamation. Cependant, je suis à peu près sûr qu'il ne sera pas possible de formuler le problème de la vérification de cette revendication directement en tant qu'instance SAT; tester la validité d'une formule 2QBF est presque certainement plus difficile que SAT. (Le$\Leftarrow$ la direction est facile à formuler comme une instance SAT, mais la $\Rightarrow$ la direction est difficile car elle implique intrinsèquement deux quantificateurs alternés.)

Mais supposons que Priscilla puisse me fournir des preuves supplémentaires pour étayer sa demande. Y a-t-il des preuves supplémentaires ou un témoin que Priscilla pourrait me donner, ce qui me permettrait de vérifier facilement sa demande? En particulier, y a-t-il des preuves ou des témoins supplémentaires qu'elle pourrait me fournir, qui me permettraient de formuler facilement le problème de la vérification de sa réclamation en tant qu'instance de SAT (à laquelle je peux ensuite appliquer mon solveur SAT)?

Un aspect inhabituel de mon environnement est que je suppose (heuristiquement) que j'ai un oracle pour SAT. Si vous aimez la théorie de la complexité, vous pouvez y penser de cette façon: je prends le rôle d'une machine capable de calculer des choses dans$P^{NP}$ (c.-à-d. $\Delta^P_2$), et je cherche à vérifier l'affirmation de Priscilla à l'aide d'un algorithme $P^{NP}$. Merci à mdx pour cette façon de penser les choses.

Ma motivation / application: je cherche à faire une vérification formelle d'un système (par exemple, vérification de modèle symbolique), et une étape clé du raisonnement implique l'élimination du quantificateur (c'est-à-dire, à partir de $Q$, obtenez $P$). J'espère un moyen propre de vérifier que l'élimination du quantificateur a été effectuée correctement.

S'il n'y a pas de solution qui fonctionne pour tous les possibles $P,Q$, n'hésitez pas à suggérer une solution "saine mais pas complète", c'est-à-dire une technique qui, pour $P,Q$me permet de vérifier l'équivalence revendiquée. (Même s'il ne parvient pas à vérifier la réclamation sur certains$P,Q$qui satisfont la demande, je peux toujours essayer cela comme une heuristique, tant qu'il ne prétend jamais à tort avoir vérifié une fausse demande. Sur tout donné$P,Q$, cela pourrait fonctionner ou non; si cela ne fonctionne pas, je ne suis pas pire que là où j'ai commencé.)

Voici deux techniques que j'ai pu identifier:

• Identifiez une fonction Skolem explicite. Supposons que Priscilla puisse identifier une fonction explicite$f$ tel que

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

  tient. Il s'ensuit ensuite que la prétention de Priscilla est correcte.

  Cela signifie que Priscilla peut nous aider à vérifier sa demande en fournissant une fonction $f$de sorte que la proposition ci-dessus est valable. Nous pouvons confirmer que la proposition ci-dessus est vraie en testant la formule suivante pour la satisfiabilité:

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

  Si cette formule n'est pas satisfaisante, la réclamation de Priscilla a été vérifiée.

  Une mise en garde est que Priscilla doit être en mesure d'identifier une fonction appropriée $f$. Une autre mise en garde est que nous avons besoin$f$être concrètement représentable sous une forme concise, disons, comme un circuit booléen de taille polynomiale. Cependant, si ces conditions sont remplies, cette technique devrait fonctionner.

• Un argument hybride. Considérons le cas particulier de ce problème, où nous quantifions sur une variable d'un bit (plutôt qu'un$n$-bit variable); il s'avère que le problème est facile à résoudre dans ce cas. Cela suggère que nous essayons d'enchaîner cette technique$n$ fois, chaque fois en supprimant un bit de plus $y$. Il s'avère que cette idée fonctionnera parfois, mais pas toujours.

  Permettez-moi d'expliquer comment vérifier la réclamation de Priscilla dans le cas où $y=(y_1)$est une variable d'un bit. alors$\exists y . Q(x,y)$ est équivalent à $Q(x,\text{False}) \lor Q(x,\text{True})$. Cette dernière formule est au plus deux fois plus grande que$Q$, donc toujours de taille polynomiale. Maintenant, nous pouvons utiliser notre solveur SAT pour tester si$Q(x,\text{False}) \lor Q(x,\text{True})$ est équivalent à $P(x)$; l'équivalence est exacte si la formule suivante n'est pas satisfaisable:

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

  Donc, si nous quantifions sur un seul bit, cela donne un moyen de vérifier que l'élimination du quantificateur a été effectuée correctement.

  Pour résoudre le problème d'origine, appliquez ceci plusieurs fois. Le travail de Priscilla sera de nous donner$n+1$ prédicats booléens $R_0,R_1,R_2,\dots,R_n$ tel que

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

  Notre tâche sera de vérifier si tous ces prédicats booléens ont été correctement générés. Nous pouvons le faire en testant si$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$}.$$

  Notez que ce dernier est une instance d'élimination de quantificateur avec un seul bit, nous avons donc déjà décrit comment tester qu'il a été fait correctement en utilisant un solveur SAT. Nous pouvons également tester si$Q \equiv R_0$ et $P \equiv R$en utilisant un solveur SAT directement. Ainsi, nous pouvons vérifier si Priscilla a généré$R_0,\dots,R_n$correctement. Si c'est le cas, nous avons vérifié que$P$ a été généré correctement.

  Une mise en garde est que Priscilla doit être en mesure de générer le $R_i$'s. Une mise en garde plus importante est que la taille de tous les$R_i$doit être raisonnable (par exemple, de taille polynomiale). Si Priscilla génère le$R_i$naïvement, leur taille pourrait croître de façon exponentielle avec $i$, ce qui n'est pas bon. Ainsi, Priscilla aura besoin d'un moyen de simplifier à chaque étape; il doit exister une séquence de$R_0,\dots,R_n$qui sont tous de taille polynomiale, et Priscilla doit pouvoir trouver une telle séquence. Ce n'est nullement garanti. Cela dit, si Priscilla peut le faire, cette technique devrait fonctionner.

Je ne suis pas entièrement satisfait de ces techniques - ce sont des heuristiques incomplètes, et elles peuvent échouer sur certains / nombreux exemples de problèmes - donc je serais toujours intéressé de voir d'autres façons d'aborder ce problème.