An Efficient Algorithm for Solving the 2-MAXSAT Problem

Résumé technique : Un algorithme efficace pour la résolution du problème 2-MAXSAT

Définition du problème
L'article traite du problème 2-MAXSAT, une version restreinte du problème de satisfaction maximale (MAXSAT). Étant donné un ensemble $V$ de $m$ variables booléennes et une collection $C$ de $n$ clauses en Forme Normale Conjonctive (FNC), où chaque clause contient au plus deux littéraux, l'objectif est de trouver une affectation de vérité qui maximise le nombre de clauses satisfaites. Le problème est établi comme étant NP-complet, même sous cette restriction.

Méthodologie
L'algorithme proposé s'écarte des méthodes traditionnelles de type « branch-and-bound » ou d'approximation en transformant le problème en une tâche de maximisation de Forme Normale Disjonctive (FND) et en utilisant une structure de recherche spécialisée basée sur les graphes. La méthodologie se déroule en trois étapes principales :

1. Transformation en FND :
   L'algorithme construit une nouvelle formule $D$ en FND à partir de la formule FNC originale $C$. Pour chaque clause $C_i = l_{i1} \lor l_{i2}$ dans $C$, l'algorithme introduit une nouvelle variable auxiliaire $x_i$ et génère deux conjonctions : $D_{i1} = l_{i1} \land x_i$ et $D_{i2} = l_{i2} \land \neg x_i$. La formule $D$ résultante se compose de $2n$ conjonctions. La Proposition 1 de l'article établit que $C$ possède au moins $n^*$ clauses satisfaites si et seulement si $D$ possède au moins $n^*$ conjonctions satisfaites sous une affectation de vérité pour $V \cup \{x_1, \dots, x_n\}$.

2. Représentation graphique (graphes p et Tries) :*
   Pour représenter efficacement les affectations de vérité qui satisfont les conjonctions dans $D$, l'article introduit le graphe p*.

   • Séquences de variables : Chaque conjonction est convertie en une séquence de variables triée basée sur la fréquence globale d'apparition des variables. Les littéraux négatifs sont gérés par l'introduction d'une notation spéciale $(c, *)$, représentant que la variable $c$ peut être vraie ou fausse (ou ignorée) sans affecter la vérité de la conjonction.
   • Graphes p : Un graphe orienté représentant une seule conjonction où les nœuds correspondent aux variables dans la séquence. Les « spans » (arêtes sautant des variables) représentent les options $(c, *)$.
   • Graphes p :* Un raffinement des graphes p où les « spans chevauchants » (variables optionnelles consécutives) sont fusionnés via la clôture transitive. Cela garantit que le graphe représente correctement toutes les affectations de vérité valides pour une conjonction spécifique.
   • Structure de type Trie ($G$) : Tous les graphes p* sont intégrés dans un seul graphe de type tri nommé $G$. Cette structure regroupe les séquences de variables communes pour éviter les vérifications redondantes. Le graphe inclut des « nœuds de branchement » là où les chemins divergent.

3. Recherche récursive ascendante (Bottom-Up) :
   Le cœur de l'algorithme, SEARCH(G), explore le graphe $G$ de manière ascendante (post-ordre) pour trouver le sous-ensemble maximal de conjonctions satisfaites.

   • Sous-ensembles atteignables (RS) : Pour un nœud de branchement $v$, l'algorithme calcule les « sous-ensembles atteignables » des nœuds atteignables via les spans depuis les ancêtres. Ces sous-ensembles représentent des groupes de conjonctions qui peuvent être satisfaites simultanément en contournant certaines variables.
   • Limites supérieures (upBounds) : Sur la base des RS, l'algorithme identifie des « limites supérieures » — des ensembles de nœuds qui permettent la fusion de sous-graphes.
   • Construction récursive : Lorsqu'un nœud de branchement est rencontré, l'algorithme construit un nouveau sous-graphe plus petit de type tri, enraciné dans les nœuds de la limite supérieure. Une racine virtuelle (le nœud de branchement d'origine) est ajoutée pour maintenir la connectivité. L'algorithme appelle récursivement SEARCH sur ces sous-graphes.
   • Optimisation : Pour éviter les calculs redondants, l'algorithme emploie deux améliorations : (1) limiter les calculs de RS au segment entre le nœud de branchement actuel et son ancêtre de branchement le plus bas, et (2) utiliser un tableau de hachage pour mettre en cache les résultats des sous-graphes déjà visités, supprimant ainsi les appels récursifs répétés.

Principales contributions

• Technique de transformation : Une réduction en temps polynomial du problème 2-MAXSAT à un problème de conjonction maximale en FND.
• Structure de graphe p :* La définition des graphes p* et de leur clôture transitive pour représenter de manière précise et compacte les affectations de vérité pour les conjonctions contenant des variables optionnelles.
• Recherche récursive sur Trie : Un nouvel algorithme récursif qui construit et parcourt dynamiquement une structure de graphe de type tri, utilisant des « sous-ensembles atteignables » et des « limites supérieures » pour fusionner efficacement les espaces de solutions.
• Analyse de complexité : L'article fournit une analyse détaillée affirmant que l'algorithme opère dans des limites de temps polynomial.

Résultats et Complexité
L'article affirme que la complexité temporelle dans le pire des cas de l'algorithme proposé est bornée par $O(n^2 m^4)$, où $n$ est le nombre de clauses et $m$ le nombre de variables.

• La construction du tri initial et des graphes p* prend $O(nm^2)$.
• La recherche récursive implique au plus $O(nm)$ nœuds de branchement.
• Chaque nœud de branchement est impliqué dans au plus $O(m)$ appels récursifs en raison de la réduction de la hauteur du graphe à chaque étape.
• Le coût de construction d'un sous-graphe par appel est de $O(nm^2)$.
• La combinaison de ces facteurs donne la borne $O(n^2 m^4)$.

Signification et Revendications
L'article conclut que puisque le problème 2-MAXSAT est connu pour être NP-complet, l'existence d'un algorithme en temps polynomial pour le résoudre constitue une preuve que P = NP. Les auteurs affirment que ce résultat constitue une preuve de P = NP, modifiant fondamentalement la compréhension de la complexité computationnelle pour les problèmes de satisfaction. Ce travail est présenté comme une modification et une extension d'un article de conférence, soutenu par le CRSNG, Canada.