CNF, SAT, encoding, cardinality constraints.
Parmi les solveurs modernes en programmation sous
contrainte les plus performants, on trouve aujourd’hui un
certain nombre de solveurs CNF-SAT. Les palmarès
récents du MiniZinc Challenge en témoignent [
De nombreux travaux se sont donc penchés sur la
question de savoir comment exprimer des contraintes classiques
des CSP sous forme CNF de manière performante pour les
solveurs CNF-SAT [
Parmi les travaux existants, on trouve des comparaisons
des différents encodages proposés [
Par ailleurs, on introduit dans cet article un nouvel encodage : l’encodage séquentiel bidirectionnel. Cet encodage, dont la définition est assez naturelle, est particulièrement adapté pour considérer des contraintes de cardinalité plus complexes, notamment les contraintes de cardinalité correspondant à un intervalle. On montre par ailleurs qu’il permet de considérer des contraintes de cardinalité de type 2 K(x1; :::; xn) où K J0; nK de manière performante ce qui représente une nouveauté.
1. Le terme contrainte de cardinalité est utilisé ici selon la nomenclature standard dans le contexte SAT et ne doit pas être confondu avec d’autres notions telles que celle de global cardinality constraint utilisée dans le contexte de la programmation sous contrainte.
Dans la suite, on considère des entiers n et k tels que n 2
et k 2 J1; n 1K, les autres cas étant évidemment triviaux.
La démarche qui mène à définir l’encodage proposé dans
cette section s’apparente à la démarche qui mène à
l’encodage séquentiel proposé par Carsten Sinz dans [
L’encodage CNF qui suit permet d’encoder exactement l’ensemble des équivalences (si j) () si;j pour tout i 2 J1; nK et pour tout j 2 J1; k + 1K. On appelle encodage séquentiel bidirectionnel cet encodage et on le note SeqB#nk.
(x1 _ :s1;1) (:xi _ si;1) 8i 2 J1; nK (:sj 1;j ) 8j 2K1; k + 1K (:si 1;j _ si;j ) (xi _ si 1;j _ :si;j ) (si 1;j 1 _ :si;j ) (:xi _ :si 1;j 1 _ si;j ) 9 8j 2 J1; k + 1K>>= 8j 2K1; k + 1K >>; 8i 2K1; nK (SeqB#nk) À partir de cet encodage, il est très facile d’obtenir la contrainte de cardinalité k(x1; :::; xn). En effet, il suffit de rajouter la clause :sn;k+1. De même, la contrainte k(x1; :::; xn) s’obtient simplement par le rajout de la clause sn;k. Enfin, la contrainte = k(x1; :::; xn) s’obtient par le rajout de ces deux clauses. On note SeqBnk, SeqBnk et SeqB=nk les encodages respectifs correspondants. 3 3.1
Comparaisons des encodages En plus des encodages décrits précédemment, on va également considérer l’encodage naïf (N nk) défini par : (N nk) ^ k+1 _ i2Cnk+1 j=1
:xij
où i = (i1; :::; ik+1) est une combinaison appartenant
à l’ensemble Cnk+1 des combinaisons de k + 1 éléments
de J1; nK. On rajoute l’encodage proposé par Bailleux &
Boufkhad dans [
D’autres encodages de la littérature [
Par ailleurs, par manque de temps, nous n’avons pas
intégré ici d’encodage à base de réseaux [
Le tableau 1 donne le nombres de clauses (avec le détail en
fonction de la taille en nombre de littéraux de ces clauses)
ainsi que le nombre de variables auxilaires pour chacun de
ces encodages. Les valeurs figurant dans ce tableau ont été
recalculées à partir des descriptions de ces encodages dans
les articles précités [
; 2 et k2 = 23 (nJk+21;k)1.J ;
; 8 et k 2
; 13 et k 2
; 30 et k 2
N nk J1; nJ 2. Les valeurs données ici sont exactes si n est une puissance de 2. On remarque d’abord que pour une telle contrainte, l’encodage SeqU nk est clairement toujours plus performant que l’encodage SeqBnk donc on peut exclure ce dernier de notre comparaison. Par contre, en utilisant (1), on peut considérer l’encodage SeqBnn k appliqué à (:x1; :::; :xn). On note SeqB:nn k cet encodage. On cherche donc à comparer les encodages N nk, SeqU nk, SeqB:nn k, BBn0; k. Une analyse complète des différents nombres totaux de clauses pour chacun de ces encodages permet de déterminer l’encodage offrant le plus petit nombre de clauses en fonction de n et k. On a réalisé cette analyse ici et regroupé les résultats dans le tableau 2. Ce tableau décrit, en fin de compte, une partition de l’ensemble des valeurs potentielles de n et k en 4 parties, chacune correspondant aux valeurs de n et k pour lesquelles l’encodage en colonne est optimal (pour le critère du nombre de clauses considéré ici).
SeqU nk
; J1; k1J où k1 = n J1; k1J où k1 = n J1; k2J où k1 = n J1; k2J où k1 = n
Conditions sur n et k par encodage
BBn0; k SeqB:nn k n
5 et k 2 3. 2. ; 8 ; n n
; 7 et k 2
; 10 et k 2
; 11 n 27 et k 2
; Jk2; k1J 2 et k2 = l 10n2 3n 3 m.
3(5n 6) 28 n 148 et k 2
; Jk2; k1J 1 et k2 = l 10n2 3n 3 m.
3(5n 6) n et k 2
N nk J1; nJ TABLE 3 – Encodage de k(x1; :::; xn) donnant le nombre total minimal de littéraux en fonction de n et k Le tableau 2 permet de choisir un encodage en fonction du nombre de clauses de cet encodage mais il ne prend pas en compte la taille de ces clauses (i.e. le nombre de littéraux par clause). Or la taille des clauses dans une contrainte CNF peut avoir une influence importante sur la rapidité d’un solveur SAT sur cette contrainte. Comme l’évaluation d’une valuation d’une contrainte CNF est linéaire par rapport à son nombre total de littéraux, on pourrait également considérer le nombre total de littéraux de chacun de encodages plutôt que leur nombre de clauses comme critère pour choisir un encodage. Même si le nombre total de clauses est généralement utilisé comme critère de comparaison des encodages dans l’état de l’art précité, on penche plutôt pour l’utilisation du nombre total de littéraux. En tout état de cause, on présentera systèmatiquement par la suite les valeurs obtenues pour chacun de ces deux critères. Le tableau 3 permet de déterminer l’encodage avec le plus petit nombre total de littéraux. Dans cette section, on compare 5 encodages pour la contrainte k(x1; :::; xn). Par l’équivalence (1), on ob37 n et k 2 oùJ1k;13J= l n2J32;nk2loJg2(n) Jnk+2;1km1J
2(n 1) et k2 = l n2+2n log2(n) 2n 2 m.
4(n 1) N:nn k tient bien la contrainte souhaitée en appliquant les encodages N nn k, SeqU nn k et SeqBnn k à (:x1; :::; :xn). On note respectivement N :nn k, SeqU :nn k et SeqB:nn k ces trois encodages. On considère par ailleurs les deux encodages SeqBnk et BBnk; n.
Comme précédemment, on détermine les encodages donnant le nombre total minimal de clauses (tableau 4) ainsi que les encodages donnant le nombre total minimal de littéraux (5) en fonction de n et k. On remarque que, dans ce cas, c’est l’encodage SeqB:nn k qui est écarté systématiquement.
Contrainte = k(x1; :::; xn) Dans cette section, on compare 7 encodages différents de = k(x1; :::; xn) parmi lesquels 2 sont des encodages mixtes entre deux encodages différents. Il s’agit des encodages : 1. BB=nk (i.e. BBnk; k) ; 2. SeqB=nk ; 3. SeqB=:nn k ; 4. SeqU=nk (i.e. SeqU nk et SeqU :nn k) ; 5. N=nk (i.e. N nk et N :nn k) ; 6. N S=nk (i.e. N nk et SeqU :nn k) ; 7. SN=nk (i.e. SeqU nk et N :nn k).
Comme dans les deux sections précédentes, on a determiné les encodages donnant le nombre total de clauses minimal en fonction de n et k ainsi que celui donnant le nombre total de littéraux minimal en fonction des mêmes paramètres. Chacun de ces résultats étant difficilement synthétisable en un seul tableau, on renvoie aux annexes pour le détail pour tous les entiers n 2 J6; 17K.
Encodage Pour n 5, c’est l’encodage naïf N=nk qui donne les plus petits nombres de clauses et de littéraux quel que soit k. Les deux tableaux 6 et 7 donnent les résultats pour n 18. On remarquera que les encodages SeqU=nk et N=nk en sont absents. Par ailleurs, on a indiqué, pour chaque encodage, la limite de la proportion à n donné de valeurs différentes de k pour laquelle cet encodage est optimal lorsque n tend vers l’infini. SN=nk k = 1 SeqB=nk 2 k < k2
BB=nk k2 k < k1 SeqB=:nn k k1 k < n 1
N S=nk k = n 1 où k1 = l 7n2 6n log2(n) 6n+1 m
10n 9 et k2 = l 3n2+6n log2(n) 3n 1 m.
10n 9 TABLE 7 – Encodage de = k(x1; :::; xn) donnant le nombre total minimal de littéraux en fonction de k pour n 18 3.5 On étudie ici le cas d’une contrainte donnant un intervalle. On compare 7 encodages de cette contrainte, correspondant aux cas généraux des encodages de = k(x1; :::; xn) de la section précédente. Il s’agit des encodages : 1. BBnk1; k2 ; 2. SeqBnk1; k2 ; 3. SeqB:nn k2; n k1 ; 4. SeqU nk1; k2 (i.e. SeqU nk2 et SeqU :nn k1 ) ; 5. N nk1; k2 (i.e. N nk2 et N :nn k1 ) ; 6. SN nk1; k2 (i.e. SeqU nk2 et N :nn k1 ) ; 7. N Snk1; k2 (i.e. N nk2 et SeqU :nn k1 ).
On ne fait pas ici une comparaison exhaustive de toutes les valeurs possibles de k et n comme on a pu le faire pour les contraintes précédentes car cela nous semble trop fastidieux et difficilement exposable de manière concise. On donne simplement les expressions des nombres totaux de clauses et nombres totaux de littéraux pour chacun de ces encodages. Ces expressions peuvent être évaluées au cas par cas pour déterminer une valeur minimale et choisir l’encodage associé lorsque n est faible.
N nk1; k2 SN nk1; k2 N Snk1; k2
Nombre total de clauses n2 + 2n log2(n) + 2n k2 + k1 4nk2 + 3n 3k2 + 1 4n2 4nk1 + 3k1 + 1 2n2 + 2n(k2 k1) n 3(k2
n n k1n 1 +k2 +2n1k2++kn1 1 k2n+1 + 2n2 2nk1
3k2 1 2n + 3k1 2 1 Sinon, en dehors de certains effets de bord quand k1 2 ou bien k2 n 2, on peut voir que, pour n suffisamment grand, ce sont les trois premiers encodages qui sont les plus performants. On peut alors utiliser le protocole sui
Nnk1; k2 SN nk1; k2 N Snk1; k2 (n Dans cette section, on considère un sous-ensemble K = fk1; :::; kmg J0; nK avec m 2 et k1 < k2 < ::: < km. Le cas général d’une contrainte d’appartenance du cardinal à un sous-ensemble K se distingue entièrement des cas précédents. En effet, la proposition k 2 K est équivalente m à la disjonction W [k = ki]. Ainsi, à part le cas particui=1 lier d’un intervalle traité précédemment, on ne peut pas se ramener directement à une conjonction des encodages CNF décrits précédemment. Or obtenir une contrainte CNF à partir d’une disjonction de contraintes CNF nécessite une opération supplémentaire. Effectuer cette opération est prohibitif si l’on considère directement des disjonctions des encodages précédents. Toutefois, on peut également considérer ces disjonctions au sein d’un encodage séquentiel bidirectionnel unique ce qui permet de rendre cette opération tout à fait envisageable.
En effet, la contrainte suivante est bien un encodage de la contrainte 2 K(x1; :::; xn).
SeqB#n ^
m
_ (sn;ki ^ :sn;ki+1)
i=1
!
(4)
Cette encodage n’est pas une contrainte CNF mais on peut
se ramener à une contrainte CNF équisatisfaisable
facilement en introduisant m variables supplémentaires y0,
..., ym 1 [
!! m 1 W yj j=i (SeqBn ) 2K !! (5) (6) Cette contrainte a un nombre total de clauses égal à : 4nkm + 3n
3km + 2m et un nombre total de littéraux égal à : 10nkm + 7n 9km + m2 + 3m 2 Enfin, on peut remarquer que l’encodage SeqBn (où K 2K est le complèmentaire de K) appliqué à (:x1; :::; :xn) donne également la contrainte 2 K(x1; :::; xn). On note SeqB:n cet encodage. Il peut éventuellement être plus perfor2mKant que l’encodage précédent selon K. Son nombre total de clauses et son nombre total de littéraux s’obtiennent en remplaçant km par max(K) et m par n m dans (5) et (6).
Le pire des cas est atteint pour une contrainte de type k pair. On a alors un nombre de clauses de l’ordre de 4n2 et un nombre de littéraux de l’ordre de 10:5n2 ce qui est tout à fait raisonnable. Par ailleurs, à notre connaissance, il s’agit du seul encodage CNF de la littérature de la contrainte 2 K(x1; :::; xn). 4
Lorsque l’on recherche un algorithme optimisé pour un problème donné, il est rare de découvrir un seul algorithme qui soit le plus optimisé pour chacune des occurrences de ce problème. Pour le problème d’une résolution CNF-SAT d’une contrainte de cardinalité, on peut remarquer que chacun des encodages d’une contrainte de cardinalité considérés dans cet article est préférable aux autres pour au moins quelques valeurs différentes de k et n. Par ailleurs, les comportements des différentes solutions à l’infini ne préjugent en rien quant à leurs comportements en faible dimension. Par exemple dans le cas des contraintes k(x1; :::; xn) et k(x1; :::; xn), l’encodage proposé par Bailleux et Boufkhad est préférable (selon le critère du nombre total de littéraux) dans environ 10% des cas lorsque n est très grand mais n’est préférable en aucun cas lorsque n < 149. Afin de pouvoir déterminer l’encodage réellement le mieux adapté à une contrainte et des paramètres donnés, il est nécessaire de passer par une étude exhaustive des cas comme cela a été réalisé dans cet article.
On pourrait objecter que, si n est petit alors la taille de l’encodage le sera également et qu’en conséquence, même si on reste loin de l’optimum possible, on pourra négliger l’accroissement. Cet argument ne tient toutefois pas longtemps car un gain fixe sur une opération peut être non négligeable, d’autant plus si cette opération est répétée de nombreuses fois au cours d’un même processus.
Par ailleurs, le nouvel encodage séquentiel bidirectionnel qui est proposé dans cet article offre une performance nettement améliorée dans certains cas ainsi que des perspectives nouvelles.
En effet, dans le cas d’une contrainte de type =
k(x1; :::; xn), les nombres totaux de clauses et de littéraux
sont au mieux quadratiques en n pour les autres encodages
et ceci quel que soit k. Toutefois, dans un certain nombre de
problèmes, k est fixé indépendamment de n. Les nombres
totaux de clauses et de littéraux de l’encodage séquentiel
bidirectionnel sont alors linéaires en n. Cet encodage a
ainsi pu être mis à profit dans le cas de la résolution SAT
d’un problème d’emploi du temps en BTS [
Enfin, on peut noter que sa présentation explicite
(semblable à celle de l’encodage séquentiel dans [
Le travail de recherche présenté dans cet article est d’ordre
théorique. Si les critères du nombre total de clauses ou du
nombre total de littéraux sont généralement pertinents, ils
ne suffisent pas à déterminer l’encodage le mieux adapté
qui pourra dépendre non seulement du problème considéré
mais également du solveur utilisé. Il appelle donc d’autres
travaux qui permettront de mettre en pratique (tels que [
Annexe 5 k Les tableaux 10 et 11 donnent, en fonction de k et n, les encodages de = k(x1; :::; xn) pour n 2 J6; 17K ayant un TABLE 11 – Encodage de la contrainte = k(x1; :::; xn) donnant le nombre total minimal de littéraux pour n 2 J6; 17K nombre total minimal de clauses et de littéraux respectivement. Les encodages sont indiqués dans le tableau par un numéro qui correspond à leur numérotation dans la section 3.4.