Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking

Résumé Technique : Schémas de Dépendance Forts (D)QBF via Chemins Purs avec Applications à la Vérification de Preuves

Énoncé du Problème
La certification pour les Formules Booléennes Quantifiées (QBF) et les Formules Booléennes Quantifiées à Dépendances (DQBF) reste un défi majeur. Bien que des recherches récentes en complexité de preuves aient démontré que la règle « Extension Indépendante » (IndExt) permet au système de preuves IndExtQURes de p-simuler la vaste majorité des techniques QBF et DQBF existantes, IndExtQURes n'est pas encore un format de certification pratique. À l'inverse, des formats pratiques comme QRAT (Tautologie Asymétrique de Résolution Quantifiée) et sa généralisation DQBF, DQRAT (Tautologie Asymétrique de Résolution Quantifiée à Dépendances), manquent de la force théorique nécessaire pour p-simuler IndExtQURes. Plus précisément, DQRAT, qui repose sur le schéma de dépendance de chemin de résolution réflexif ($D_{rrs}$), n'a pas été prouvé comme équivalent en puissance à IndExtQURes, laissant un fossé entre l'optimalité théorique et la certification pratique.

Méthodologie
Les auteurs comblent ce fossé en introduisant un nouveau schéma de dépendance appelé $D_{\forall pure}$ (Schéma de Dépendance Universelle Pure). Ce schéma est basé sur le concept de « chemins purs », qui restreint les chemins de résolution entre les littéraux universels et existentiels. Contrairement au chemin de résolution réflexif standard ($D_{rrs}$), $D_{\forall pure}$ exclut les chemins de résolution d'un littéral universel $u$ vers un littéral existentiel $x$ si le chemin est simplement une extension d'un chemin de $\bar{u}$ vers $x$. Cela garantit que seules les dépendances minimales et nécessaires sont conservées.

La méthodologie comprend trois composantes principales :

1. Définition et Correction : Les auteurs définissent formellement $D_{\forall pure}$ en utilisant des constructions de point fixe sur des ensembles de clauses et de littéraux. Ils prouvent la correction sémantique de ce schéma (Théorème 10), démontrant que la suppression des dépendances fallacieuses identifiées par $D_{\forall pure}$ préserve la valeur de vérité de la DQBF.
2. Intégration dans les Systèmes de Preuves : Les auteurs intègrent $D_{\forall pure}$ dans le système de preuves DQRAT, créant un nouveau système noté DQRAT+$D_{\forall pure}$. Ils définissent également une règle de réduction locale, Loc$_{\forall pure}$-Red, qui permet la réduction directe de clauses contenant des littéraux universels sans altérer le préfixe, à condition qu'aucun chemin pur n'existe vers des clauses conflictuelles.
3. Analyse de Complexité : L'article établit la relation entre le nouveau système et IndExtQURes. Les auteurs prouvent que DQRAT+$D_{\forall pure}$ et IndExtQURes sont p-équivalents (équivalents en temps polynomial). Cela est obtenu en montrant que DQRAT+$D_{\forall pure}$ peut p-simuler IndExtQURes (en simulant la règle d'Extension Indépendante à l'aide du nouveau schéma de dépendance pour supprimer les dépendances inutiles) et que IndExtQURes peut p-simuler DQRAT+$D_{\forall pure}$.

Contributions Clés

• Nouveau Schéma de Dépendance ($D_{\forall pure}$) : L'article introduit un schéma de dépendance strictement plus fort que $D_{rrs}$ dans des contextes spécifiques (par exemple, la séparation de LD-Q(Drrs)-Res de LD-Q(D$_{\forall pure}$)-Res) tout en maintenant une vérification en temps polynomial.
• Équivalence des Systèmes de Preuves : La contribution théorique principale est la preuve que DQRAT+$D_{\forall pure}$ est p-équivalent à IndExtQURes. Cela implique que DQRAT+$D_{\forall pure}$ peut p-simuler tous les principaux systèmes de preuves QBF et DQBF que IndExtQURes peut simuler, y compris QRAT, G, et diverses règles de schémas de dépendance.
• Extraction de Stratégie : Les auteurs montrent que $D_{\forall pure}$ est un schéma de dépendance « normal », ce qui permet une extraction de stratégie en temps polynomial dans la Résolution Q à Longue Distance (LD-Q-Res). Ce résultat soutient l'intégration correcte de $D_{\forall pure}$ dans des solveurs comme Qute.
• Implémentation : Les auteurs ont implémenté un vérificateur de preuves prototype, DQRAT-check, qui prend en charge le format DQRAT+$D_{\forall pure}$. Ils ont également étendu le solveur Qute pour utiliser $D_{\forall pure}$ dans l'apprentissage de clauses.

Résultats

• Théorique : L'article démontre que $D_{\forall pure}$ permet la suppression de dépendances que $D_{rrs}$ ne peut pas éliminer, spécifiquement dans des cas impliquant des formules de parité « pontées » où $D_{rrs}$ échoue à détecter l'indépendance mais où $D_{\forall pure}$ réussit.
• Expérimental (Vérification de Preuves) : Le vérificateur prototype a été testé sur des benchmarks de QBFEval 2022 et des formules artificielles (incluant les exemples de l'article). Le vérificateur a validé avec succès les preuves. Les auteurs notent que l'extraction de preuves et la conversion du format QRP (format interne de Qute) vers DQRAT représentent 97 % du temps de vérification, tandis que le vérificateur DQRAT lui-même ne représente que 3 %.
• Expérimental (Résolution) : Lorsqu'intégré dans le solveur Qute, $D_{\forall pure}$ a montré des promesses sur les benchmarks QBFEval 2020, réduisant le temps de calcul des dépendances par un facteur de 7 et trouvant deux fois plus de paires indépendantes que $D_{rrs}$. Cependant, sur les benchmarks plus récents de QBFEval 2022, $D_{\forall pure}$ n'a détecté aucune nouvelle indépendance, et la surcharge n'a pas amélioré le nombre d'instances résolues ni les scores PAR2.

Signification
L'article affirme que sa signification principale réside dans le comblement du fossé entre la force théorique des preuves et les formats de certification pratiques. En montrant qu'une modification simple du cadre DQRAT existant (l'ajout de la règle $D_{\forall pure}$) produit un système p-équivalent au puissant IndExtQURes, les auteurs fournissent une voie vers une norme de certification unifiée et forte pour les QBF et les DQBF. Cela évite la nécessité de prouver des p-simulations pour chaque système de preuves individuel contre IndExtQURes, en s'appuyant plutôt sur la transitivité de l'équivalence entre DQRAT+$D_{\forall pure}$ et IndExtQURes. De plus, ce travail fournit une implémentation concrète (DQRAT-check) et démontre la faisabilité de l'intégration de ces schémas de dépendance forts dans l'infrastructure de résolution existante, ouvrant la voie à une certification plus robuste dans les futurs solveurs DQBF.