Est-il plus difficile de trouver une solution à un problème de satisfiabilité que de décider de la satisfiabilité?

Le problème de déterminer si une expression booléenne donnée est satisfaisante sur le plan du calcul est-il distinct de trouver réellement une solution à l'expression?

En d'autres termes, existe-t-il un autre moyen de trouver qu'une expression donnée est satisfaisable sans déterminer explicitement les `` bons paramètres '' pour les variables booléennes? Ou bien toutes les preuves possibles réduisent-elles le temps polynomial aux «bons paramètres»?

Pardonnez mon ignorance, je ne suis qu'un étudiant en génie. Wikipedia semble impliquer que le fait de simplement trouver SAT ou UNSAT est NP-complet.

Comme mentionné dans un commentaire, toute méthode de détermination de la satisfiabilité d'une formule booléenne peut être facilement convertie en une méthode pour trouver l'affectation de variable satisfaisante. En effet, tous les problèmes NP-complets sont auto-réductibles vers le bas.

De Wikipédia :

Auto-réductibilité

Le problème SAT est auto-réductible, c'est-à-dire que chaque algorithme qui répond correctement si une instance de SAT est résoluble peut être utilisé pour trouver une affectation satisfaisante. Tout d'abord, la question est posée sur la formule donnée . Si la réponse est "non", la formule n'est pas satisfaisante. Sinon, la question est posée sur la formule partiellement instanciée , c'est-à-dire avec la première variable remplacée par , et simplifiée en conséquence. Si la réponse est "oui", alors , sinon . Les valeurs des autres variables peuvent être retrouvées ultérieurement de la même manière. Au total, exécutions de l'algorithme sont nécessaires, où$Φ$$Φ$$\{x_1=TRUE\}$$Φ$$x_1$$TRUE$$x_1=TRUE$$x_1=FALSE$$n+1$$n$ est le nombre de variables distinctes dans .$Φ$

La bonne réponse est que la détermination de l'existence d'une solution et la détermination d'une solution sont distinctes sur le plan du calcul. Toutes les méthodes permettant de déterminer si une solution existe peuvent produire une solution. Il existe une solution au problème du chemin Hamiltonian qui peut déterminer si un chemin existe mais ne peut pas produire un tel chemin. Cela dit, la question est rendue théorique par arxiv.org/abs/cs/0205064.