Satisfaction - Satisfiability

En logique mathématique , comprenant notamment la logique du premier ordre et le calcul propositionnel , la satisfiabilité et la validité sont des concepts élémentaires de la sémantique . Une formule est satisfiable s'il existe une interprétation ( modèle ) qui rend la formule vraie. Une formule est valide si toutes les interprétations rendent la formule vraie. Les opposés de ces concepts sont l' insatisfiabilité et l' invalidité , c'est-à-dire qu'une formule est insatisfiable si aucune des interprétations ne rend la formule vraie, et invalide si une telle interprétation rend la formule fausse. Ces quatre concepts sont liés les uns aux autres d'une manière exactement analogue à Aristote de la place de l' opposition .

Les quatre concepts peuvent être élevés pour s'appliquer à des théories entières : une théorie est satisfiable (valide) si une (toutes) des interprétations rend chacun des axiomes de la théorie vrai, et une théorie est insatisfiable (invalide) si tous (une) des interprétations rend faux l'un des axiomes de la théorie.

Il est également possible de ne considérer que les interprétations qui rendent vrais tous les axiomes d'une seconde théorie. Cette généralisation est communément appelée théories de satisfiabilité modulo .

La question de savoir si une phrase en logique propositionnelle est satisfiable est un problème décidable ( problème de satisfiabilité booléenne ). En général, la question de savoir si une phrase de logique du premier ordre est satisfiable n'est pas décidable. En algèbre universelle et en théorie équationnelle , les méthodes de réécriture de termes , de fermeture de congruence et d' unification sont utilisées pour tenter de décider de la satisfiabilité. Qu'une théorie particulière soit décidable ou non dépend si la théorie est sans variable ou sous d'autres conditions.

Réduction de la validité à la satisfiabilité

Pour les logiques classiques avec négation, il est généralement possible de réexprimer la question de la validité d'une formule à celle impliquant la satisfiabilité, en raison des relations entre les concepts exprimés dans le carré d'opposition ci-dessus. En particulier φ est valide si et seulement si ¬φ est insatisfiable, c'est-à-dire qu'il est faux que ¬φ soit satisfiable. En d'autres termes, φ est satisfiable si et seulement si ¬φ est invalide.

Pour les logiques sans négation, comme le calcul propositionnel positif , les questions de validité et de satisfiabilité peuvent être sans rapport. Dans le cas du calcul propositionnel positif , le problème de satisfiabilité est trivial, car toute formule est satisfiable, tandis que le problème de validité est co-NP complet .

satisfiabilité propositionnelle pour la logique classique

Dans le cas de la logique propositionnelle classique , la satisfiabilité est décidable pour les formules propositionnelles. En particulier, la satisfiabilité est un problème NP-complet et l'un des problèmes les plus étudiés en théorie de la complexité computationnelle .

Satisfiabilité en logique du premier ordre

Pour la logique du premier ordre (FOL), la satisfiabilité est indécidable . Plus précisément, il s'agit d'un problème co-RE-complet et donc non semi-décidable . Ce fait est lié à l'indécidabilité du problème de validité pour FOL. La question du statut du problème de validité a été posée en premier lieu par David Hilbert , comme le soi-disant Entscheidungsproblem . La validité universelle d'une formule est un problème semi-décidable par le théorème de complétude de Gödel . Si la satisfiabilité était aussi un problème semi-décidable, alors le problème de l'existence de contre-modèles le serait aussi (une formule a des contre-modèles si sa négation est satisfiable). Ainsi, le problème de la validité logique serait décidable, ce qui contredit le théorème de Church-Turing , un résultat indiquant la réponse négative pour le problème Entscheidungs.

Satisfiabilité en théorie des modèles

Dans la théorie des modèles , une formule atomique est satisfiable s'il existe un ensemble d'éléments d'une structure qui rendent la formule vraie. Si A est une structure, est une formule et a est une collection d'éléments, tirés de la structure, qui satisfont φ, alors il est communément écrit que

