Труднее ли найти решение проблемы выполнимости, чем решить выполнимость?

Является ли проблема определения того, является ли данное булево выражение выполнимым в вычислительном отношении отличным от фактического нахождения решения выражения?

Другими словами, есть ли другой способ найти, что данное выражение выполнимо без явного определения «правильных настроек» для булевых переменных? Или все возможные доказательства сводятся за полиномиальное время к «правильным настройкам»?

Прости мое невежество, я всего лишь студент инженерного факультета. Википедия, по-видимому, подразумевает, что просто поиск SAT или UNSAT является NP-полным.

Как упомянуто в комментарии, любой метод определения выполнимости булевой формулы может быть легко преобразован в метод поиска удовлетворительного присвоения переменной. Это потому, что все NP-полные проблемы являются самоуничтожаемыми.

Из Википедии :

Self-сводимость

Проблема SAT является самовосстанавливаемой, то есть каждый алгоритм, который правильно отвечает, если экземпляр SAT является разрешимым, может использоваться для поиска удовлетворительного назначения. Сначала задается вопрос по заданной формуле . Если ответ «нет», формула неудовлетворительная. В противном случае вопрос задается по частично инстанцированной формуле , т. с заменой первой переменной на , и соответственно упрощается. Если ответ «да», то , иначе . Значения других переменных могут быть найдены впоследствии таким же образом. Всего требуется прогонов алгоритма, где$Φ$$Φ$$\{x_1=TRUE\}$$Φ$$x_1$$TRUE$$x_1=TRUE$$x_1=FALSE$$n+1$$n$ - число различных переменных в .$Φ$

Правильный ответ состоит в том, что определение, существует ли решение, и определение решения являются вычислительно различными. Не все методы определения того, существует ли решение, могут дать решение. Существует решение задачи о гамильтоновом пути, которое может определить, существует ли путь, но не может создать такой путь. При этом вопрос сделан спорным по arxiv.org/abs/cs/0205064.