Problème 2-SATEn informatique théorique, le problème 2-SAT est un problème de décision. C'est une restriction du problème SAT qui peut être résolu en temps polynomial, alors que le problème général est NP complet. Le problème 2-SAT consiste à décider si une formule booléenne en forme normale conjonctive, dont toutes les clauses sont de taille 2, est satisfaisable. De telles formules sont appelées 2-CNF ou formules de Krom. On considère des formules en forme normale conjonctive, c'est-à-dire que ce sont des ET de OU de littéraux (un littéral est une variable ou la négation d'une variable).
Recherche exhaustiveLa recherche exhaustive ou recherche par force brute est une méthode algorithmique qui consiste principalement à essayer toutes les solutions possibles. Par exemple pour trouver le maximum d'un certain ensemble de valeurs, on consulte toutes les valeurs. En cryptanalyse on parle d'attaque par force brute, ou par recherche exhaustive pour les attaques utilisant cette méthode. Le principe de cet algorithme est d'essayer toutes les possibilités dans un intervalle. Un exemple courant est l'attaque par force brute des mots de passe.
Retour sur trace non chronologiqueDans les algorithmes de recherche et de retour sur trace, le retour sur trace non chronologique ou backjumping est une technique qui réduit l'espace de recherche, et permet donc d'augmenter l'efficacité. En retour sur trace habituel, un retour en arrière remonte d'un niveau dans l'arbre de recherche lorsque toutes les valeurs d'une variable ont été testées. Le retour non chronologique permet de remonter de plusieurs niveaux grâce à une analyse des raisons qui conduisent une combinaison de valeurs pour des variables à échouer.
KakuroLe kakuro (en japonais : カックロ, kakkuro, abréviation de 加算クロス kasan-cross, « addition en croix ») est un jeu logique que l'on perçoit souvent comme une adaptation numérique des mots croisés. Au Japon, ce jeu est connu sous le nom de Kakkuro et sa popularité est immense. En Grande-Bretagne, The Guardian a commencé à publier ce jeu en . Depuis, beaucoup d'autres journaux britanniques ont suivi et publient quotidiennement une grille.
Constraint logic programmingConstraint logic programming is a form of constraint programming, in which logic programming is extended to include concepts from constraint satisfaction. A constraint logic program is a logic program that contains constraints in the body of clauses. An example of a clause including a constraint is . In this clause, is a constraint; A(X,Y), B(X), and C(Y) are literals as in regular logic programming. This clause states one condition under which the statement A(X,Y) holds: X+Y is greater than zero and both B(X) and C(Y) are true.
Problème SATvignette|Une instance du Sudoku peut être transformée en une formule de logique propositionnelle à satisfaire. Une assignation des variables propositionnelles donne une grille complétée. En informatique théorique, le problème SAT ou problème de satisfaisabilité booléenne est le 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. Ce problème est important en théorie de la complexité.
