Encodage d'une contrainte sur 1 pour les solveurs SAT

J'utilise un solveur SAT pour coder un problème, et dans le cadre de l'instance SAT, j'ai des variables booléennes $x_1,x_2,\dots,x_n$ où il est prévu que l'une d'entre elles soit vraie et que le reste soit être faux. (J'ai parfois vu cela décrit comme un encodage "à chaud".)

Je veux encoder la contrainte "exactement un sur $x_1,\dots,x_n$ doit être vrai" dans SAT. Quelle est la meilleure façon de coder cette contrainte, pour faire fonctionner le solveur SAT aussi efficacement que possible?

Je peux voir de nombreuses façons de coder cette contrainte:

• Contraintes par paire. Je pourrais ajouter des contraintes par paire $\neg x_i \lor \neg x_j$ pour tout $i,j$ pour m'assurer qu'au plus un $x_i$ est vrai, puis ajouter $x_1 \lor x_2 \lor \cdots \lor x_n$ pour m'assurer qu'au moins un est vrai.

  Cela ajoute des clauses $\Theta(n^2)$ et aucune variable booléenne supplémentaire.

• Encodage binaire. Je pourrais introduire $\lg n$ nouvelles variables booléennes $i_1,i_2,\dots,i_{\lg n}$ pour représenter (en binaire) un entier $i$ tel que $1 \le i \le n$ (en ajoutant quelques contraintes booléennes pour s'assurer que $i$ est dans la plage souhaitée ). Ensuite, je peux ajouter des contraintes imposant que $x_i$ est arbre et que tous les autres $x_j$ sont faux. En d'autres termes, pour chaque $j$ , nous ajoutons des clauses imposant que $i=j \Leftrightarrow x_j$ .

  Cela ajoute des clauses $\Theta(n \lg n)$ et je ne sais pas combien de variables booléennes supplémentaires.

• Comptez le nombre de vraies valeurs. Je pourrais implémenter un arbre de circuits d'additionneurs booléens et exiger que $x_1+x_2+\dots+x_n=1$ , en traitant chaque $x_i$ comme 0 ou 1 au lieu de faux ou vrai, et utiliser la transformation Tseitin pour convertir le circuit en SAT clauses. Un arbre de demi-additionneurs suffit: contraignez la sortie de report de chaque demi-additionneur à 0, et contraignez la sortie finale du demi-additionneur final de l'arbre à 1. L'arbre peut être choisi pour être de n'importe quelle forme ( arbre binaire équilibré, ou déséquilibré, ou autre).

  Cela peut être fait en portes et ajoute ainsi thetav ( n ) clauses et Θ ( n ) de nouvelles variables booléennes.$\Theta(n)$$\Theta(n)$$\Theta(n)$

  Un cas particulier de cette approche est d'introduire des variables booléennes , avec l'idée que y i devrait contenir la valeur de x 1 ∨ x 2 ∨ ⋯ ∨ x i . Cette intention peut être appliquée en ajoutant les clauses y i ∨ ¬ x i , y i ∨ ¬ y i - 1 , et ¬ y i ∨ x i ∨ y i $y_1,\dots,y_n$$y_i$$x_1 \lor x_2 \lor \cdots \lor x_i$$y_i \lor \neg x_i$$y_i \lor \neg y_{i-1}$ (où nous traitons y 0 comme synonyme de faux) pouri=1,…,n. Ensuite, on peut ajouter les restrictions¬ y i ∨¬ x i + 1 pouri=1,2,…,n-1. Ceci est fondamentalement équivalent à la transformée Tseitin d'un arbre à moitié additionneur, où l'arbre a une forme au maximum déséquilibrée.$\neg y_i \lor x_i \lor y_{i-1}$$y_0$$i=1,\dots,n$$\neg y_i \lor \neg x_{i+1}$$i=1,2,\dots,n-1$

• Réseau de papillons. Je pourrais construire un réseau papillon sur bits, contraindre l' entrée à n bits à 000 ⋯ 01 , contraindre la sortie à n bits à x 1 x 2 ⋯ x n , et traiter chaque porte papillon 2 bits comme une porte indépendante qui permute ou n'échange pas son entrée avec la décision de le faire sur la base d'une nouvelle variable booléenne qui n'est pas contrainte. Ensuite, je peux appliquer la transformée Tseitin pour convertir le circuit en clauses SAT.$n$$n$$000\cdots 01$$n$$x_1 x_2 \cdots x_n$

  Cela nécessite portes et ajoute donc Θ ( n lg n ) clauses et Θ ( n lg n ) nouvelles variables booléennes.$\Theta(n \lg n)$$\Theta(n \lg n)$$\Theta(n \lg n)$

Y a-t-il d'autres méthodes que j'ai ignorées? Lequel devrais-je utiliser? Quelqu'un l'a-t-il testé ou essayé expérimentalement, ou quelqu'un a-t-il une expérience avec l'un de ces éléments? Le nombre de clauses et / ou le nombre de nouvelles variables booléennes est-il une bonne métrique stand-in pour estimer l'impact de ceci sur les performances du solveur SAT, ou sinon, quelle métrique utiliseriez-vous?

Je viens de remarquer que cette réponse a des références sur l'application des contraintes de cardinalité pour SAT, c'est-à-dire, l'application de la contrainte selon laquelle exactement des n variables sont vraies. Donc, ma question se résume à un cas spécial où k = 1 . Peut-être que la littérature sur les contraintes de cardinalité aidera à éclairer ma question.$k$$n$$k=1$

Pour le cas spécial de k sur n variables vraies où k = 1, il existe un codage de variable de commande comme décrit dans EOD CNF Encoding for Selecting 1 to N Objects by Klieber and Kwon. Simplifié: divisez les variables en petits groupes et ajoutez des clauses qui font que l'état d'une variable de commande implique qu'un groupe de variables est soit faux soit tout sauf un. Ensuite, appliquez récursivement le même algorithme aux variables de commande. À la fin du processus, exigez que l'exactement l'une des quelques variables finales du commandant soit vraie. Le résultat est O (n) nouvelles clauses et O (n) nouvelles variables.

Étant donné l'omniprésence des littéraux à deux observés dans les solveurs basés sur DPLL, je pense que la croissance de la clause O (n) est un avantage décisif par rapport aux schémas de codage qui ajouteraient plus de clauses.

Un article de Magnus Björk décrit deux techniques qui pourraient valoir la peine d'être essayées.

Pour 1-out-of- , on peut utiliser à la fois d' un hot et codage binaire simultanément. Ainsi, nous avons x 1 , … , x n comme un codage à chaud, et y 1 , … , y b comme un codage binaire, où b = lg n . On peut encoder facilement la "au moins une" contrainte, en une seule clause: ( x 1 ∨ ⋯ ∨ x n ) . On peut également forcer les deux encodages à être cohérents avec 2 lg $n$$x_1,\dots,x_n$$y_1,\dots,y_b$$b = \lg n$$(x_1 \lor \dots \lor x_n)$$2 \lg n$clauses: on ajoute simplement ou x $x_i \implies \neg y_j$ , selon que le j ème bit du codage binaire de i est 0 ou 1. Enfin, la contrainte "au plus un" suit automatiquement. Cela permet également au reste de l'instance SAT d'utiliser le codage le plus pratique.$x_i \implies y_j$$j$$i$

Pour -out-of- n , on peut appliquer un réseau de tri à l'entrée x 1 , … , x n pour obtenir la sortie triée y 1 , … , y n , puis ajouter une clause exigeant que y k soit vrai et y k + 1 est faux. Il existe un certain nombre de réseaux de tri simples qui ne nécessitent que des unités de comparaison O ( n lg 2 n ) . Par conséquent, nous obtenons un encodage qui utilise O ( n lg $k$$n$$x_1,\dots,x_n$$y_1,\dots,y_n$$y_k$$y_{k+1}$$O(n \lg^2 n)$ clauses et variables temporaires.$O(n \lg^2 n)$

Le papier est

Magnus Björk. Techniques d'encodage SAT réussies . 25 juillet 2009.

L'article suivant contient une liste détaillée des codages pour 1 sur et k sur - n , avec une évaluation expérimentale de chacun d'eux. Les conclusions ne sont pas tout à fait claires (l'encodage des commandes semble assez bon dans leurs expériences).$n$$k$$n$

Alan M. Frisch, Paul A. Giannaros. Encodages SAT de la contrainte At-Most-k: certains anciens, certains nouveaux, certains rapides, certains lents . ModRef 2010.