Encontrar uma solução para um problema de satisfação é mais difícil do que decidir a satisfação?

O problema de determinar se uma determinada expressão booleana é satisfatoriamente distinta em termos computacionais de realmente encontrar uma solução para a expressão?

Em outras palavras, existe outra maneira de descobrir que uma determinada expressão é satisfatória sem determinar explicitamente as 'configurações corretas' para as variáveis ​​booleanas? Ou todas as provas possíveis reduzem o tempo polinomial para as 'configurações corretas'?

Perdoe minha ignorância, sou apenas um estudante de engenharia. A Wikipedia parece sugerir que o ato de encontrar apenas SAT ou UNSAT é NP-completo.

Como mencionado em um comentário, qualquer método para determinar a satisfação de uma fórmula booleana pode ser facilmente convertido em um método para encontrar a atribuição de variável satisfatória. Isso ocorre porque todos os problemas de NP-completos são auto-redutíveis em baixa.

Da Wikipedia :

Auto-redutibilidade

O problema do SAT é auto-redutível, ou seja, cada algoritmo que responde corretamente se uma instância do SAT é solucionável pode ser usado para encontrar uma tarefa satisfatória. Primeiro, a pergunta é feita sobre a fórmula dada . Se a resposta for "não", a fórmula é insatisfatória. Caso contrário, a pergunta é feita na fórmula parcialmente instanciada , ou seja, com a primeira variável substituída por , e simplificada de acordo. Se a resposta for "sim", , caso contrário . Valores de outras variáveis ​​podem ser encontrados posteriormente da mesma maneira. No total, são necessárias execuções do algoritmo, onde$Φ$$Φ$$\{x_1=TRUE\}$$Φ$$x_1$$TRUE$$x_1=TRUE$$x_1=FALSE$$n+1$$n$ é o número de variáveis ​​distintas em .$Φ$

A resposta correta é que a determinação se existe uma solução e a determinação de uma solução são computacionalmente distintas. Nem todos os métodos para determinar se existe uma solução podem produzir uma solução. Existe uma solução para o problema do caminho hamiltoniano que pode determinar se existe um caminho, mas não pode produzir esse caminho. Dito isto, a questão é discutida por arxiv.org/abs/cs/0205064.