Réduisez le problème suivant à SAT

Voici le problème. Étant donné , où chaque . Existe-t-il un sous-ensemble dont la taille est au plus telle que pour tout ? J'essaie de réduire ce problème à SAT. Mon idée d'une solution serait d'avoir une variable pour chacun de 1 à . Pour chaque , créez une clause si . Ensuite et toutes ces clauses ensemble. Mais ce n'est clairement pas une solution complète car elle ne représente pas la contrainte queT i ⊆ { 1 , … , n } S ⊆ { 1 , … , n } k S ∩ T i ≠ ∅ i x i n T i ( x i 1 ∨ ⋯ ∨ x i k ) T i = { i 1$k, n, T_1, \ldots, T_m$$T_i \subseteq \{1, \ldots, n\}$$S \subseteq \{1, \ldots, n\}$$k$$S \cap T_i \neq \emptyset$$i$$x_i$$n$$T_i$$(x_{i_1} \vee \cdots \vee x_{i_k})$$T_i = \{i_1, \ldots, i_k\}$$S$doit avoir au plus éléments. Je sais que je dois créer plus de variables, mais je ne sais tout simplement pas comment. J'ai donc deux questions:$k$

1. Mon idée de solution est-elle sur la bonne voie?
2. Comment créer les nouvelles variables pour qu'elles puissent être utilisées pour représenter la contrainte de cardinalité ?$k$

Il semble que vous essayez de calculer un hypergraphe transversal de taille . Autrement dit, est votre hypergraphe, et est votre transversale. Une traduction standard consiste à exprimer les clauses telles que vous les avez, puis à traduire la restriction de longueur en une contrainte de cardinalité.{ T 1 , … , T m } $k$$\{T_1,\dots,T_m\}$$S$

Utilisez donc votre encodage existant, c'est-à-dire puis ajoutez des clauses encodant .∑ 1 ≤ i ≤ n xi≤$\bigwedge_{1 \le j \le m} \bigvee_{i \in T_j} x_i$$\sum_{1 \le i \le n} x_i \le k$

$\sum_{1 \le i \le n} x_i \le k$ est une contrainte de cardinalité. Il existe différentes traductions de contraintes de cardinalité en SAT.

La traduction de contrainte de cardinalité la plus simple mais la plus grande est simplement . De cette façon, chaque disjonction représente la contrainte - pour tous les sous-ensembles de de taille k + 1. Autrement dit, nous nous assurons qu'il n'y a aucun moyen de définir plus de k variables. Notez que ce n'est pas une taille polynomiale en ¬ ⋀ i ∈ X x i X { 1 , … , n } k$\bigwedge_{X \subseteq \{1,\dots,n\}, |X| = k+1} \bigvee_{i \in X} \neg x_i$$\neg \bigwedge_{i \in X} x_i$$X$$\{1,\dots,n\}$$k$

Quelques liens vers des articles sur des traductions de contraintes de cardinalité plus efficaces en espace qui sont de taille polynomiale en$k$ :

• Traduire les contraintes pseudo-booléennes en SAT - Niklas Eén et Niklas Sörensson, JSAT vol 2 (2006), p. 1-26 (une bonne enquête).
• Codage CNF efficace des contraintes de cardinalité booléenne - Olivier Bailleux et Yacine Boufkhad, Actes de principes et pratique de programmation par contraintes 2003, LNCS vol 2833, p. 108-122 (une traduction agréable et assez facile à mettre en œuvre).
• Vers un codage CNF optimal des contraintes de cardinalité booléenne - Carsten Sinz - Actes de principes et pratiques de programmation par contraintes 2005, LNCS 3709, pg 827-831.
• Vers des codages CNF robustes des contraintes de cardinalité - Joao Marques-Silva et Inês Lynce, Actes de principes et pratiques de programmation par contraintes 2007, LNCS 4741, p. 483-497.

Si vous êtes réellement intéressé à résoudre de tels problèmes, il est peut-être préférable de les formuler comme des problèmes pseudo-booléens (voir l' article wiki sur les problèmes pseudo-booléens ) et d'utiliser des solveurs pseudo-booléens (voir la concurrence pseudo-booléenne ). De cette façon, les contraintes de cardinalité ne sont que des contraintes pseudo-booléennes et font partie du langage - espérons que le solveur pseudo-booléen les traite ensuite directement et donc plus efficacement.

Si vous n'êtes pas absolument défini sur le SAT normal, votre idée est déjà une réduction à MIN-ONES (sur des formules CNF positives), qui est fondamentalement SAT, mais où vous pouvez définir au plus variables sur true (strictement c'est l'optimisation version où nous minimisons le nombre de vraies variables).$k$

De même, si vous vous dirigez dans une direction de complexité paramétrée, alors vous avez déjà essentiellement WSAT ( ), où est la classe de tous les positifs Formules CNF (comme précédemment, la notation pourrait cependant aider vos investigations). Dans ce cas, vous devez commencer à regarder quel paramétrage serait utile dans votre cas. Γ + 2 , $\Gamma_{2,1}^{+}$$\Gamma_{2,1}^{+}$

Je suppose que vous recherchez une réduction explicite, mais sinon, vous pouvez toujours vous rabattre sur le théorème de Cook-Levin .