Problème de satisfiabilité booléenne - Boolean satisfiability problem

En logique et en informatique , le problème de satisfiabilité booléenne (parfois appelé problème de satisfiabilité propositionnelle et en abrégé SATISFABILITÉ , SAT ou B-SAT ) est le problème de déterminer s'il existe une interprétation qui satisfait une formule booléenne donnée . En d'autres termes, il demande si les variables d'une formule booléenne donnée peuvent être systématiquement remplacées par les valeurs TRUE ou FALSE de telle sorte que la formule soit évaluée à TRUE . Si tel est le cas, la formule est dite satisfiable . D'autre part, si une telle affectation n'existe pas, la fonction exprimée par la formule est FAUX pour toutes les affectations de variables possibles et la formule est insatisfiable . Par exemple, la formule " a AND NOT b " est satisfaisable car on peut trouver les valeurs a  = TRUE et b  = FALSE, ce qui fait ( a AND NOT b ) = TRUE. En revanche, " a AND NOT a " est insatisfiable.

SAT est le premier problème qui s'est avéré NP-complet ; voir le théorème de Cook-Levin . Cela signifie que tous les problèmes de la classe de complexité NP , qui comprend un large éventail de problèmes de décision naturelle et d'optimisation, sont au plus aussi difficiles à résoudre que SAT. Il n'y a pas d'algorithme connu qui résout efficacement chaque problème SAT, et il est généralement admis qu'un tel algorithme n'existe pas ; pourtant cette croyance n'a pas été prouvée mathématiquement, et résoudre la question de savoir si SAT a un algorithme en temps polynomial est équivalent au problème P versus NP , qui est un problème ouvert célèbre dans la théorie de l'informatique.

Néanmoins, à partir de 2007, les algorithmes SAT heuristiques sont capables de résoudre des instances de problèmes impliquant des dizaines de milliers de variables et de formules composées de millions de symboles, ce qui est suffisant pour de nombreux problèmes SAT pratiques provenant, par exemple, de l'intelligence artificielle , de la conception de circuits et de l' automatique. démonstration du théorème .

Définitions de base et terminologie

Une formule logique propositionnelle , également appelée expression booléenne , est construite à partir de variables , d'opérateurs ET ( conjonction , également désignée par ∧), OU ( disjonction , ∨), NON ( négation , ¬) et de parenthèses. Une formule est dite satisfiable si elle peut être rendue VRAI en attribuant des valeurs logiques appropriées (c'est-à-dire VRAI, FAUX) à ses variables. Le problème de satisfiabilité booléenne (SAT) est, étant donné une formule, de vérifier s'il est satisfiable. Ce problème de décision est d'une importance centrale dans de nombreux domaines de l' informatique , notamment l'informatique théorique , la théorie de la complexité , l' algorithmique , la cryptographie et l' intelligence artificielle .

Il existe plusieurs cas particuliers du problème de satisfiabilité booléenne dans lesquels les formules doivent avoir une structure particulière. Un littéral est soit une variable, appelée littéral positif , soit la négation d'une variable, appelée littéral négatif . Une clause est une disjonction de littéraux (ou un seul littéral). Une clause est appelée clause Horn si elle contient au plus un littéral positif. Une formule est en forme normale conjonctive (CNF) si elle est une conjonction de clauses (ou une seule clause). Par exemple, x ₁ est un littéral positif, ¬ x ₂ est un littéral négatif, x ₁ ¬ x ₂ est une clause. La formule ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ est sous forme normale conjonctive; ses première et troisième clauses sont des clauses de Horn, mais sa deuxième clause ne l'est pas. La formule est satisfiable, en choisissant x ₁  = FAUX, x ₂  = FAUX, et x ₃ arbitrairement, puisque (FAUX ¬FAUX) ∧ (¬FAUX ∨ FAUX ∨ x ₃ ) ∧ ¬FAUX est évalué à (FAUX ∨ VRAI) ∧ (VRAI ∨ FAUX x ₃ ) VRAI, et à son tour à VRAI VRAI VRAI (c'est-à-dire à VRAI). En revanche, la formule CNF a ∧ ¬ a , constituée de deux clauses d'un littéral, est insatisfaisable, car pour a =VRAI ou a =FAUX elle est évaluée à VRAI ∧ ¬VRAI (c'est-à-dire FAUX) ou FAUX ∧ FAUX (c'est-à-dire , à nouveau FALSE), respectivement.

Pour certaines versions du problème SAT, il est utile de définir la notion de formule de forme normale conjonctive généralisée , à savoir. comme une conjonction de clauses généralisées arbitrairement nombreuses , ces dernières étant de la forme R ( l ₁ ,..., l _n ) pour une fonction booléenne R et des littéraux (ordinaires) l _i . Différents ensembles de fonctions booléennes autorisées conduisent à différentes versions de problèmes. Par exemple, R (¬ x , a , b ) est une clause généralisée, et R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d ,¬ z ) est une clause généralisée forme normale conjonctive. Cette formule est utilisée ci - dessous , avec R étant l'opérateur ternaire qui est VRAI juste au moment où exactement l'un de ses arguments l'est.

En utilisant les lois de l'algèbre de Boole , chaque formule logique propositionnelle peut être transformée en une forme normale conjonctive équivalente, qui peut cependant être exponentiellement plus longue. Par exemple, transformer la formule ( x ₁ ∧ y ₁ ) ∨ ( x ₂ ∧ y ₂ ) ∨ ... ∨ ( x _n ∧ y _n ) en forme normale conjonctive donne

