|
|
| (15 versions intermédiaires par 2 utilisateurs non affichées) |
| Ligne 1 : |
Ligne 1 : |
|
| |
| == Domaine ==
| |
| [[Category:Vocabulary]]
| |
|
| |
| == Définition == | | == Définition == |
| | En informatique théorique, problème de décision, qui, étant donné une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie. |
|
| |
|
| | == Français == |
| | '''problème SAT''' |
|
| |
|
|
| | '''problème de satisfaisabilité booléenne''' |
| | |
| == Termes privilégiés ==
| |
|
| |
|
|
| |
|
| |
|
| |
|
| |
| == Anglais == | | == Anglais == |
| | '''Boolean satisfiability problem''' |
|
| |
|
| === Boolean satisfiability problem ===
| | '''SAT''' |
| In computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated as SATISFIABILITY or SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.
| |
|
| |
|
| SAT is the first problem that was proven to be NP-complete; see Cook–Levin theorem. This means that all problems in the complexity class NP, which includes a wide range of natural decision and optimization problems, are at most as difficult to solve as SAT. There is no known algorithm that efficiently solves each SAT problem, and it is generally believed that no such algorithm exists; yet this belief has not been proven mathematically, and resolving the question whether SAT has a polynomial-time algorithm is equivalent to the P versus NP problem, which is a famous open problem in the theory of computing.
| | ==Sources== |
| | [https://fr.wikipedia.org/wiki/Probl%C3%A8me_SAT Source : Wikipédia ] |
|
| |
|
| Nevertheless, as of 2007, heuristical SAT-algorithms are able to solve problem instances involving tens of thousands of variables and formulas consisting of millions of symbols,[1] which is sufficient for many practical SAT problems from e.g. artificial intelligence, circuit design, and automatic theorem proving.
| |
|
| |
|
| <br/>
| | [[Catégorie:GRAND LEXIQUE FRANÇAIS]] |
| <br/>
| |
| <br/>
| |
| <br/>
| |
| <br/>
| |
| <br/>
| |
| <br/>
| |
Dernière version du 28 janvier 2024 à 11:38
Définition
En informatique théorique, problème de décision, qui, étant donné une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie.
Français
problème SAT
problème de satisfaisabilité booléenne
Anglais
Boolean satisfiability problem
SAT
Sources
Source : Wikipédia
