algorithme dédié à la résolution efficace des instances (cas) du problème SATle problème de satisfaction en logique* propositionnelle consiste à déterminer si une formule, exprimée en logique propositionnelle, est vraie ou fausse. Ce problème est très important en informatique, car il constitue la référence des problèmes difficiles à résoudre (ce qui est l’objet de la théorie... More*. La complexité(complexité algorithmique) théorie permettant de classer les différents problèmes de calcul selon le niveau de difficulté de leur résolution. Cette théorie est au cœur de l’informatique: en informatique, montrer l’existence d’une solution à un problème donné ne suffit pas, il faut pouvoir la construire en... More* théorique du problème SATle problème de satisfaction en logique* propositionnelle consiste à déterminer si une formule, exprimée en logique propositionnelle, est vraie ou fausse. Ce problème est très important en informatique, car il constitue la référence des problèmes difficiles à résoudre (ce qui est l’objet de la théorie... More fait que l’on sait que pour un certain nombre d’instances on ne pourra pas trouver de solution en un temps raisonnable. Le but des solveurs SATvoir Problème SAT * est de trouver une solution pour un maximum d’instances. Ce qui est généralement suffisant en pratique sur les problèmes réels.
De quoi s'agit-il vraiment ?