Choisir un encodage CNF de contraintes de cardinalité performant pour SAT T. Delacroix IMT Atlantique - Dépt. LUSSI, Brest, France thomas.delacroix@imt-atlantique.fr Résumé veur et à la fois de la façon dont la contrainte est exprimée sous forme CNF. Cet article répond à une double problématique : (1) com- ment choisir un encodage CNF pour des contraintes de De nombreux travaux se sont donc penchés sur la ques- cardinalité de type #k(x1 , ..., xn ) où # peut être l’un des tion de savoir comment exprimer des contraintes classiques symboles ≤, =, ≥ ; (2) déterminer un encodage CNF per- des CSP sous forme CNF de manière performante pour les formant pour les contraintes de cardinalité plus générales solveurs CNF-SAT [1, 2, 3, 4, 5, 7, 10, 14, 15]. C’est le ∈ K(x1 , ..., xn ) où K ⊂ J0, nK. Pour ce faire, on intro- cas notamment pour les contraintes de cardinalité 1 de type duit d’abord un nouvel encodage séquentiel bidirectionnel. #k(x1 , ..., xn ) où # peut être l’un des symboles ≤, =, ≥. On décrit alors un processus pour choisir l’encodage le En effet, un encodage naïf de ces contraintes contient, dès plus performant pour une contrainte de cardinalité donnée que n augmente, beaucoup trop de clauses pour pouvoir s’appuyant sur une comparaison de différents encodages être utilisé de manière raisonnable en pratique. De nom- pour tous les cas possibles de valeurs n et k. Enfin, on breux encodages CNF ont donc été proposés, fonctionnant montre que l’encodage séquentiel bidirectionnel permet de tous sur le même principe général : des variables supplé- répondre à la problématique (2). mentaires sont introduites de manière à réduire drastique- ment le nombre de clauses. Mots Clef Parmi les travaux existants, on trouve des comparaisons CNF, SAT, encodage, contraintes de cardinalité. des différents encodages proposés [2, 9, 12]. Toutefois, ces comparaisons ne sont pas exhaustives. En effet, l’ac- Abstract cent y est généralement mis sur le comportement des en- This article has a double aim : (1) define a process for codages lorsque n tend vers l’infini. Or, en pratique, on choosing the most efficient CNF encoding for cardinality peut également être amené à considérer de très nombreuses constraints of type #k(x1 , ..., xn ) where # is one of the contraintes de cardinalité de faible dimension. Une compa- following symbols ≤, =, ≥ ; (2) determine an efficient CNF raison exhaustive des encodages existants s’impose donc encoding for the more general cardinality constraints of afin d’essayer d’optimiser au maximum l’étape du choix de type ∈ K(x1 , ..., xn ) where K ⊂ J0, nK. In order to do this, l’encodage dans la résolution SAT et cela constitue un des we introduce a new sequential bidirectional encoding. We éléments central de cet article. On s’aperçoit alors qu’il n’y then describe a process for choosing the most efficient en- a pas un encodage plus performant que tous les autres mais coding for a given cardinality constraint based on a com- de nombreux encodages performants selon les paramètres parison of different encodings for all possible values of n du problème. On montre également qu’il est possible de and k. Finally, we show that the sequential bidirectional combiner des encodages pour obtenir de meilleures perfor- encoding can be used to reach our second aim. mances. Keywords Par ailleurs, on introduit dans cet article un nouvel enco- dage : l’encodage séquentiel bidirectionnel. Cet encodage, CNF, SAT, encoding, cardinality constraints. dont la définition est assez naturelle, est particulièrement adapté pour considérer des contraintes de cardinalité plus 1 Introduction complexes, notamment les contraintes de cardinalité cor- Parmi les solveurs modernes en programmation sous respondant à un intervalle. On montre par ailleurs qu’il contrainte les plus performants, on trouve aujourd’hui un permet de considérer des contraintes de cardinalité de type certain nombre de solveurs CNF-SAT. Les palmarès ré- ∈ K(x1 , ..., xn ) où K ⊂ J0, nK de manière performante ce cents du MiniZinc Challenge en témoignent [13, 11]. qui représente une nouveauté. Un solveur CNF-SAT permet d’obtenir une valuation pour laquelle une expression logique sous forme conjonctive 1. Le terme contrainte de cardinalité est utilisé ici selon la nomen- normale (CNF) donnée est satisfaite lorsqu’il en existe une. clature standard dans le contexte SAT et ne doit pas être confondu avec Pour une contrainte particulière, la performance du solveur d’autres notions telles que celle de global cardinality constraint utilisée dépend donc à la fois de l’algorithme de résolution du sol- dans le contexte de la programmation sous contrainte. 2 Encodage séquentiel bidirectionnel n rajout de ces deux clauses. On note SeqB≤k n , SeqB≥k et n SeqB=k les encodages respectifs correspondants. Dans la suite, on considère des entiers n et k tels que n ≥ 2 et k ∈ J1, n − 1K, les autres cas étant évidemment triviaux. La démarche qui mène à définir l’encodage proposé dans 3 Choisir son encodage cette section s’apparente à la démarche qui mène à l’en- 3.1 Comparaisons des encodages codage séquentiel proposé par Carsten Sinz dans [12]. En En plus des encodages décrits précédemment, on va égale- effet, dans l’article Pi précité, l’auteur définit les sommes par- n ment considérer l’encodage naïf (N≤k ) défini par : tielles si = m=1 xm et considère le j-ième bit si,j de la représentation unaire de si . Il transpose alors ces bits ^ k+1 _ n en variable booléenne dans un encodage CNF pour abou- ¬xij (N≤k ) tir à l’encodage ci-dessous pour la contrainte de cardinalité k+1 j=1 i∈Cn ≤ k(x1 , ..., xn ). Par la suite, on le désigne par le nom d’en- codage séquentiel unidirectionnel et on le note SeqU≤k n . 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 & n (¬x1 ∨ s1,1 ) Boufkhad dans [3] (BB≥k 1 ,≤k2 ). On note que les auteurs (¬s1,j ) ∀j ∈K1, kK précités ne donnent pas d’expression explicite de leur en- codage mais décrivent plutôt un algorithme permettant de  (¬xi ∨ si,1 )  le construire.  (¬si−1,1 ∨ si,1 )    (¬xi ∨ ¬si−1,j−1 ∨ si,j )  ∀i ∈K1, nJ D’autres encodages de la littérature [15] ne sont pas consi- ∀j ∈K1, kK dérés car ils ne satisfont pas la condition de performance (¬si−1,j ∨ si,j )   relative à la propagation unitaire décrite initalement dans  (¬xi ∨ ¬si−1,k )  (¬xn ∨ ¬sn−1,k ) [3] (i.e. il ne permettent pas de vérifier la contrainte sur n une valuation partielle des variables xi ). (SeqU≤k ) Par ailleurs, par manque de temps, nous n’avons pas in- Cependant, cette transposition contient une réduction qui tégré ici d’encodage à base de réseaux [1, 2, 7]. En ef- aboutit à une perte d’information entre la variable si,j tel fet, nous souhaitons d’abord vérifier que la génération de qu’elle est encodée dans SeqU≤k n par rapport au bit si,j dé- tels encodages est bien linéaire en leur nombre total de crit précédemment. En effet, le bit si,j est équivalent à si ≥ clauses (ou de littéraux), de manière à ce que la compa- j. Or l’encodage SeqU≤k n donne (si ≥ j) =⇒ si,j mais raison soit valable. Ce travail reste donc à compléter sur pas l’implication réciproque. Cette perte d’information est ce point. En effet, de tels encodages peuvent comporter volontaire car elle entraine un encodage plus restreint de un nombre total de clauses inférieur à ceux des encodages la contrainte ≤ k(x1 , ..., xn ). Toutefois, ce choix n’est pas considérés ici pour un certain nombre de valeurs de n et k. forcément judicieux lorsque l’on considère une contrainte Ceci est notamment le cas de l’encodage de la contrainte = k(x1 , ..., xn ) ou deux contraintes ≥ k1 (x1 , ..., xn ) et ≤ k(x1 , ..., xn ) proposé par Asín et al. dans [2] dont le ≤ k2 (x1 , ..., xn ) définissant un intervalle. nombre total de clauses est égal à : L’encodage CNF qui suit permet d’encoder exactement 3 3 3 l’ensemble des équivalences (si ≥ j) ⇐⇒ si,j pour tout −3m+6mK+ mK log2 (K)+ mK log2 (K)−3K− K log2 (K) 4 4 2 i ∈ J1, nK et pour tout j ∈ J1, k + 1K. On appelle enco- avec K = 2dlog2 (k)e et m = n dage séquentiel bidirectionnel cet encodage et on le note n K . SeqB#k . Le tableau 1 donne le nombres de clauses (avec le détail en (x1 ∨ ¬s1,1 ) fonction de la taille en nombre de littéraux de ces clauses) (¬xi ∨ si,1 ) ∀i ∈ J1, nK ainsi que le nombre de variables auxilaires pour chacun de (¬sj−1,j ) ∀j ∈K1, k +  1K ces encodages. Les valeurs figurant dans ce tableau ont été recalculées à partir des descriptions de ces encodages dans  (¬si−1,j ∨ si,j ) ∀j ∈ J1, k + 1K  (xi ∨ si−1,j ∨ ¬si,j )  les articles précités [12, 3] ainsi que le présent article.  ∀i ∈K1, nK (si−1,j−1 ∨ ¬si,j ) ∀j ∈K1, k + 1K   (¬xi ∨ ¬si−1,j−1 ∨ si,j )  Dans la suite de cet article, on utilise les informations n de ce tableau pour permettre de choisir l’encodage le (SeqB#k ) mieux adapté aux différents cas étudiés. On fera également usage de la règle suivante pour obtenir un encodage d’une À partir de cet encodage, il est très facile d’obtenir la contrainte ≥ k(x1 , ..., xn ) en considérant l’encodage pour contrainte de cardinalité ≤ k(x1 , ..., xn ). En effet, il suf- la contrainte ≤ k(x1 , ..., xn ) via l’utilisation de la règle fit de rajouter la clause ¬sn,k+1 . De même, la contrainte ≥ suivante : k(x1 , ..., xn ) s’obtient simplement par le rajout de la clause sn,k . Enfin, la contrainte = k(x1 , ..., xn ) s’obtient par le ≥ k(x1 , ..., xn ) ⇐⇒ ≤ (n − k)(¬x1 , ..., ¬xn ) (1) De même, on pourra obtenir un encodage de la contrainte On remarque d’abord que pour une telle contrainte, l’en- n = k(x1 , ..., xn ) en combinant différents encodages via codage SeqU≤k est clairement toujours plus performant n l’utilisation de la constation suivante : que l’encodage SeqB≤k donc on peut exclure ce der- nier de notre comparaison. Par contre, en utilisant (1), n = k(x1 , ..., xn ) ⇐⇒ (≤ k(x1 , ..., xn )∧ ≥ k(x1 , ..., xn )) on peut considérer l’encodage SeqB≥n−k appliqué à ¬n (2) (¬x1 , ..., ¬xn ). On note SeqB≥n−k cet encodage. n n On cherche donc à comparer les encodages N≤k , SeqU≤k , ¬n n SeqB≥n−k , BB≥0,≤k . Une analyse complète des diffé- Nombre de Nombre de rents nombres totaux de clauses pour chacun de ces enco- Encodage clauses composées variables dages permet de déterminer l’encodage offrant le plus petit de m littéraux auxiliaires nombre de clauses en fonction de n et k. On a réalisé cette m=1 k−1 analyse ici et regroupé les résultats dans le tableau 2. Ce ta- n m=2 nk + 2n − 2k − 2 SeqU≤k nk − k bleau décrit, en fin de compte, une partition de l’ensemble m=3 nk − n − 2k + 2 Total 2nk + n − 3k − 1 des valeurs potentielles de n et k en 4 parties, chacune cor- m=1 k respondant aux valeurs de n et k pour lesquelles l’enco- n SeqB#k m=2 2nk + 2n − 2k dage en colonne est optimal (pour le critère du nombre de nk + n m=3 2nk + n − 2k − 1 clauses considéré ici). Total 4nk + 3n − 3k − 1 n n  N≤k m=k+1 k+1 0 Conditions sur n et k par encodage m=1 n − k2 + k1 n SeqU≤k n BB≥0,≤k ¬n SeqB≥n−k n N≤k n2 + 2n log2 (n) n 2 m=3 n ≤ 5 et k ∈ BB≥k1 ,≤k2 +n − 2 n log2 (n) n2 + 2n log2 (n) ∅ ∅ ∅ J1, nJ Total +2n − k2 + k1 − 2 6 ≤ n ≤ 7 et k ∈ J1, k1 J ∅ ∅ Jk1 , nJ où k1 = n − 3. TABLE 1 – Nombre et tailles de clauses pour chaque enco- 8 ≤ n ≤ 10 et k ∈ dage considéré J1, k1 J ∅ ∅ Jk1 , nJ où k1 = n − 2. 3.2 Contrainte ≤ k(x1 , ..., xn ) 11 ≤ n ≤ 27 et k ∈ J1, k2 J ∅ Jk2 , k1 J m Jk1 , nJ Dans cette secion, on compare différents encodages de ≤ l 10n2 −3n−3 où k1 = n − 2 et k2 = 3(5n−6) . k(x1 , ..., xn ). 28 ≤ n ≤ 148 et k ∈ Conditions sur n et k par encodage J1, k2 J ∅ Jk2 , k1 J m Jk1 , nJ 10n2 −3n−3 l n SeqU≤k n BB≥0,≤k ¬n SeqB≥n−k n N≤k où k1 = n − 1 et k2 = . 3(5n−6) n ≤ 5 et k ∈ 149 ≤ n et k ∈ ∅ ∅ ∅ J1, nJ J1, k3 J Jk3 , k2 J Jk , k J Jk1 , nJ l 2 2 1 m 7n −6n log2 (n)−6n+4 6 ≤ n ≤ 8 et k ∈ où k1 = n − 1, k2 = 10(n−1) J1, k1 J ∅ ∅ Jk1 , nJ l 2 m 3n +6n log2 (n)+3n−7 et k3 = 5n−8 . où k1 = n − 4. 9 ≤ n ≤ 13 et k ∈ TABLE 3 – Encodage de ≤ k(x1 , ..., xn ) donnant le J1, k1 J ∅ ∅ Jk1 , nJ où k1 = n − 3. nombre total minimal de littéraux en fonction de n et k 14 ≤ n ≤ 30 et k ∈ J1, k2 J ∅ Jk2 , k1 J Jk1 , nJ Le tableau 2 permet de choisir un encodage en fonction du où k1 = n − 3 et k2 = 23 (n + 1) .   nombre de clauses de cet encodage mais il ne prend pas 31 ≤ n ≤ 36 et k ∈ en compte la taille de ces clauses (i.e. le nombre de litté- J1, k2 J ∅ Jk2 , k1 J Jk1 , nJ raux par clause). Or la taille des clauses dans une contrainte où k1 = n − 2 et k2 = 23 (n + 1) .   CNF peut avoir une influence importante sur la rapidité 37 ≤ n et k ∈ d’un solveur SAT sur cette contrainte. Comme l’évalua- J1, k3 J Jk3 , k2 J Jk , k J Jk1 , nJ tion d’une valuation d’une contrainte CNF est linéaire par l 2 2 1 où k1 = n − 2, k2 = 3n −2n log2 (n)−2n+2 m rapport à son nombre total de littéraux, on pourrait égale- 4(n−1) l 2 n +2n log2 (n)+n−1 m ment considérer le nombre total de littéraux de chacun de et k3 = . 2(n−1) encodages plutôt que leur nombre de clauses comme cri- tère pour choisir un encodage. Même si le nombre total de TABLE 2 – Encodage de ≤ k(x1 , ..., xn ) donnant le clauses est généralement utilisé comme critère de compa- nombre total minimal de clauses en fonction de n et k raison des encodages dans l’état de l’art précité, on penche 2. Les valeurs données ici sont exactes si n est une puissance de 2. plutôt pour l’utilisation du nombre total de littéraux. En tout état de cause, on présentera systèmatiquement par la tient bien la contrainte souhaitée en appliquant les enco- n n n suite les valeurs obtenues pour chacun de ces deux critères. dages N≤n−k , SeqU≤n−k et SeqB≤n−k à (¬x1 , ..., ¬xn ). ¬n ¬n ¬n Le tableau 3 permet de déterminer l’encodage avec le plus On note respectivement N≤n−k , SeqU≤n−k et SeqB≤n−k petit nombre total de littéraux. ces trois encodages. On considère par ailleurs les deux en- n n codages SeqB≥k et BB≥k,≤n . 3.3 Contrainte ≥ k(x1 , ..., xn ) Comme précédemment, on détermine les encodages don- nant le nombre total minimal de clauses (tableau 4) ainsi Conditions sur n et k par encodage que les encodages donnant le nombre total minimal de lit- ¬n N≤n−k SeqB≥k n n BB≥k,≤n ¬n SeqU≤n−k téraux (5) en fonction de n et k. On remarque que, dans ce ¬n n ≤ 5 et k ∈ cas, c’est l’encodage SeqB≤n−k qui est écarté systémati- J1, nJ ∅ ∅ ∅ quement. 6 ≤ n ≤ 8 et k ∈ J1, 5J ∅ ∅ J5, nJ 3.4 Contrainte = k(x1 , ..., xn ) 9 ≤ n ≤ 13 et k ∈ Dans cette section, on compare 7 encodages différents de = J1, 4J ∅ ∅ J4, nJ k(x1 , ..., xn ) parmi lesquels 2 sont des encodages mixtes 14 ≤ n ≤ 30 et k ∈ entre deux encodages différents. Il s’agit des encodages : J1, 4J J4, k1 J ∅ Jk1 , nJ n n où k1 = n−1  3  . 1. BB=k (i.e. BB≥k,≤k ); 31 ≤ n ≤ 36 et k ∈ n 2. SeqB=k ; J1, 3J J3, k J ∅ Jk1 , nJ  n−1  1 ¬n où k1 = . 3. SeqB=n−k ; 3 37 ≤ n et k ∈ n n ¬n 4. SeqU=k (i.e. SeqU≤k et SeqU≤n−k ); J1, 3J J3, k2 J Jk2 , k1 J Jk1 , nJ n n ¬n l 2 n −2n log2 (n)−n+1 m 5. N=k (i.e. N≤k et N≤n−k ); où k1 = 2(n−1) n n ¬n 6. N S=k (i.e. N≤k et SeqU≤n−k ); l 2 m n +2n log2 (n)−2n−2 et k2 = 4(n−1) . n n ¬n 7. SN=k (i.e. SeqU≤k et N≤n−k ). TABLE 4 – Encodage de ≥ k(x1 , ..., xn ) donnant le nombre total minimal de clauses en fonction de n et 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 to- Conditions sur n et k par encodage tal de littéraux minimal en fonction des mêmes paramètres. ¬n N≤n−k SeqB≥k n n BB≥k,≤n ¬n SeqU≤n−k Chacun de ces résultats étant difficilement synthétisable en n ≤ 5 et k ∈ un seul tableau, on renvoie aux annexes pour le détail pour J1, nJ ∅ ∅ ∅ tous les entiers n ∈ J6, 17K. n = 6 et k ∈ {1, 2, 3, 5} ∅ ∅ k=4 Proportion Encodage Condition sur k en n → +∞ n = 7 et k ∈ n SN=k 1≤k<3 0% J1, 4J ∅ ∅ J4, nJ n SeqB=k 3 ≤ k < k2 25% 8 ≤ n ≤ 10 et k ∈ n BB=k k2 ≤ k < k1 50% J1, 3J ∅ ∅ J3, nJ ¬n SeqB=n−k k1 ≤ k < n − 2 25% 11 ≤ n ≤ 27 et k ∈ n N S=k n−2≤k