( x ₁  ∨  x ₂  ∨ … ∨  x _n ) ∧

( Y ₁  ∨  x ₂  ∨ ... ∨  x _n ) ∧

( x ₁  ∨  y ₂  ∨ … ∨  x _n ) ∧

( y ₁  ∨  y ₂  ∨ … ∨  x _n ) ∧ ... ∧

( x ₁  ∨  x ₂  ∨ … ∨  y _n ) ∧

( y ₁  ∨  x ₂  ∨ … ∨  y _n ) ∧

( x ₁  ∨  y ₂  ∨ … ∨  y _n ) ∧

( y ₁  ∨  y ₂  ∨ … ∨  y _n ) ;

tandis que la première est une disjonction de n conjonctions de 2 variables, la seconde consiste en 2 ⁿ clauses de n variables.

Complexité et versions restreintes

Satisfaction illimitée (SAT)

SAT a été le premier problème NP-complet connu , comme l'a prouvé Stephen Cook à l' Université de Toronto en 1971 et indépendamment par Leonid Levin à la National Academy of Sciences en 1973. Jusqu'à cette époque, le concept d'un problème NP-complet n'avait pas existe même. La preuve montre comment chaque problème de décision dans la classe de complexité NP peut être réduit au problème SAT pour les formules CNF, parfois appelé CNFSAT . Une propriété utile de la réduction de Cook est qu'elle préserve le nombre de réponses acceptées. Par exemple, décider si un graphe donné a une 3-coloration est un autre problème dans NP ; si un graphique a 17 3-colorations valides, la formule SAT produite par la réduction de Cook-Levin aura 17 affectations satisfaisantes.

L'exhaustivité NP fait uniquement référence au temps d'exécution des pires instances. De nombreux cas qui se produisent dans les applications pratiques peuvent être résolus beaucoup plus rapidement. Voir Algorithmes pour résoudre SAT ci-dessous.

SAT est triviale si les formules sont restreintes à celles sous forme normale disjonctive , c'est-à-dire qu'elles sont une disjonction de conjonctions de littéraux. Une telle formule est en effet satisfiable si et seulement si au moins une de ses conjonctions est satisfiable, et une conjonction est satisfiable si et seulement si elle ne contient pas à la fois x et NON x pour une variable x . Ceci peut être vérifié en temps linéaire. De plus, si elles sont limitées à une forme normale disjonctive complète , dans laquelle chaque variable apparaît exactement une fois dans chaque conjonction, elles peuvent être vérifiées en temps constant (chaque conjonction représente une affectation satisfaisante). Mais cela peut prendre un temps et un espace exponentiels pour convertir un problème SAT général en forme normale disjonctive ; par exemple, échangez "∧" et "∨" dans l' exemple d'explosion exponentielle ci -dessus pour des formes normales conjonctives.

3-satisfiabilité

L'instance 3-SAT ( x ∨ x ∨ y ) ∧ (¬ x ∨ ¬ y ∨ ¬ y ) ∧ (¬ x ∨ y ∨ y ) réduite à un problème de clique . Les sommets verts forment une 3-clique et correspondent à l'affectation satisfaisante x = FAUX, y = VRAI.

Comme le problème de satisfiabilité pour des formules arbitraires, déterminer la satisfiabilité d'une formule sous forme normale conjonctive où chaque clause est limitée à au plus trois littéraux est également NP-complet ; ce problème est appelé 3-SAT , 3CNFSAT , ou 3-satisfiabilité . Pour réduire le problème SAT non restreint à 3-SAT, transformez chaque clause l ₁ ∨ ⋯ ∨ l _n en une conjonction de n - 2 clauses

( l ₁ ∨ l ₂ ∨ x ₂ ) ∧

(¬ x ₂ ∨ l ₃ ∨ x ₃ ) ∧

(¬ x ₃ ∨ l ₄ ∨ x ₄ ) ∧ ⋯ ∧

(¬ x _{n − 3} ∨ l _{n − 2} ∨ x _{n − 2} ) ∧

(¬ x _{n - 2} ∨ l _{n - 1} ∨ l _n )

où x ₂ , ,  x _{n − 2} sont de nouvelles variables n'apparaissant pas ailleurs. Bien que les deux formules ne soient pas logiquement équivalentes , elles sont équisatisfiables . La formule résultant de la transformation de toutes les clauses est au plus 3 fois plus longue que son origine, c'est-à-dire que la croissance en longueur est polynomiale.

3-SAT est l'un des 21 problèmes NP-complets de Karp , et il est utilisé comme point de départ pour prouver que d'autres problèmes sont également NP-difficiles . Cela se fait par réduction en temps polynomial de 3-SAT à l'autre problème. Un exemple de problème où cette méthode a été utilisée est le problème de clique : étant donné une formule CNF composée de c clauses, le graphe correspondant se compose d'un sommet pour chaque littéral, et d'une arête entre chaque deux littéraux non contradictoires de différentes clauses, cf. photo. Le graphe a une c -clique si et seulement si la formule est satisfiable.

Il existe un algorithme aléatoire simple dû à Schöning (1999) qui s'exécute dans le temps (4/3) ⁿ où n est le nombre de variables dans la proposition 3-SAT, et réussit avec une forte probabilité à décider correctement 3-SAT.

