Czy wszystkie znane algorytmy rozwiązywania problemów NP-zupełnych są konstruktywne?

Czy są znane algorytmy, które poprawnie wypisują odpowiedź „tak” dla problemu NP-complete bez pośredniego generowania certyfikatu?

Rozumiem, że łatwo jest przekształcić wyrocznię spełniającą w znajdującą satysfakcjonujące zadanie: po prostu iteruj po zmiennych, za każdym razem pytając wyrocznię spełniającą o rozwiązanie związku tej zmiennej z pierwotnym problemem.

Ale czy takie opakowanie byłoby kiedyś przydatne? Czy wszystkie satelitarne solwery przeszukują przestrzeń możliwych zadań?

A może istnieją jakieś rodzaje problemów z NP-zupełnością (podróżny sprzedawca, suma podzbiorów itp.), W których solver może, powiedzmy, wykorzystać twierdzenie matematyczne, aby udowodnić, że rozwiązanie musi istnieć? Jak robienie dowodu przez sprzeczność?

Jak rozumiem, zadajesz dwa pytania: (1) czy istnieją np. Algorytmy SAT, które są bardziej sprytne niż naiwna brutalna siła, oraz (2) istnieją algorytmy, które po prostu dają odpowiedź TAK / NIE podczas rozwiązywania problemu NP-zupełnego bez znalezienia rozwiązania. Odpowiem na oba pytania w tej kolejności.

(1) Rozwiązanie problemu jest możliwe bez brutalnej siły, tzn. Bez naiwnego wypróbowywania wszystkich możliwości. Na przykład nowoczesne kompletne solwery SAT mogą stosować sprytne algorytmy, które wywnioskują lub dowodzą, że pewne (częściowe) przypisania nie mogą prowadzić do rozwiązania, więc nawet nie badają tej części.

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

$k$

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

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

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