A Resolution-Based Interactive Proof System for UNSAT

1. Problématique et Contexte

Le déséquilibre des certificats SAT/UNSAT :
Les solveurs SAT modernes doivent produire des certificats de correction. Pour les formules satisfaisables (SAT), un certificat (une affectation satisfaisante) est vérifiable en temps polynomial. En revanche, pour les formules insatisfaisables (UNSAT), les certificats traditionnels (comme les preuves de résolution ou les certificats DRAT) peuvent avoir une taille exponentielle par rapport à la taille de la formule.

• Conséquence pratique : Dans un scénario de service de résolution où un client faible en puissance de calcul envoie une formule à un serveur puissant, la vérification du certificat par le client devient impossible si celui-ci est trop volumineux (atteignant parfois des téraoctets).

Limites des approches existantes :
Le théorème $IP = PSPACE$ (Shamir, 1992) garantit l'existence de protocoles interactifs où le vérificateur travaille en temps polynomial. Cependant, les protocoles existants pour l'UNSAT reposent souvent sur des preuves de complexité asymptotique qui nécessitent que le "Prouveur" génère la table de vérité complète (temps exponentiel même dans le meilleur des cas), ce qui les rend incompatibles avec les algorithmes de résolution modernes.
Une approche récente (Couillard et al.) a proposé des protocoles interactifs compétitifs pour les algorithmes basés sur les Diagrammes de Décision Binaire (BDD), mais aucun solveur SAT moderne n'utilise les BDD comme moteur principal.

Question centrale : Peut-on concevoir des protocoles de preuve interactifs qui soient "compétitifs" (c'est-à-dire avec une surcharge polynomiale pour le Prouveur) par rapport à des algorithmes de résolution pratiques, comme la procédure de Davis-Putnam ?

2. Méthodologie

Les auteurs proposent un cadre théorique pour transformer un algorithme de décision UNSAT en un protocole de preuve interactif compétitif.

A. Définition de la compétitivité :
Un protocole interactif est dit compétitif par rapport à un algorithme $Alg$ si le temps d'exécution du Prouveur dans le protocole est borné par un polynôme multiplié par le temps d'exécution de $Alg$. L'objectif est d'ajouter la vérification interactive sans rendre le Prouveur exponentiellement plus lent que l'algorithme de base.

B. Arithmétisation et Compatibilité :
La méthode repose sur l'arithmétisation (encodage des formules booléennes en polynômes sur un corps fini), technique fondamentale du théorème $IP = PSPACE$.

• L'idée est de mapper chaque étape de l'algorithme (macro-étape) à une opération sur des polynômes.
• Définition clé : Une arithmétisation $A$ est dite compatible avec une macro-étape $M$ (ex: résolution ou nettoyage de clauses) s'il existe une opération sur les polynômes $P_M$ qui commute avec l'évaluation partielle. Cela signifie que l'ordre des opérations (appliquer $M$ puis évaluer, ou évaluer puis appliquer $P_M$) n'a pas d'importance.

C. Le Théorème Principal (Théorème 5.6) :
Les auteurs prouvent que la recherche d'un protocole interactif compétitif pour un algorithme $Alg$ se réduit à la recherche d'une arithmétisation compatible avec $Alg$. Si une telle arithmétisation existe et satisfait certaines bornes de degré et de taille, un protocole existe où :

1. Le Vérificateur travaille en temps polynomial.
2. Le Prouveur travaille en temps $O(T \cdot poly(n))$, où $T$ est le temps de $Alg$.

D. Application à Davis-Putnam :
Les auteurs appliquent ce cadre à la procédure de Davis-Putnam (une variante de la résolution).

• Problème : Les arithmétisations standards (comme celle de [LFKN92]) ne sont pas compatibles avec la résolution de Davis-Putnam car elles ne respectent pas les propriétés de commutativité requises lors de l'élimination de variables.
• Solution : Ils introduisent une arithmétisation non standard (notée $B$). Cette arithmétisation utilise des puissances spécifiques (ex: $x^3$ pour $\neg x$) et des opérations de réduction de polynômes ($\gamma_x$ et $\delta_x$) conçues spécifiquement pour simuler les étapes de résolution complète ($R_x$) et de nettoyage ($C_x$) de Davis-Putnam tout en préservant la compatibilité.

3. Contributions Clés

1. Théorème de réduction : Établissement d'un lien formel entre la conception de protocoles interactifs compétitifs et la recherche d'arithmétisations compatibles.
2. Premier protocole pour la résolution : Présentation du premier protocole de preuve interactif compétitif pour la procédure de Davis-Putnam, un algorithme historique de résolution.
3. Arithmétisation non standard : Découverte qu'une arithmétisation non standard est nécessaire pour rendre la procédure de Davis-Putnam compatible avec les preuves interactives, contournant les limitations des méthodes classiques.
4. Implémentation et évaluation : Développement d'un outil nommé icdp (Interactively Certified Davis-Putnam) et réalisation d'expériences empiriques.

4. Résultats Expérimentaux

Les auteurs ont comparé la certification interactive (via icdp) avec la certification conventionnelle (envoi d'une preuve de résolution ou DRAT) sur un ensemble de 108 instances insatisfaisables.

• Temps du Prouveur : Le Prouveur interactif est plus lent que le solveur conventionnel, mais la surcharge est quasi-constante (facteur linéaire faible) par rapport au temps de résolution de Davis-Putnam. Cependant, comme Davis-Putnam est lui-même lent comparé aux solveurs modernes (CDCL), le temps absolu reste élevé.
• Temps du Vérificateur : C'est le gain majeur. Le vérificateur interactif est plus rapide de plusieurs ordres de grandeur (environ 10 fois plus rapide que les vérificateurs DRAT sur les instances testées, et théoriquement exponentiellement plus rapide pour de grandes instances). Il ne lit jamais la preuve complète.
• Complexité de communication : La taille des messages échangés dans le protocole interactif est extrêmement faible (quelques kilooctets) et croît très lentement par rapport à la taille de la preuve de résolution conventionnelle (qui peut atteindre des téraoctets). La communication interactive semble suivre une loi de puissance inverse par rapport à la taille de la preuve classique.
• Mémoire : Le Prouveur interactif consomme plus de mémoire (quadratique par rapport à l'algorithme de base) car il doit stocker les formules intermédiaires pour les envoyer au vérificateur dans l'ordre inverse de leur calcul.

5. Signification et Perspectives

• Preuve de concept : L'article démontre que les preuves interactives ne sont pas réservées aux algorithmes de force brute ou aux BDD, mais peuvent s'appliquer à des algorithmes de résolution, bien que l'arithmétisation doive être adaptée.
• Limites pratiques actuelles : Bien que le protocole soit théoriquement compétitif pour Davis-Putnam, Davis-Putnam est obsolète face aux solveurs modernes (CDCL). L'extension de cette technique aux solveurs modernes (CDCL) reste un défi ouvert, car les techniques actuelles ne s'étendent pas directement à ces algorithmes complexes.
• Potentiel futur : Si une arithmétisation compatible peut être trouvée pour les solveurs CDCL modernes, cela permettrait de déployer des services de résolution SAT distribués où un client faible peut vérifier l'insatisfaisabilité d'une formule complexe en temps polynomial et avec une communication minimale, résolvant ainsi le problème de la taille des certificats UNSAT.

En résumé, ce travail ouvre la voie à une nouvelle génération de certificats de correction pour les problèmes SAT/UNSAT, en remplaçant l'envoi de preuves massives par des échanges interactifs légers, au prix d'une légère surcharge de calcul pour le Prouveur.