SAT

Définition du problème SAT

Le problème de satisfiabilité booléenne (SAT) est un problème fondamental en informatique théorique et en logique.
Il consiste à déterminer si une formule booléenne donnée peut être rendue vraie en attribuant des valeurs de vérité (vrai ou faux) à ses variables.

Formellement :

Instance : Une formule booléenne ( \phi ) en forme normale conjonctive (CNF), c’est-à-dire une conjonction de clauses, chaque clause étant une disjonction de littéraux.

Question : Existe-t-il une affectation des variables telle que ( \phi ) soit vraie ?

Une formule CNF s’écrit comme :

$$\varphi =C_1\wedge C_2\wedge \cdots \wedge C_m$$

où chaque clause ($C_i$) est une disjonction de littéraux :

$$C_i=(l_{i1}\vee l_{i2}\vee \cdots \vee l_{ik})$$

et chaque littéral ($l_{ij}$) est soit une variable ($x_j$), soit sa négation ($\neg x_j$).

Instance SAT

$$\varphi =(x_1\vee \neg x_2\vee x_3)\wedge (\neg x_1\vee x_2)\wedge (x_2\vee \neg x_3)$$

La question est : existe-t-il une affectation de ( x_1, x_2, x_3 \in {\text{vrai}, \text{faux}} ) qui rend ( \phi ) vraie ?

Self-réductibilité

SAT est self-réductible.

Algorithme avec oracle

SATdec(C) -> oui/non  // oracle O(1)

si !SATdec(C):
    retourner faux

v = []
pour i = 1 à n:
    si SATdec(C[xi=0]):
        C = C[xi=0]
        v[i] = 0
    sinon:
        C = C[xi=1]
        v[i] = 1
retourner v

Complexité : $O(n)$ appels à l’oracle.

Le cas particulier : le problème 3-SAT

Le 3-SAT est une version restreinte du problème SAT où chaque clause contient exactement trois littéraux.

Instance : Une formule booléenne en CNF où chaque clause a exactement 3 littéraux. Question : Existe-t-il une affectation des variables qui satisfait la formule ?

Exemple :

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

Remarques

• SAT est le premier problème prouvé NP-complet (théorème de Cook-Levin, 1971).
• 3-SAT est aussi NP-complet, même s’il est plus restreint, ce qui en fait un cas d’étude standard pour la complexité algorithmique et la conception de solveurs SAT.