Algorithmes, structures de données et procédures pour déterminer si une formule booléenne propositionnelle (typiquement en forme normale conjonctive) est satisfaisable, et pour produire une affectation satisfaisante quand elle existe ; la résolution SAT moderne inclut DPLL, CDCL, heuristiques, apprentissage de clauses, redémarrages et prétraitement.

Principe

Chercher systématiquement une affectation booléenne qui satisfait toutes les clauses par recherche avec retour arrière (style DPLL), augmentée par l'apprentissage de clauses piloté par conflits (CDCL), la propagation d'unités, des heuristiques de sélection de variables et l'enregistrement de preuves ou d'unsat cores pour améliorer l'efficacité et fournir des preuves d'insatisfiabilité.

Démonstration

Pour une instance CNF encodant une contrainte d'ordonnancement, un solveur CDCL effectue la propagation d'unités pour déduire des affectations forcées, branche sur une variable choisie, enregistre des clauses apprises issues de conflits pour éviter de répéter des affectations partielles invalides, puis renvoie finalement une affectation complète satisfaisante ou une preuve d'insatisfiabilité.

Mauvaise application

Fournir à un solveur SAT un problème sans encodage approprié (perdant la sémantique), attendre un comportement polynomial dans le pire cas sur des instances NP‑complètes, ou mal interpréter le résultat 'unknown' ou un time‑out comme satisfaisable ou insatisfaisable sans analyse complémentaire.

Conséquence

Les solveurs SAT fournissent des moteurs très efficaces pour de nombreux problèmes NP pratiques via des encodages (planification, vérification, synthèse), produisent des modèles concrets pour les instances satisfaisables et peuvent fournir des preuves par résolution ou des unsat cores pour les cas insatisfaisables ; ils sont très scalables en pratique malgré la difficulté théorique.

Inversion

Le comptage des solutions (#SAT) ou la résolution de formules booléennes quantifiées (QBF) inverse le problème SAT en traitant l'énumération ou des alternances de quantificateurs supplémentaires, ce qui est strictement plus difficile et exige des algorithmes et des considérations de complexité différents.

Limite

S'applique à la logique propositionnelle ; les problèmes doivent être encodés (souvent en CNF) et l'efficacité du solveur dépend fortement de la qualité de l'encodage et des heuristiques. La résolution SAT est décidable et complète pour la propositionnelle mais ne traite pas directement des théories (utiliser SMT pour le raisonnement en théorie).

Tension sémantique

Tension entre SAT et la programmation par contraintes ou SMT : SAT repose sur des encodages binaires et l'apprentissage de clauses, tandis que CP utilise des domaines plus riches et la propagation ; SMT étend SAT en intégrant des théories, échangeant performance booléenne brute contre expressivité.

Synthèse

La résolution SAT est une approche mûre et très axée sur l'ingénierie pour décider la satisfiabilité propositionnelle : elle combine recherche systématique avec des mécanismes d'inférence et d'apprentissage puissants pour produire des affectations ou des preuves, et sert de moteur pour de nombreuses tâches de raisonnement de niveau supérieur via encodage.