SAT

Soit une expression booléenne à $n$ variables sous forme clausale (conjonction de disjonctions), par exemple,

$$(x_1\vee \neg x_3\vee x_2) \wedge (\neg x_2) \wedge (\neg x_1 \vee x_3) \wedge (x_3) \wedge (x_1 \vee x_2 \vee x_3 \vee x_4)$$

Les clauses (contenant des disjonctions) sont notées

$$\{C_1, c_2, \ldots, c_k\}$$

Toute clause est formée de $k_i$ littéraux

$$C_i = {l_1^i, l_2^i, \ldots, l_{k_i}^i}$$

chaque littéral $l$ est soit une variable ($l = x_j$), soit la négation d'une variable ($l = \not x_j$). Une affectation $\mathcal{A}$ des variables est une application de $\{x_1, \ldots, x_n\}$ dans $\{true, false\}$.

• Si $\mathcal{A}(x_j) = true$, alors $l$ est satisfait si $l = x_j$, non satisfait sinon
• si $\mathcal{A}(x_j) = false$, alors $l_j$ est satisfait si $l = \neg x_j$, non satisfait si $l = x_j$

Une clause est satisfaite si au moins un des littéraux qui la forment est satisfait. Une expression sous forme clausale est satisfaite si toutes les clauses sont satisfaites. Le problème est le suivant :

• données : $n$ variables, $k$ clauses de chacune $k_i$ littéraux, chacun correspondant à une variable ou à la négation d'une variable.
• question : trouver une affectation qui satisfasse toutes les clauses (donc au moins un littéral par clause)

Ce problème (de satisfaction de contraintes) est NP-Complet dans le cas général, et facile si les clauses contiennent au plus $2$ littéraux.. Remarquons que si la question avait été "existe-t-il une affectation qui satisfasse toutes les clauses ?'', ce problème serait un problème de décision.