L' hypothèse du temps exponentiel affirme qu'aucun algorithme ne peut résoudre 3-SAT (ou même k -SAT pour tout ) en temps exp( o ( n )) (c'est-à-dire fondamentalement plus rapide que l'exponentielle en n ). ${\displaystyle k>2}$

Selman, Mitchell et Levesque (1996) donnent des données empiriques sur la difficulté des formules 3-SAT générées aléatoirement, en fonction de leurs paramètres de taille. La difficulté est mesurée en nombre d'appels récursifs effectués par un algorithme DPLL .

La 3-satisfiabilité peut être généralisée à la k-satisfiabilité ( k-SAT , aussi k-CNF-SAT ), lorsque les formules en CNF sont considérées avec chaque clause contenant jusqu'à k littéraux. Cependant, puisque pour tout k 3, ce problème ne peut être ni plus facile que 3-SAT ni plus difficile que SAT, et les deux derniers sont NP-complets, donc doit être k-SAT.

Certains auteurs restreignent k-SAT aux formules CNF avec exactement k littéraux . Cela ne conduit pas non plus à une classe de complexité différente, car chaque clause l ₁ ∨ ⋯ ∨ l _j avec j < k littéraux peut être complétée avec des variables muettes fixes à l ₁ ∨ ⋯ ∨ l _j ∨ d _{j +1} ∨ ⋯ ∨ d _k . Après avoir rempli toutes les clauses, 2 ^k -1 clauses supplémentaires doivent être ajoutées pour s'assurer que seule d ₁ = ⋯ = d _k = FALSE peut conduire à une affectation satisfaisante. Puisque k ne dépend pas de la longueur de la formule, les clauses supplémentaires entraînent une augmentation constante de la longueur. Pour la même raison, peu importe que les littéraux en double soient autorisés dans les clauses, comme dans ¬ x ∨ ¬ y ∨ ¬ y .

Exactement-1 3-satisfiabilité

À gauche : réduction de Schaefer d'une clause 3-SAT x ∨ y ∨ z . Le résultat de R est VRAI (1) si exactement un de ses arguments est VRAI, et FAUX (0) sinon. Les 8 combinaisons de valeurs pour x , y , z sont examinées, une par ligne. Les nouvelles variables a , ..., f peuvent être choisies pour satisfaire toutes les clauses (exactement un vert arguments pour chaque R ) dans toutes les lignes sauf la première, où x ∨ y ∨ z est FAUX. À droite : une réduction plus simple avec les mêmes propriétés.

Une variante du problème de satisfiabilité 3-est le 3-SAT un-en-trois (également connu sous le nom de 1-en-3-SAT et exactement-1 3-SAT ). Étant donné une forme normale conjonctive avec trois littéraux par clause, le problème est de déterminer s'il existe une affectation de vérité aux variables de sorte que chaque clause ait exactement un littéral VRAI (et donc exactement deux littéraux FAUX). En revanche, 3-SAT ordinaire exige que chaque clause ait au moins un littéral TRUE. Formellement, un problème 3-SAT un sur trois est donné sous une forme normale conjonctive généralisée avec toutes les clauses généralisées utilisant un opérateur ternaire R qui est VRAI juste si exactement l'un de ses arguments l'est. Lorsque tous les littéraux d'une formule 3-SAT un sur trois sont positifs, le problème de satisfiabilité est appelé 3-SAT positif un sur trois .

Un 3-SAT sur trois, avec son cas positif, est répertorié comme problème NP-complet "LO4" dans la référence standard, Computers and Intractability: A Guide to the Theory of NP-Completeness par Michael R. Garey et David S. Johnson . Un 3-SAT sur trois a été prouvé être NP-complet par Thomas Jerome Schaefer en tant que cas particulier du théorème de dichotomie de Schaefer , qui affirme que tout problème généralisant la satisfiabilité booléenne d'une certaine manière est soit dans la classe P soit NP- Achevée.

Schaefer donne une construction permettant une réduction facile du temps polynomial de 3-SAT à un sur trois 3-SAT. Soit "( x ou y ou z )" une clause dans une formule 3CNF. Ajoutez six nouvelles variables booléennes a , b , c , d , e et f , à utiliser pour simuler cette clause et aucune autre. Alors la formule R ( x , a , d ) R ( y , b , d ) ∧ R ( a , b , e ) ∧ R ( c , d , f ) ∧ R ( z , c ,FALSE) est satisfiable par un certain réglage des nouvelles variables si et seulement si au moins l'un des x , y ou z est VRAI, voir l'image (à gauche). Ainsi, toute instance 3-SAT avec m clauses et n variables peut être convertie en une instance 3-SAT équisatisfiable sur trois avec 5 m clauses et n +6 m variables. Une autre réduction ne fait intervenir que quatre nouvelles variables et trois clauses : R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R( c , d ,¬ z ), voir image (à droite).

3-satisfiabilité pas toutes égales

Une autre variante est le problème de 3-satisfiabilité pas tous égaux (également appelé NAE3SAT ). Étant donné une forme normale conjonctive avec trois littéraux par clause, le problème est de déterminer s'il existe une affectation aux variables telle que dans aucune clause les trois littéraux ont la même valeur de vérité. Ce problème est également NP-complet, même si aucun symbole de négation n'est admis, par le théorème de dichotomie de Schaefer.

SAT linéaire

Une formule 3-SAT est Linear SAT ( LSAT ) si chaque clause (considérée comme un ensemble de littéraux) coupe au plus une autre clause, et, de plus, si deux clauses se coupent, alors elles ont exactement un littéral en commun. Une formule LSAT peut être représentée comme un ensemble d'intervalles semi-fermés disjoints sur une ligne. Décider si une formule LSAT est satisfiable ou non est NP-complet.

