Tous les algorithmes connus pour résoudre des problèmes NP-complets sont-ils constructifs?

Existe-t-il des algorithmes connus qui donnent correctement "oui" à un problème NP-complet sans générer implicitement un certificat?

Je comprends qu'il est simple de transformer un oracle de satisfiabilité en un chercheur d'affectation satisfaisante: il suffit d'itérer sur les variables, en demandant à chaque fois à l'oracle de satisfiabilité de résoudre la conjonction de cette variable avec le problème d'origine.

Mais un tel emballage serait-il jamais utile? Tous les solveurs assis recherchent-ils l'espace des affectations possibles?

Ou existe-t-il des types de problèmes NP-complets (vendeur itinérant, somme de sous-ensemble, etc.) dans lesquels le solveur peut, par exemple, exploiter un théorème mathématique pour prouver qu'une solution doit exister? Comme faire une preuve par contradiction?

Si je comprends bien, vous posez deux questions: (1) y a-t-il par exemple des algorithmes SAT qui sont plus intelligents que la force brute naïve, et (2) y a-t-il des algorithmes qui donnent simplement une réponse OUI / NON lors de la résolution d'un problème NP-complet sans vraiment trouver la solution. Je répondrai aux deux questions dans cet ordre.

(1) Il est parfaitement possible de résoudre un problème sans force brute, c'est-à-dire sans essayer naïvement toutes les possibilités. Pour prendre votre exemple, les solveurs SAT complets modernes peuvent appliquer des algorithmes intelligents qui déduisent ou prouvent que certaines affectations (partielles) ne peuvent pas conduire à une solution, donc ils n'examinent même pas cette partie.

$n!$$n$$n$$O(2^nn^2)$

$k$

$k$$G$$k$$G$$k$

$O^*(2^k)$$k$

$k$$O^*(2^k)$