A φ [a]

Si φ n'a pas de variables libres, c'est-à-dire si est une phrase atomique , et qu'elle est satisfaite par A , alors on écrit

Un φ

Dans ce cas, on peut aussi dire que A est un modèle pour φ, ou que φ est vrai dans A . Si T est une collection de phrases atomiques (une théorie) satisfaite par A , on écrit

A ⊧ T

satisfiabilité finie

Un problème lié à la satisfiabilité est celui de la satisfiabilité finie , qui est la question de déterminer si une formule admet un modèle fini qui la rend vraie. Pour une logique qui a la propriété de modèle fini , les problèmes de satisfiabilité et de satisfiabilité finie coïncident, car une formule de cette logique a un modèle si et seulement si elle a un modèle fini. Cette question est importante dans le domaine mathématique de la théorie des modèles finis .

La satisfiabilité finie et la satisfiabilité n'ont pas besoin de coïncider en général. Par exemple, considérons la formule logique du premier ordre obtenue comme la conjonction des phrases suivantes, où et sont des constantes : ${\style d'affichage a}$ ${\style d'affichage b}$

${\style d'affichage R(a_{0},a_{0})}$
${\style d'affichage R(a_{0},a_{1})}$
$\forall xy(R(x,y)\rightarrow \exists zR(y,z))$
$\forall xyz(R(y,x)\wedge R(z,x)\rightarrow x=z))$

La formule résultante a le modèle infini , mais on peut montrer qu'elle n'a pas de modèle fini (en partant du fait et en suivant la chaîne d' atomes qui doit exister par le troisième axiome, la finitude d'un modèle nécessiterait l'existence d'une boucle , ce qui violerait le quatrième axiome, qu'il reboucle sur ou sur un élément différent). $R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ ${\style d'affichage R(a,b)}$ ${\style d'affichage R}$ ${\style d'affichage a_{0}}$

La complexité de calcul de la décision de satisfiabilité pour une formule d'entrée dans une logique donnée peut différer de celle de la décision de satisfiabilité finie ; en fait, pour certaines logiques, une seule d'entre elles est décidable .

Pour la logique classique du premier ordre , la satisfiabilité finie est récursivement énumérable (en classe RE ) et indécidable par le théorème de Trakhtenbrot appliqué à la négation de la formule.

Contraintes numériques

Les contraintes numériques apparaissent souvent dans le domaine de l'optimisation mathématique , où l'on veut généralement maximiser (ou minimiser) une fonction objectif soumise à certaines contraintes. Cependant, en laissant de côté la fonction objectif, la question fondamentale de simplement décider si les contraintes sont satisfiables peut être difficile ou indécidable dans certains contextes. Le tableau suivant résume les principaux cas.

Contraintes	sur les réels	sur des entiers
Linéaire	PTIME (voir programmation linéaire )	NP-complet (voir programmation en nombres entiers )
Polynôme	décidable par exemple par décomposition algébrique cylindrique	indécidable ( le dixième problème de Hilbert )

Source du tableau : Bockmayr et Weispfenning .

Pour les contraintes linéaires, une image plus complète est fournie par le tableau suivant.

Plus de contraintes :	rationnels	entiers	nombres naturels
Équations linéaires	PTIME	PTIME	NP-complet
Inégalités linéaires	PTIME	NP-complet	NP-complet

Source du tableau : Bockmayr et Weispfenning .

Voir également

Remarques

Les références

Boolos et Jeffrey, 1974. Calculabilité et logique . La presse de l'Universite de Cambridge.

Lectures complémentaires

Daniel Kroening ; Ofer Strichman (2008). Procédures de décision : un point de vue algorithmique . Springer Science & Business Media. ISBN 978-3-540-74104-6.
A. Bière ; M. Heule ; H. van Maaren ; T. Walsh, éd. (2009). Manuel de satisfaction . Presse IOS. ISBN 978-1-60750-376-7.

Languages

In other projects