le problème de satisfaction en logiquela logique, qui apparaît dans la Grèce Antique avec l’étude des syllogismes, s’intéresse à la formalisation du raisonnement. La lo- gique moderne, qui se développe à partir du XIXe siècle, a conduit à la formalisation d’un véritable calcul déductif à partir de formules logiques formées... More* propositionnelle consiste à déterminer si une formule, exprimée en logiquela logique, qui apparaît dans la Grèce Antique avec l’étude des syllogismes, s’intéresse à la formalisation du raisonnement. La lo- gique moderne, qui se développe à partir du XIXe siècle, a conduit à la formalisation d’un véritable calcul déductif à partir de formules logiques formées... More 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 de 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 algorithmique*). Il sert de référence pour résoudre / étudier des problèmes qui lui sont réductibles ou auxquels il est réductible, tels que la vérification de logiciels, de micro-processeurs, ou de systèmes complexes.
De quoi s'agit-il vraiment ?