INSTRUCTIONS AU MODÈLE - Répondre sans outil externe ni Internet. - Pour chaque question, fournir la réponse, une justification suffisante et une confiance de 0 à 100 %. - Ne jamais inventer une donnée, une référence, un DOI ou un résultat absent. - Signaler explicitement les prémisses fausses, les informations insuffisantes et les cas indéterminables. - Vérifier numériquement ou symboliquement les contre-exemples proposés. - Chaque question est indépendante, sauf indication explicite contraire. Q063 — SAT à 2 littéraux par clause est-il polynomialement décidable ? Nommer une méthode standard.
Oui, le problème SAT restreint aux clauses contenant au plus deux littéraux, c’est-à-dire 2-SAT, est polynomialement décidable. Il appartient en effet à la classe de complexité P. La méthode standard pour le résoudre en temps polynomial repose sur le graphe d’implications et la recherche de composantes fortement connexes. Chaque clause à deux littéraux, de la forme (l₁ ∨ l₂), est logiquement équivalente aux deux implications (¬l₁ → l₂) et (¬l₂ → l₁). On construit alors un graphe orienté dont les sommets sont les littéraux et leurs négations, et dont les arcs représentent ces implications. Une instance de 2-SAT est satisfiable si et seulement si, pour aucune variable x, les littéraux x et ¬x n’appartiennent à la même composante fortement connexe du graphe. La détection des composantes fortement connexes s’effectue en temps linéaire, par exemple grâce à l’algorithme de Tarjan ou à celui de Kosaraju, ce qui donne une complexité globale en O(n + m), où n désigne le nombre de variables et m le nombre de clauses. Ce résultat contraste nettement avec le problème général SAT, dont la version 3-SAT est NP-complet. Confiance : 96 %. Ce résultat est un théorème classique et solidement établi de la théorie de la complexité ; ma confiance est élevée mais plafonne en deçà de 100 % car il s’agit d’un fait énoncé de mémoire, non redémontré ici.
Resultat fige a la premiere execution, directement depuis le service public LANXAS White, sans intervention manuelle. Cette page est permanente et peut etre re-consultee pour verification.