Un million de clauses, ou soixante et une

La résolution n’a qu’une règle d’inférence et exige son entrée en forme normale conjonctive : une conjonction de disjonctions de littéraux. Toute formule propositionnelle admet un équivalent en FNC, ce que l’on énonce d’ordinaire comme si l’affaire était réglée.

Voici une formule qui sépare « il en existe un » de « vous pouvez vous le permettre ».

$$\varphi \;=\; (x_1 \wedge y_1) \vee (x_2 \wedge y_2) \vee \dots \vee (x_{20} \wedge y_{20}).$$

Vingt conjonctions, quarante variables, une ligne.

A. Par distribution

La conversion classique distribue $\vee$ sur $\wedge$. Chacun des vingt disjoints fournit soit son $x$, soit son $y$ à chaque clause, indépendamment : le résultat compte donc une clause par choix,

$$2^{20} = 1{,}048{,}576 \text{ clauses},$$

chacune longue de vingt littéraux, soit 20 971 520 littéraux au total. Pour trente disjoints, cela fait 1 073 741 824 clauses. La conversion est correcte, elle termine, et elle est inutilisable.

B. En nommant les sous-formules

L’alternative consiste à donner un nom à chaque conjonction. Introduisez $t_i$ et affirmez $t_i \leftrightarrow (x_i \wedge y_i)$, ce qui fait trois clauses :

$$(\neg t_i \vee x_i), \qquad (\neg t_i \vee y_i), \qquad (t_i \vee \neg x_i \vee \neg y_i),$$

puis dites qu’au moins l’une d’elles est vraie : $(t_1 \vee \dots \vee t_{20})$.

Cela fait $3 \times 20 + 1 = \mathbf{61}$ clauses et 160 littéraux, contre 20 971 520. Un facteur 131 072 sur les littéraux, obtenu par une règle de réécriture et non par un meilleur solveur. C’est la transformation de Tseitin, et c’est ce que fait l’entrée de tout solveur SAT.

C. Ce que cela coûte

Le résumé habituel est que le résultat est équisatisfiable plutôt qu’équivalent, ce qui sonne comme une concession. Il vaut la peine de préciser à quel point elle est mince.

La nouvelle formule a vingt variables de plus : elle porte donc sur un autre vocabulaire et ne peut être équivalente à $\varphi$ au sens strict. Mais chaque $t_i$ est contraint : les trois clauses le fixent à la valeur de vérité de $x_i \wedge y_i$, sans aucune liberté restante. Tout modèle de $\varphi$ se prolonge donc en exactement un modèle du codage, et le comptage le confirme :

Vérifié en énumérant toutes les affectations, $2^{2n}$ pour $\varphi$ et $2^{3n}$ pour le codage. La satisfiabilité est préservée, les solutions le sont, et le nombre de modèles aussi. Ce qui ne l’est pas, c’est la liste des variables, et le prix à payer est une projection à la fin.

D. La règle elle-même

La résolution prend deux clauses contenant une paire complémentaire et produit leur résolvante :

$$\frac{(\alpha \vee \ell) \qquad (\beta \vee \neg \ell)}{(\alpha \vee \beta)}.$$

Elle n’est pas complète pour dériver des conséquences quelconques - de $P$ elle ne dérivera jamais $P \vee Q$, qui est pourtant impliqué - mais elle est complète pour la réfutation : si un ensemble de clauses est insatisfiable, la résolution répétée dérive la clause vide. Cela suffit, car $\text{KB} \models \alpha$ exactement lorsque $\text{KB} \wedge \neg\alpha$ est insatisfiable.

Sur les clauses $\{P \vee Q,\; \neg P \vee R,\; \neg Q \vee R,\; \neg R\}$, il existe une réfutation en quatre étapes :

1. $\neg R$ avec $\neg P \vee R$ donne $\neg P$
2. $\neg R$ avec $\neg Q \vee R$ donne $\neg Q$
3. $P \vee Q$ avec $\neg P$ donne $Q$
4. $Q$ avec $\neg Q$ donne la clause vide.

Saturer aveuglément - résoudre toutes les paires jusqu’à ce que rien de nouveau n’apparaisse - dérive 8 clauses nouvelles et atteint une clôture de 12 avant d’y parvenir. Sur quatre clauses, la différence est nulle. C’est la même différence qui sépare un solveur moderne piloté par les conflits de l’algorithme tel qu’il est écrit dans un manuel, et à grande échelle elle est tout.

La figure applique la même règle à une autre base de connaissances, la règle de la brise du monde du Wumpus, $B_{1,1} \Leftrightarrow (P_{1,2} \vee P_{2,1})$ avec $\neg B_{1,1}$ : quatre clauses plus la requête niée, et chaque réponse est vérifiée sur les huit mondes possibles.

E. Ce qu’il faut en retenir

• La traduction fait partie de l’algorithme. Un problème impossible après distribution et routinier après Tseitin n’a jamais été un problème difficile ; il était mal codé.
• Comptez les littéraux, pas les clauses. La forme distribuée ci-dessus est mauvaise dans les deux, mais des codages comparables en nombre de clauses diffèrent souvent d’un ordre de grandeur en littéraux, or c’est cela que la propagation parcourt.
• « Il existe un équivalent en FNC » est un énoncé d’existence. « Tout problème de NP se réduit à SAT » aussi. Les deux sont vrais, et aucun ne dit quoi que ce soit sur la taille de ce que l’on obtient.