Le problème paramétré k-FLIP SAT est défini comme suit:
Entrée: une formule 3-CNF avec n variables et une affectation de vérité \ sigma: [n] \ à \ {0,1 \} Paramètre: k Question: pouvons-nous transformer l'affectation \ sigma en une affectation satisfaisante \ sigma ' pour \ varphi retourner la valeur de vérité d'au plus k variables?
Le problème est clairement en FPT ( Stefan Szeider: La complexité paramétrée de la recherche locale k-Flip pour SAT et MAX SAT. Optimisation discrète 8 (1): 139-145 (2011) )
Admet-il un noyau polynomial? (sous des hypothèses de complexité raisonnable)
Les techniques récentes de composition croisée (voir Hans L. Bodlaender, Bart MP Jansen, Stefan Kratsch, "Kernelization Lower Bounds By Cross-Composition" ) semblent inutiles pour ce problème. Et ils semblent également inutiles pour des problèmes similaires qui demandent si une solution donnée à un problème NP-difficile peut être trouvée à partir d'une instance donnée par une recherche locale (en limitant la recherche aux voisins de l'instance donnée, sous une mesure de distance naturelle).
la source
Réponses:
Le problème n'a pas de noyau polynomial à moins que NP ne soit en coNP / poly. La technique de composition croisée de notre article s'applique de manière non triviale.
Permettez-moi de montrer comment le problème classique de Vertex Cover OR-cross-compose dans le problème k-FLIP-SAT; d'après les résultats de l'article cité, cela suffit. Concrètement, nous construisons un algorithme à temps polynomial dont l'entrée est une séquence d'instances de Vertex Cover qui partagent toutes la même valeur de et toutes ont exactement sommets. La sortie est une instance de -FLIP SAT avec une valeur de paramètre de , qui est suffisamment petite pour une composition croisée, de sorte que l' instance -FLIP SAT a répondu oui si une des entrées les graphiques ont une couverture de sommet de taillek n k O ( k + log t ) k k t( G1, k ) , ( G2, k ) , … , ( Gt, k ) k n k O ( k + logt ) k k . En dupliquant une entrée (ce qui ne change pas la valeur de l'OR), nous pouvons nous assurer que le nombre d'entrées est une puissance de deux.t
La composition se déroule comme suit. Numérotez les sommets du graphe de chaque graphe d'entrée comme . Créez une variable correspondante dans l'instance FLIP-SAT pour chaque sommet de chaque graphique d'entrée. De plus, créez une variable de sélection pour chaque numéro d'instance d'entrée . Pour chaque graphe d'entrée , nous ajoutons quelques clauses à la formule. Pour chaque arête du graphe , ajoutez la clause à la formule, qui encodera "l'un des points d'extrémité de ce bord est défini sur true, ou l'instancev i , 1 , v i , 2 , … , v i , n u i i ∈ [ t ] G i { v i , x , v i , y } G i ( v i , x ∨ v i , y ∨ ¬ u i ) i u igje vi , 1, vi , 2, … , Vi , n uje i ∈ [ t ] gje { vi , x, vi , y} gje ( vi , x∨ vi , y∨ ¬ uje) je n'est pas actif ". Dans l'affectation initiale, toutes les variables de vertex sont définies sur false et toutes les variables de sélection sont définies sur false, de sorte que ces clauses sont toutes satisfaites. Pour intégrer le comportement OR dans la composition, nous allons augmenter la formule pour garantir qu'une affectation satisfaisante définit au moins un sélecteur sur true et doit ensuite également former une couverture de sommet du graphique sélectionné.uje
Pour nous assurer que nous pouvons faire cette sélection tout en gardant la distance de retournement petite par rapport au nombre d'entrées , nous utilisons la structure d'un arbre binaire complet avec feuilles, qui a la hauteur . Numérotez les feuilles de à et associez la ème feuille à la variable qui contrôle si l'entrée est active ou non. Créez une nouvelle variable pour chaque nœud interne de l'arborescence binaire. Pour chaque nœud interne, soit sa variable correspondante soit et les variables de ses deux enfants et . Ajoutez la clauset log t 1 t i u i i x y z ( ¬ x ∨ y ∨ z ) ( x → ( y ∨ z ) ) xt t Journalt 1 t je uje je X y z ( ¬ x ∨ y∨ z) à la formule qui capture l'implication , imposant que ne peut être vrai que si l'un de ses enfants est vrai. Pour compléter la formule, ajoutez une clause singleton indiquant que la variable du nœud racine de l'arbre binaire doit être vraie. Dans l'affectation de vérité initiale, les valeurs de toutes les variables pour les nœuds internes sont définies sur false, ce qui satisfait toutes les clauses de la formule, à l'exception de la clause singleton exigeant que le nœud racine de l'arbre ait sa variable true.( x → ( y∨ z) ) X
Ceci termine la description de la formule et de l'affectation de vérité. Définissez le paramètre du problème FLIP DISTANCE pour être égal à , qui est convenablement limité pour une composition croisée. Il reste à montrer que l'on peut inverser variables pour rendre la formule vraie si un graphe d'entrée a un sommet de taille . ( k + log t + 1 ) k ′ G i kk′ ( k + logt + 1 ) k′ gje k
Dans le sens inverse, supposons que ait une couverture de sommet de taille . Définissez les variables correspondant aux sommets de la couverture sur true en les retournant. Définissez la variable de sélection sur true pour coder que l'entrée est activée et inversez les variables des nœuds d'arbre binaire interne sur le chemin de la feuille à la racine sur true. Il est facile de vérifier qu'il s'agit d'une affectation satisfaisante: les implications dans l'arbre binaire sont toutes satisfaites, la valeur du nœud racine est définie sur true, les clauses qui vérifient les bords de pour restent satisfaites parce que k k k u i i log t i G i ′ i ′ ≠ i u i ′ G igje k k k uje je Journalt je gje′ je′≠ i uje′ reste faux, tandis que les clauses du graphe sont satisfaites car pour chaque front, nous définissons au moins un point de terminaison sur true.gje
Pour la direction avant, supposons que la formule puisse être satisfaite en inversant au plus variables. Ensuite, nous devons retourner la variable du nœud racine sur true. Les implications dans l'arbre binaire imposent qu'au moins une variable de sélection d'une feuille soit définie sur true, disons . Pour satisfaire les implications codées dans l'arbre binaire, tous les nœuds internes sur le chemin de à la racine ont été définis sur true, ce qui représente flips. Puisque est défini sur true, les clauses faites pour le graphe ne sont pas satisfaites sur le littéral , elles sont donc satisfaites car l'un des points d'extrémité de chaque bord deu i u i 1 + log t u i G i ¬ u i G i 1 + log t k k G ik + logt + 1 uje uje 1 + journalt uje gje ¬ uje gje est défini sur true. Puisqu'au moins variables de l'arbre binaire ont été inversées, au plus sommets-variables sont inversés à true dans cette solution. Cela code un sommet de taille dans et prouve que l'une des entrées est une instance YES. Ceci complète la preuve.1 + journalt k k gje
la source