La procédure algorithmique qui détermine si une formule propositionnelle ou booléenne admet au moins une assignation de valeurs de vérité rendant la formule vraie ; appliquée généralement à des formules en forme normale conjonctive (FNC) et mise en œuvre par des solveurs SAT.

Principe

Réduire la satisfiabilité logique à une recherche guidée sur les assignations complétée par de l'inférence et de l'apprentissage : explorer systématiquement des assignations partielles, propager les valeurs implicites, détecter les conflits, reculer avec des clauses apprises ou des heuristiques, et terminer lorsqu'une assignation satisfaisante complète est trouvée ou que l'insatisfiabilité est prouvée.

Démonstration

Pour des clauses en FNC (x ∨ y), (¬x ∨ z), (¬y ∨ ¬z), un solveur SAT basé sur CDCL peut fixer x=true, propager y=true, obtenir un conflit avec (¬y ∨ ¬z), analyser le conflit pour apprendre la clause (¬x ∨ ¬z), reculer, puis trouver une assignation complète comme x=false, y=true, z=false qui satisfait toutes les clauses.

Mauvaise application

Considérer la résolution de satisfiabilité comme une routine d'optimisation qui renverrait nécessairement le « meilleur » modèle ou supposer qu'un solveur SAT énumère par défaut toutes les solutions satisfaisantes ; ou appliquer directement des méthodes propositionnelles à des formules du premier ordre sans mise à la terre ni gestion de théories.

Conséquence

Une application correcte fournit un certificat : soit une assignation satisfaisante concrète (modèle) démontrant la satisfiabilité, soit une preuve d'insatisfiabilité (par exemple la clause vide dérivée), permettant la vérification automatisée, la génération de contre-exemples et les réductions de nombreux problèmes NP vers SAT.

Inversion

À la place de rechercher une assignation satisfaisante, la tâche inverse consiste à extraire un noyau insatisfiable ou à énumérer des modèles ; conceptuellement, on peut inverser la procédure pour énumérer des sous-ensembles insatisfiables minimaux plutôt que des modèles.

Limite

Le champ couvre les formules propositionnelles/booléennes (combinaisons booléennes finies). Il exclut, sauf extension explicite, la logique du premier ordre avec symboles de fonction et domaines infinis, ainsi que le SMT qui intègre des théories de base comme l'arithmétique.

Tension sémantique

Tension entre le SAT pur et le SMT : les deux décident de la satisfiabilité mais SMT combine raisonnement théorique et techniques SAT, donc méthodes et garanties diffèrent ; tension aussi entre décision (existe-t-il un modèle ?) et recherche/optimisation (trouver le meilleur modèle selon un coût).

Synthèse

La résolution de satisfiabilité rassemble recherche, propagation, analyse de conflits et heuristiques pour résoudre le problème de décision pour les formules booléennes : elle produit soit une assignation concrète rendant la formule vraie, soit une preuve d'insatisfiabilité utile en vérification et synthèse.