2-satisfiabilité

SAT est plus facile si le nombre de littéraux dans une clause est limité à au plus 2, auquel cas le problème est appelé 2-SAT . Ce problème peut être résolu en temps polynomial, et est en fait complet pour la classe de complexité NL . Si en outre toutes les opérations OU en littéraux sont modifiées pour XOR opérations, le résultat est appelé exclusif ou 2-satisfiability , qui est un problème complet pour la classe de complexité SL = L .

Corne-satisfiabilité

Le problème consistant à décider de la satisfiabilité d'une conjonction donnée de clauses de Horn est appelé Horn-satisfiabilité , ou HORN-SAT . Il peut être résolu en temps polynomial par une seule étape de l' algorithme de propagation unitaire , qui produit le modèle minimal unique de l'ensemble des clauses de Horn (par rapport à l'ensemble des littéraux affectés à TRUE). Horn-satisfiability est P-complet . Il peut être vu comme la version de P du problème de satisfiabilité booléenne. De plus, décider de la vérité des formules de Horn quantifiées peut être fait en temps polynomial.

Les clauses Horn sont intéressantes car elles sont capables d'exprimer l' implication d'une variable à partir d'un ensemble d'autres variables. En effet, une telle clause ¬ x ₁ ∨ ... ∨ ¬ x _n ∨ y peut être réécrite comme x ₁ ∧ ... ∧ x _n → y , c'est-à-dire si x ₁ ,..., x _n sont tous VRAI , alors y doit également être VRAI.

