Améliorer la réduction générique de Cook pour Clique en SAT?

Je souhaite réduire -Clique en SAT sans agrandir l'instance.$k$

La clique est en NP, elle peut donc être réduite à SAT en utilisant l'espace logarithmique. La réduction simple des manuels de Garey / Johnson fait exploser l'instance à la taille cubique . Cependant, -Clique est en P pour chaque fixe , il devrait donc y avoir une réduction efficace au moins pour fixe .$k$$k$$k$

Une façon de construire la réduction consiste à utiliser les variables SAT comme vecteur caractéristique , une variable définie sur true indiquant que le sommet associé est dans la clique. Cette réduction est naturelle mais crée une instance SAT de taille quadratique si le graphique est clairsemé. Pour un graphe clairsemé, de nombreuses clauses quadratiques sont nécessaires pour faire en sorte que dans chaque paire de sommets non adjacents, au plus un sommet puisse être dans la clique.

Essayons de faire mieux que .$O(n^2)$

La réduction générique de Cook / Schnorr / Pippenger / Fischer fonctionne en prenant d'abord un NDTM polynomialement limité dans le temps qui décide de la langue, en simulant le NDTM par un DTM inconscient, en simulant le DTM inconscient par un circuit, puis en simulant le circuit par un 3 -Instance SAM. Cela crée une instance 3-SAT de taille si la limite de temps NDTM est . Le facteur logarithmique semble inévitable en raison des frais généraux lors de la simulation par une machine inconsciente. Pour -Clique, on semble avoir , ce qui donne une instance 3-SAT de taille , qui est quasi linéaire pour fixe$O(t(n)\log t(n))$$t(n)$$k$$t(n) = O(nk)$$O(nk(\log n + \log k))$$k$. Dans son article de 1988, Cook a demandé s'il existait une meilleure réduction générique pour les langues en NP, et pour autant que je sache, cela est toujours ouvert. Cependant, Clique a beaucoup de structure donc on peut peut-être faire mieux dans ce cas.

Y a-t-il une meilleure réduction connue de Clique à SAT?

En particulier, est-il possible pour fixe de réduire -Clique en SAT tout en maintenant l'augmentation de la taille d'instance linéaire? Ou peut-on utiliser un résultat existant pour affirmer qu'il est peu probable que cela soit possible? J'ai essayé d'utiliser Fortnow / Santhanam et Dell / van Melkebeek mais les frais généraux semblent trop importants pour que ces résultats impliquent quoi que ce soit de spécifique.$k$$k$

(J'ai travaillé avec une réduction qui semble éviter le facteur logarithmique, mais avant de perdre plus de temps sur les détails sanglants pour vérifier son exactitude, je voudrais savoir si une telle réduction est déjà connue, ou s'il est peu probable qu'elle exister.)

Vous pouvez exprimer -clique comme une instance SAT avec variables et clauses. Pour fixe , c'est linéaire en .$k$$O(nk)$$O(nk^2)$$k$$n$

Soit si est le ème sommet de la clique (par ordre trié lexicographiquement). En d'autres termes, est un codage "à chaud" du ème sommet de la clique (c'est le vecteur caractéristique d'un ensemble à un élément). Cela introduit variables.$x_{iv}=1$$v$$i$$x_i$$i$$nk$

Maintenant, pour chacun vous pouvez imposer que les deux sommets correspondants sont connectés par une arête, en utilisant clauses. par exemple, une clause est où sont les sommets adjacents au sommet . Vous obtenez une clause par sommet . Cela introduit un total de clauses .$(i,j)$$n$$(\neg x_{iu} \lor x_{jv_1} \lor \dots \lor x_{jv_m})$$v_1,\dots,v_m$$u$$u$$O(nk^2)$

Pour chaque , vous pouvez imposer que est un vecteur de poids de Hamming 1 et que , en utilisant des clauses . Cela ajoute un total de clauses supplémentaires.$i$$x_i$$x_i < x_{i+1}$$O(n)$$O(nk)$

Il pourrait être possible de faire mieux en utilisant variables pour représenter les sommets de la clique ( bits suffisent pour représenter le ème sommet de la clique) puis en construisant un circuit pour vérifier si un ensemble de sommets correspondent à une clique. Une approche pour construire un tel circuit pourrait être de construire la liste de toutes les paires de ces sommets, dans l'ordre trié, puis de la comparer à la liste des arêtes en utilisant la procédure de fusion de Mergesort, ou quelque chose comme cette. Il pourrait être possible d'obtenir quelque chose comme un circuit de taille , qui se traduit alors par une instance SAT de la même taille (où$k \lg n$$\lg n$$i$$k$$k(k-1)/2$$O((n+m+k^2) \text{poly}(\lg n))$$m =$le nombre d'arêtes dans le graphique). Je n'ai pas essayé de travailler sur les détails pour voir si c'est réellement possible, cependant.