Une généralisation de la classe des formules de Horn est celle des formules de Horn renommables, qui est l'ensemble des formules qui peuvent être placées sous forme de Horn en remplaçant certaines variables par leur négation respective. Par exemple, ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ n'est pas une formule de Horn, mais peut être renommée en la formule de Horn ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ ¬ y ₃ ) ∧ ¬ x ₁ en introduisant y ₃ comme négation de x ₃ . En revanche, aucun changement de nom de ( x ₁ ∨ ¬ x ₂ ∨ ¬ x ₃ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ conduit à une formule de Horn. La vérification de l'existence d'un tel remplacement peut se faire en temps linéaire ; par conséquent, la satisfiabilité de telles formules est dans P car elle peut être résolue en effectuant d'abord ce remplacement, puis en vérifiant la satisfiabilité de la formule de Horn résultante.

Une formule avec 2 clauses peut être insatisfaite (rouge), 3-satisfaite (vert), xor-3-satisfaite (bleu) ou/et 1-en-3-satisfaite (jaune), selon le nombre de VRAI-littéraux dans la 1ère (hor) et la 2ème (vert) clause.

XOR-satisfiabilité

Un autre cas particulier est la classe de problèmes où chaque clause contient des opérateurs OU exclusifs (c'est-à-dire exclusifs ou ) plutôt que (simples) OU. Ceci est en P , puisqu'une formule XOR-SAT peut aussi être vue comme un système d'équations linéaires mod 2, et peut être résolue en temps cubique par élimination gaussienne ; voir l'encadré pour un exemple. Cette refonte est basée sur la parenté entre les algèbres booléennes et les anneaux booléens , et le fait que l' arithmétique modulo deux forme un corps fini . Puisque a XOR b XOR c est évalué à VRAI si et seulement si exactement 1 ou 3 membres de { a , b , c } sont VRAI, chaque solution du problème 1-en-3-SAT pour une formule CNF donnée est aussi une solution du problème XOR-3-SAT, et à son tour chaque solution de XOR-3-SAT est une solution de 3-SAT, cf. photo. En conséquence, pour chaque formule CNF, il est possible de résoudre le problème XOR-3-SAT défini par la formule, et en se basant sur le résultat en déduire soit que le problème 3-SAT est résolvable soit que le problème 1-en-3- Le problème SAT est insoluble.

A condition que les classes de complexité P et NP ne soient pas égales , ni la 2-, ni Horn-, ni XOR-satisfiability n'est NP-complet, contrairement à SAT.

Le théorème de dichotomie de Schaefer

Les restrictions ci-dessus (CNF, 2CNF, 3CNF, Horn, XOR-SAT) liaient les formules considérées à des conjonctions de sous-formules ; chaque restriction énonce une forme spécifique pour toutes les sous-formules : par exemple, seules les clauses binaires peuvent être des sous-formules dans 2CNF.

Le théorème de dichotomie de Schaefer stipule que, pour toute restriction aux fonctions booléennes pouvant être utilisées pour former ces sous-formules, le problème de satisfiabilité correspondant est en P ou NP-complet. L'appartenance à P de la satisfiabilité des formules 2CNF, Horn et XOR-SAT sont des cas particuliers de ce théorème.

Le tableau suivant résume quelques variantes courantes de SAT.

Prolongations de SAT

Une extension qui a gagné en popularité depuis 2003 est les théories de satisfiabilité modulo ( SMT ) qui peuvent enrichir les formules CNF avec des contraintes linéaires, des tableaux, des contraintes toutes différentes, des fonctions non interprétées , etc. De telles extensions restent généralement NP-complètes, mais des solveurs très efficaces sont maintenant disponible qui peut gérer de nombreux types de contraintes.

Le problème de satisfiabilité devient plus difficile si les quantificateurs « pour tout » ( ∀ ) et « il existe » ( ∃ ) sont autorisés à lier les variables booléennes. Un exemple d'une telle expression serait ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z ) ; c'est valide, puisque pour toutes les valeurs de x et y , une valeur appropriée de z peut être trouvée, à savoir. z = VRAI si x et y sont tous les deux FAUX, et z = FAUX sinon. SAT lui-même (tacitement) n'utilise que des quantificateurs . Si seuls les quantificateurs ∀ sont autorisés à la place, le problème dit de tautologie est obtenu, qui est co-NP-complet . Si les deux quantificateurs sont autorisés, le problème est appelé problème de formule booléenne quantifiée ( QBF ), qui peut être montré comme étant PSPACE-complet . Il est largement admis que les problèmes PSPACE-complet sont strictement plus difficiles que n'importe quel problème dans NP, bien que cela n'ait pas encore été prouvé. En utilisant des systèmes P hautement parallèles , les problèmes QBF-SAT peuvent être résolus en temps linéaire.

Le SAT ordinaire demande s'il existe au moins une affectation de variable qui rend la formule vraie. Une variété de variantes traitent du nombre de ces affectations :

• MAJ-SAT demande si la majorité de toutes les affectations rendent la formule VRAIE. Il est connu pour être complet pour PP , une classe probabiliste.
• #SAT , le problème de comptage du nombre d'affectations de variables satisfaisant une formule, est un problème de comptage, pas un problème de décision, et est #P-complet .
• UNIQUE SAT est le problème de déterminer si une formule a exactement une affectation. Il est complet pour US , la classe de complexité décrivant les problèmes pouvant être résolus par une machine de Turing à temps polynomial non déterministe qui accepte lorsqu'il existe exactement un chemin d'acceptation non déterministe et rejette dans le cas contraire.
• UNAMBIGUOUS-SAT est le nom donné au problème de satisfiabilité lorsque l'entrée est restreinte à des formules ayant au plus une affectation satisfaisante. Le problème est aussi appelé USAT . Un algorithme de résolution pour UNAMBIGUOUS-SAT est autorisé à présenter n'importe quel comportement, y compris une boucle sans fin, sur une formule ayant plusieurs affectations satisfaisantes. Bien que ce problème semble plus facile, Valiant et Vazirani ont montré que s'il existe un algorithme pratique (c'est -à-dire en temps polynomial aléatoire ) pour le résoudre, alors tous les problèmes de NP peuvent être résolus tout aussi facilement.
• MAX-SAT , le problème de satisfiabilité maximale , est une généralisation FNP de SAT. Il demande le nombre maximum de clauses pouvant être satisfaites par toute cession. Il a des algorithmes d'approximation efficaces , mais il est NP-difficile à résoudre exactement. Pire encore, il est APX -complet, ce qui signifie qu'il n'y a pas de schéma d'approximation en temps polynomial (PTAS) pour ce problème à moins que P=NP.
• WMSAT est le problème de trouver une affectation de poids minimum qui satisfasse une formule booléenne monotone (c'est-à-dire une formule sans aucune négation). Les poids des variables propositionnelles sont donnés en entrée du problème. Le poids d'une affectation est la somme des poids des vraies variables. Ce problème est NP-complet (voir Th. 1 de ).

D' autres généralisations incluent la satisfiabilité pour la logique du premier et du second ordre , les problèmes de satisfaction de contraintes , la programmation en nombres entiers 0-1 .

Autoréduction

Le problème SAT est auto-réductible , c'est -à- dire que chaque algorithme qui répond correctement si une instance de SAT est résoluble peut être utilisé pour trouver une affectation satisfaisante. Premièrement, la question est posée sur la formule donnée Φ. Si la réponse est « non », la formule est insatisfaisable. Sinon, la question est posée sur la formule partiellement instanciée Φ { x ₁ =VRAI} , c'est-à-dire Φ avec la première variable x ₁ remplacée par VRAI, et simplifiée en conséquence. Si la réponse est "oui", alors x ₁ = VRAI, sinon x ₁ = FAUX. Les valeurs d'autres variables peuvent être trouvées ultérieurement de la même manière. Au total, n +1 exécutions de l'algorithme sont nécessaires, où n est le nombre de variables distinctes dans .

Cette propriété d'autoréductibilité est utilisée dans plusieurs théorèmes de la théorie de la complexité :

NP ⊆ P/poly ⇒ PH = Σ ₂   ( théorème de Karp–Lipton )

NP ⊆ BPP ⇒ NP = RP

P = NP ⇒ FP = FNP

Algorithmes pour résoudre SAT

Puisque le problème SAT est NP-complet, seuls les algorithmes avec une complexité exponentielle dans le pire des cas sont connus pour cela. Malgré cela, des algorithmes efficaces et évolutifs pour SAT ont été développés au cours des années 2000 et ont contribué à des avancées spectaculaires dans notre capacité à résoudre automatiquement des instances de problèmes impliquant des dizaines de milliers de variables et des millions de contraintes (c'est-à-dire des clauses). Des exemples de tels problèmes dans l' automatisation de la conception électronique (EDA) comprennent la vérification de l' équivalence formelle , vérification du modèle , la vérification formelle des microprocesseurs canalisées , génération de modèle de test automatique , routage des FPGA , la planification et les problèmes de planification , et ainsi de suite. Un moteur de résolution SAT est désormais considéré comme un composant essentiel de la boîte à outils EDA .

Un solveur DPLL SAT utilise une procédure de recherche de retour en arrière systématique pour explorer l'espace (de taille exponentielle) des affectations de variables à la recherche d'affectations satisfaisantes. La procédure de recherche de base a été proposée dans deux articles fondateurs au début des années 1960 (voir les références ci-dessous) et est maintenant communément appelée algorithme de Davis-Putnam-Logemann-Loveland (« DPLL » ou « DLL »). De nombreuses approches modernes de la résolution SAT pratique sont dérivées de l'algorithme DPLL et partagent la même structure. Souvent, ils n'améliorent que l'efficacité de certaines classes de problèmes SAT tels que les instances qui apparaissent dans les applications industrielles ou les instances générées aléatoirement. Théoriquement, des bornes inférieures exponentielles ont été prouvées pour la famille d'algorithmes DPLL.

Les algorithmes qui ne font pas partie de la famille DPLL incluent les algorithmes de recherche locale stochastique . Un exemple est WalkSAT . Les méthodes stochastiques tentent de trouver une interprétation satisfaisante mais ne peuvent pas en déduire qu'une instance SAT est insatisfiable, contrairement aux algorithmes complets, tels que DPLL.

En revanche, les algorithmes aléatoires tels que l'algorithme PPSZ de Paturi, Pudlak, Saks et Zane définissent les variables dans un ordre aléatoire selon certaines heuristiques, par exemple la résolution en largeur limitée . Si l'heuristique ne trouve pas le paramètre correct, la variable est affectée de manière aléatoire. L'algorithme PPSZ a une durée d' exécution de 3-SAT. C'était le runtime le plus connu pour ce problème jusqu'à une récente amélioration par Hansen, Kaplan, Zamir et Zwick qui a un runtime de 3-SAT et actuellement le runtime le plus connu pour k-SAT, pour toutes les valeurs de k. Dans le cadre de nombreuses affectations satisfaisantes, l'algorithme randomisé de Schöning a une meilleure borne. ${\style d'affichage O(1.308^{n})}$${\style d'affichage O(1.307^{n})}$

Les solveurs SAT modernes (développés dans les années 2000) se déclinent en deux versions : "conflict-driven" et "look-ahead". Les deux approches descendent de DPLL. Les solveurs axés sur les conflits, tels que l' apprentissage des clauses axées sur les conflits (CDCL), augmentent l'algorithme de recherche de base DPLL avec une analyse efficace des conflits, l'apprentissage des clauses, le retour en arrière non chronologique (alias backjumping ), ainsi que l' unité « deux-littéraux observés » propagation , branchement adaptatif et redémarrages aléatoires. Ces "extras" à la recherche systématique de base se sont avérés empiriquement essentiels pour gérer les grandes instances SAT qui surviennent dans l'automatisation de la conception électronique (EDA). Des implémentations bien connues incluent Chaff et GRASP . Les solveurs d'anticipation ont particulièrement renforcé les réductions (allant au-delà de la propagation des clauses unitaires) et les heuristiques, et ils sont généralement plus forts que les solveurs axés sur les conflits sur les instances difficiles (alors que les solveurs axés sur les conflits peuvent être bien meilleurs sur les grandes instances qui ont en fait un exemple facile à l'intérieur).

Les solveurs SAT modernes ont également un impact significatif sur les domaines de la vérification logicielle, de la résolution de contraintes en intelligence artificielle et de la recherche opérationnelle, entre autres. Des solveurs puissants sont facilement disponibles sous forme de logiciels libres et open source . En particulier, le MiniSAT axé sur les conflits , qui a connu un certain succès au concours SAT de 2005 , ne compte qu'environ 600 lignes de code. Un solveur Parallel SAT moderne est ManySAT. Il peut atteindre des accélérations super linéaires sur des classes importantes de problèmes. March_dl , qui a remporté un prix au concours SAT 2007 , est un exemple de solveurs d' anticipation .

Certains types de grandes instances aléatoires satisfiables de SAT peuvent être résolus par propagation d'enquête (SP). En particulier dans les applications de conception et de vérification de matériel , la satisfiabilité et d'autres propriétés logiques d'une formule propositionnelle donnée sont parfois décidées sur la base d'une représentation de la formule sous la forme d' un diagramme de décision binaire (BDD).

Presque tous les solveurs SAT incluent des délais d'attente, ils se termineront donc dans un délai raisonnable même s'ils ne trouvent pas de solution. Différents solveurs SAT trouveront différentes instances faciles ou difficiles, et certains excellent à prouver l'insatisfaction, et d'autres à trouver des solutions. Tous ces comportements peuvent être vus dans les concours de résolution SAT.

Résolution SAT parallèle

Les solveurs SAT parallèles se répartissent en trois catégories : les algorithmes de portefeuille, de division pour régner et de recherche locale parallèle . Avec des portefeuilles parallèles, plusieurs solveurs SAT différents s'exécutent simultanément. Chacun d'eux résout une copie de l'instance SAT, tandis que les algorithmes diviser pour régner divisent le problème entre les processeurs. Différentes approches existent pour paralléliser les algorithmes de recherche locale.

La compétition internationale de résolution de SAT a une piste parallèle reflétant les progrès récents dans la résolution de SAT parallèle. En 2016, 2017 et 2018, les benchmarks ont été exécutés sur un système à mémoire partagée avec 24 cœurs de traitement , par conséquent, les solveurs destinés à la mémoire distribuée ou aux processeurs à plusieurs cœurs pourraient avoir échoué .

Portefeuilles

En général, il n'y a pas de solveur SAT qui fonctionne mieux que tous les autres solveurs sur tous les problèmes SAT. Un algorithme peut bien fonctionner pour les instances problématiques avec lesquelles d'autres ont du mal, mais il fera moins bien avec d'autres instances. De plus, étant donné une instance SAT, il n'existe aucun moyen fiable de prédire quel algorithme résoudra cette instance particulièrement rapidement. Ces limites motivent l'approche de portefeuille parallèle. Un portefeuille est un ensemble d'algorithmes différents ou de configurations différentes d'un même algorithme. Tous les solveurs d'un portefeuille parallèle s'exécutent sur différents processeurs pour résoudre le même problème. Si un solveur se termine, le solveur de portefeuille signale que le problème est satisfiable ou insatisfiable selon ce solveur. Tous les autres solveurs sont terminés. Diversifier les portefeuilles en incluant une variété de solveurs, chacun performant sur un ensemble différent de problèmes, augmente la robustesse du solveur.

De nombreux solveurs utilisent en interne un générateur de nombres aléatoires . Diversifier leurs semences est un moyen simple de diversifier un portefeuille. D'autres stratégies de diversification consistent à activer, désactiver ou diversifier certaines heuristiques dans le solveur séquentiel.

Un inconvénient des portefeuilles parallèles est la quantité de travail en double. Si l'apprentissage des clauses est utilisé dans les solveurs séquentiels, le partage des clauses apprises entre les solveurs exécutés en parallèle peut réduire le travail en double et augmenter les performances. Pourtant, même le simple fait de gérer un portefeuille des meilleurs solveurs en parallèle en fait un solveur parallèle compétitif. Un exemple d'un tel solveur est PPfolio. Il a été conçu pour trouver une limite inférieure pour les performances qu'un solveur SAT parallèle devrait être en mesure de fournir. Malgré la grande quantité de travail en double en raison du manque d'optimisations, il a bien fonctionné sur une machine à mémoire partagée. HordeSat est un solveur de portefeuille parallèle pour les grands clusters de nœuds de calcul. Il utilise des instances configurées différemment du même solveur séquentiel en son cœur. Particulièrement pour les instances SAT dures, HordeSat peut produire des accélérations linéaires et donc réduire considérablement le temps d'exécution.

Ces dernières années, les solveurs SAT de portefeuille parallèle ont dominé la piste parallèle des compétitions internationales de solveurs SAT . Des exemples notables de ces solveurs incluent Plingeling et painless-mcomsps.

Diviser et conquérir

Contrairement aux portefeuilles parallèles, la division parallèle pour régner essaie de diviser l'espace de recherche entre les éléments de traitement. Les algorithmes de division et de conquête, tels que le DPLL séquentiel, appliquent déjà la technique de division de l'espace de recherche, leur extension vers un algorithme parallèle est donc simple. Cependant, en raison de techniques telles que la propagation unitaire, à la suite d'une division, les problèmes partiels peuvent différer considérablement en complexité. Ainsi, l'algorithme DPLL ne traite généralement pas chaque partie de l'espace de recherche dans le même laps de temps, ce qui pose un problème d' équilibrage de charge difficile .

Phase de cube pour la formule . L'heuristique de décision choisit les variables (cercles) à affecter. Une fois que l'heuristique de coupure a décidé d'arrêter le branchement, les problèmes partiels (rectangles) sont résolus indépendamment à l'aide de CDCL.${\style d'affichage F}$

En raison du retour en arrière non chronologique, la parallélisation de l'apprentissage des clauses axées sur les conflits est plus difficile. Une façon de surmonter cela est le paradigme Cube-and-Conquer . Il propose une résolution en deux phases. Dans la phase "cube", le problème est divisé en plusieurs milliers, voire millions, de sections. Ceci est fait par un solveur d'anticipation, qui trouve un ensemble de configurations partielles appelées "cubes". Un cube peut également être vu comme une conjonction d'un sous-ensemble de variables de la formule originale. En conjonction avec la formule, chacun des cubes forme une nouvelle formule. Ces formules peuvent être résolues indépendamment et simultanément par des solveurs axés sur les conflits. Comme la disjonction de ces formules est équivalente à la formule originale, le problème est déclaré satisfiable, si l'une des formules est satisfiable. Le solveur d'anticipation est favorable pour les problèmes petits mais difficiles, il est donc utilisé pour diviser progressivement le problème en plusieurs sous-problèmes. Ces sous-problèmes sont plus faciles mais toujours volumineux, ce qui est la forme idéale pour un solveur axé sur les conflits. De plus, les solveurs prospectifs considèrent l'ensemble du problème tandis que les solveurs axés sur les conflits prennent des décisions sur la base d'informations beaucoup plus locales. Il y a trois heuristiques impliquées dans la phase de cube. Les variables dans les cubes sont choisies par l'heuristique de décision. L'heuristique de direction décide quelle affectation de variable (vraie ou fausse) explorer en premier. Dans les instances de problèmes satisfiables, choisir d'abord une branche satisfiable est bénéfique. L'heuristique de coupure décide quand arrêter l'expansion d'un cube et le transmettre à la place à un solveur séquentiel basé sur les conflits. De préférence, les cubes sont également complexes à résoudre.

Le Treengeling est un exemple de solveur parallèle qui applique le paradigme Cube-and-Conquer. Depuis son introduction en 2012, il a remporté de nombreux succès au concours international de solveurs SAT . Cube-and-Conquer a été utilisé pour résoudre le problème des triplets booléens de Pythagore .

Recherche locale

Une stratégie vers un algorithme de recherche locale parallèle pour la résolution SAT consiste à essayer plusieurs retournements de variables simultanément sur différentes unités de traitement. Une autre consiste à appliquer l'approche de portefeuille susmentionnée, mais le partage de clauses n'est pas possible car les solveurs de recherche locaux ne produisent pas de clauses. Alternativement, il est possible de partager les configurations qui sont produites localement. Ces configurations peuvent être utilisées pour guider la production d'une nouvelle configuration initiale lorsqu'un solveur local décide de relancer sa recherche.

Voir également

• Noyau insatisfaisant
• Théories modulo de la satisfaction
• Compter SAT
• SAT planaire
• Algorithme de Karloff-Zwick
• satisfaisabilité des circuits

Remarques

Les références

Les références sont classées par date de publication :

Liens externes

• SAT Game - essayez de résoudre vous-même un problème de satisfiabilité booléenne

Format de problème SAT

Un problème SAT est souvent décrit au format DIMACS-CNF : un fichier d'entrée dans lequel chaque ligne représente une seule disjonction. Par exemple, un fichier avec les deux lignes

1 -5 4 0
-1 5 3 4 0

représente la formule "( x ₁ ∨ ¬ x ₅ ∨ x ₄ ) ∧ (¬ x ₁ ∨ x ₅ ∨ x ₃ ∨ x ₄ )".

Un autre format courant pour cette formule est la représentation ASCII 7 bits "(x1 | ~x5 | x4) & (~x1 | x5 | x3 | x4)".

• BCSAT est un outil qui convertit les fichiers d'entrée au format lisible par l'homme au format DIMACS-CNF.

Solveurs SAT en ligne

• BoolSAT – Résout les formules au format DIMACS-CNF ou dans un format plus convivial : « a et non b ou a ». Fonctionne sur un serveur.
• Logictools – Fournit différents solveurs en javascript pour l'apprentissage, la comparaison et le piratage. Fonctionne dans le navigateur.
• minisat-in-your-browser – Résout les formules au format DIMACS-CNF. Fonctionne dans le navigateur.
• SATRennesPA – Résout les formules écrites de manière conviviale. Fonctionne sur un serveur.
• somerby.net/mack/logic – Résout les formules écrites en logique symbolique. Fonctionne dans le navigateur.

Solveurs SAT hors ligne

• MiniSAT – Format DIMACS-CNF et format OPB pour son compagnon solveur de contraintes pseudo-booléennes MiniSat+
• Lingeling - a remporté une médaille d'or dans une compétition SAT 2011.
  • PicoSAT – un solveur antérieur du groupe Lingeling.
• Sat4j – Format DIMACS-CNF. Code source Java disponible.
• Glucose – Format DIMACS-CNF.
• RSat - a remporté une médaille d'or dans une compétition SAT 2007.
• UBCSAT . Prend en charge les clauses non pondérées et pondérées, toutes deux au format DIMACS-CNF. Code source C hébergé sur GitHub .
• CryptoMiniSat - a remporté une médaille d'or dans un concours SAT 2011. Code source C++ hébergé sur GitHub . Essaie de mettre de nombreuses fonctionnalités utiles du noyau MiniSat 2.0, PrecoSat ver 236 et Glucose dans un seul package, ajoutant de nombreuses nouvelles fonctionnalités
• Spear – Prend en charge l'arithmétique bit-vectorielle. Peut utiliser le format DIMACS-CNF ou le format Spear .
  • HyperSAT - Écrit pour expérimenter l'élagage de l'espace de recherche B-cubing. A remporté la 3e place dans une compétition SAT 2005. Un solveur plus ancien et plus lent des développeurs de Spear.
• BASsolver
• ArgoSAT
• Fast SAT Solver – basé sur des algorithmes génétiques .
• zChaff – n'est plus pris en charge.
• BCSAT - format de circuit booléen lisible par l'homme (convertit également ce format au format DIMACS-CNF et se lie automatiquement à MiniSAT ou zChaff).
• gini - Go language SAT solver avec des outils connexes.
• gophersat – Solveur SAT en langage Go qui peut également traiter les problèmes pseudo-booléens et MAXSAT.
• CLP(B) – Boolean Constraint Logic Programming, par exemple SWI-Prolog .

candidatures SAT

• WinSAT v2.04 : Une application SAT basée sur Windows spécialement conçue pour les chercheurs.

Conférences

• Conférence internationale sur la théorie et les applications des tests de satisfaction

Publications

• Journal on Satisfiability, Boolean Modelling and Computation
• Propagation de l'enquête

Repères

• Benchmarks SAT satisfaisants forcés
• Benchmarks de vérification de logiciel
• Fadi Aloul Benchmarks SAT

Résolution SAT en général :

• http://www.satlive.org
• http://www.satisfiabilité.org

Évaluation des solveurs SAT

• Évaluation annuelle des solveurs SAT
• Résultats de l'évaluation des solveurs SAT pour 2008
• Compétitions internationales SAT
• Histoire

Plus d'informations sur SAT :

• SAT et MAX-SAT pour le chercheur-profane
• SAT/SMT par exemple

Cet article comprend des éléments d'une chronique du bulletin électronique ACM SIGDA par le professeur Karem Sakallah
Le texte original est disponible ici